Functoriality of the loops of Steps 1 and 2 under smooth surjections #
The first clause of [Kol07, 34.1] for Steps 1 and 2 of the proof of [Kol07, Theorem 107] (Kol07,
111: "the functoriality conditions are just as obvious as before"). Step 1 is the loop of the
rounds BO_{n,d}(X, N(I), E) on the marked triples induced after each round
(Hironaka/Resolution/Algebraic/MarkedOrderReduction/Step1NonmonomialPart.lean), Step 2 the loop of
the rounds BO_{n,ms}(X, N(I)^m + I^s, E)
(Hironaka/Resolution/Algebraic/MarkedOrderReduction/Step2Separation.lean). Each round commutes
with a smooth surjection by clause (2) of [Kol07, Theorem 103] (BOData.commutesWithSmooth, first
clause) on the pulled-back round triple, since N(h^* I) = h^* N(I) and the loop variables are
preserved (roundOrder_of_isPullbackOf, sepOrder_of_isPullbackOf,
Hironaka/Resolution/Algebraic/MarkedOrderReduction/Parameters.lean); and the marked triple induced
at the end of the pulled-back round carries the pull-back data of the triple induced at the end of
the round, along the last-stage lift (MarkedTriple.isPullbackOf_induced_last, the marked form of
isPullbackOf_induced_last of
Hironaka/Resolution/Algebraic/OrderReduction/Step21Functorial.lean). By induction over the
well-founded recursions (on a bound for the loop variable, as in
maxOrd_nonmonomialPart_step1_lt_aux), step1 and step2 commute with smooth surjections
(step1_pullback_of_surjective, step2_pullback_of_surjective): the pull-back of a concatenation
is the concatenation of the pull-backs (pullback_concat), the induced triples are transported
along the equality of the rounds (MarkedTriple.isPullbackOf_induced_of_eq_seq, absorbing the
eqToHom), and the concatenation is re-assembled by concat_pullback_eqToHom. Step 3 and the whole
functor are treated in Hironaka/Resolution/Algebraic/MarkedOrderReduction/Step3Functorial.lean and
Functoriality.lean.
The marked triple induced at a stage of the pulled-back sequence carries the pull-back data of
the marked triple induced at that stage, along the stage lift, with the same mark (the marked form
of IsPullbackOf.induced_isPullbackOf; from the transport of marked transforms
IsOrderGeSeq.markedTransformSeq_comap_pullbackStageHom_mk and totalTransformSeq_pullback).
Transport of pull-back data of an induced marked triple along an equality of stage indices: the
eqToHom of the stage identification is absorbed (the marked form of
Triple.isPullbackOf_induced_of_eq_idx).
The marked triple induced at the end of the pulled-back sequence is the pull-back of the marked
triple induced at the end of the sequence, along the last-stage lift (the marked form of
isPullbackOf_induced_last; the transport shared by both clauses of [Kol07, 34.1]).
Transport of pull-back data of the last induced marked triple along an equality of sequences:
the eqToHom of the last-stage identification is absorbed.
The value of BO_{n,d} on a triple, transported along an equality of marks.
The round triple (X, N(I), E) of the pull-back data is the pull-back of the round triple,
since N(h^* I) = h^* N(I).
A round of Step 1 commutes with a smooth surjection (clause (2) of [Kol07, Theorem 103] with
the first clause of [Kol07, 34.1], per round): the round order is preserved and BO_{n,d}
commutes on the pulled-back round triple.
The induction behind step1_pullback_of_surjective: on a bound l for the loop variable,
following the recursion of step1.
Step 1 commutes with smooth surjections (the first clause of [Kol07, 34.1] for Step 1): round by round through the loop, by clause (2) of [Kol07, Theorem 103] on the pulled-back round triples.
The separating triple (X, N(I)^m + I^s, E) of the pull-back data is the pull-back of the
separating triple: N(h^* I) = h^* N(I), the separation order is preserved, and the inverse image
commutes with sums and powers.
A round of Step 2 commutes with a smooth surjection (clause (2) of [Kol07, Theorem 103] with
the first clause of [Kol07, 34.1], per round): the separation order is preserved and BO_{n,ms}
commutes on the pulled-back separating triple.
The induction behind step2_pullback_of_surjective: on a bound l for the separation order,
following the recursion of step2.
Step 2 commutes with smooth surjections (the first clause of [Kol07, 34.1] for Step 2): round by round through the loop, by clause (2) of [Kol07, Theorem 103] on the pulled-back separating triples.