Step 2.3 of order reduction: functoriality of Step 2.1

[Kol07, 104, Step 2.3]: "Assuming functoriality in dimension < n, we have functoriality in Step 2.1 by the corresponding functoriality in (102)." Step 2.1 (step21Seq) is the concatenation, position by position, of the values BD_{n,m,j} of the boundary-clearing functor of [Kol07, Lemma 102] on the triples induced at the end of the sequence built so far. Its functoriality is therefore proved round by round through the concatenation:

• the pull-back of a concatenation is the concatenation of the pull-backs, the second along the lift of h to the last stage (pullback_concat, pullbackLastHom, Hironaka/Scheme/BlowUpSequence/ConcatPullback.lean), which is smooth, resp. surjective, when h is (smooth_pullbackLastHom, surjective_pullbackLastHom; [Kol07, 30.1]);
• the triple induced at a stage of the pulled-back sequence is the pull-back of the triple induced at that stage along the stage lift (IsPullbackOf.induced_isPullbackOf in Hironaka/Scheme/BlowUpSequence/BaseChangeTriple.lean), and at the last stage along the last-stage lift (isPullbackOf_induced_last); likewise for a change of fields (isBaseChangeOf_induced_last); the index transport pullbackStageIdx_last is the eqToHom inside pullbackLastHom;
• hence, by induction on the number of positions, Step 2.1 commutes with smooth surjections (step21Seq_pullback_of_surjective, the first clause of [Kol07, 34.1], from the field commutesWithSmooth of the data) and with change of fields (step21Seq_baseChange, [Kol07, 34.2], from the field commutesWithBaseChange). The induction is run on the whole value of step21Seq, the sequence with its order and no-empty-centres proofs, so that the induced triple of the pulled-back sequence can be rewritten without motive problems; the pulled-back triple has the same number of boundary members, as the inverse image keeps the index set.

The second clause of [Kol07, 34.1], for an arbitrary smooth morphism, is Hironaka/Resolution/Algebraic/OrderReduction/Step21EraseEmpty.lean.

theorem Hironaka.Sequence.smooth_pullbackLastHom {X Y : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (h : Y ⟶ X) [AlgebraicGeometry.Smooth h] : AlgebraicGeometry.Smooth (S.pullbackLastHom h)

The last-stage lift of a smooth morphism is smooth ([Kol07, 30.1]: "if B is a smooth blow-up sequence then so is h^*B").

theorem Hironaka.Sequence.surjective_pullbackLastHom {X Y : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (h : Y ⟶ X) [AlgebraicGeometry.Flat h] (hs : Function.Surjective ⇑h) : Function.Surjective ⇑(S.pullbackLastHom h)

The last-stage lift of a flat surjection is surjective (the pull-back of a blow-up sequence along a morphism, [Kol07, 30.1]; flat base change preserves surjectivity).

theorem Hironaka.BO.isPullbackOf_induced_last {k : Type u} [Field k] [CharZero k] {m : ℕ} {T T' : AlgebraicGeometry.Triple k} (h : T'.X.left ⟶ T.X.left) [AlgebraicGeometry.Smooth h] (hpb : T'.IsPullbackOf T h) {S : T.X.left.BlowUpSequence} (hS : S.IsOrderSeq (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I T.E m) (hS' : (S.pullback h).IsOrderSeq (T'.X.left ↘ AlgebraicGeometry.Spec ↧k) T'.I T'.E m) : (T'.induced (S.pullback h) hS' (Fin.last (S.pullback h).length)).IsPullbackOf (T.induced S hS (Fin.last S.length)) (S.pullbackLastHom h)

The triple induced at the end of the pulled-back sequence is the pull-back of the triple induced at the end of the sequence, along the last-stage lift (IsPullbackOf.induced_isPullbackOf at the last stage, in the form IsPullbackOf of the induced triples).

theorem Hironaka.BO.isBaseChangeOf_induced_last {k : Type u} [Field k] [CharZero k] {m : ℕ} {L : Type u} [Field L] [CharZero L] {T : AlgebraicGeometry.Triple k} {T' : AlgebraicGeometry.Triple L} (σ : k →+* L) (p : T'.X.left ⟶ T.X.left) (hbc : T'.IsBaseChangeOf T σ p) {S : T.X.left.BlowUpSequence} (hS : S.IsOrderSeq (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I T.E m) (hS' : (S.pullback p).IsOrderSeq (T'.X.left ↘ AlgebraicGeometry.Spec ↧L) T'.I T'.E m) : (T'.induced (S.pullback p) hS' (Fin.last (S.pullback p).length)).IsBaseChangeOf (T.induced S hS (Fin.last S.length)) σ (S.pullbackLastHom p)

The triple induced at the end of the base-changed sequence is the base change of the triple induced at the end of the sequence, along the last-stage lift (IsBaseChangeOf.induced_isBaseChangeOf at the last stage; [Kol07, 34.2]).

theorem Hironaka.BO.step21Seq_pullback_succ_aux {k : Type u} [Field k] [CharZero k] {n m : ℕ} (T : AlgebraicGeometry.Triple k) (hn : T.HasDimLE n) (hmax : T.I.maxOrd ≤ ↑m) (bd : (j : ℕ) → BDData n m j) {T' : AlgebraicGeometry.Triple k} (hn' : T'.HasDimLE n) (hmax' : T'.I.maxOrd ≤ ↑m) (h : T'.X.left ⟶ T.X.left) [AlgebraicGeometry.Smooth h] (hs : Function.Surjective ⇑h) (hpb : T'.IsPullbackOf T h) {j : ℕ} (σ' : { S : T'.X.left.BlowUpSequence // S.IsOrderSeq (T'.X.left ↘ AlgebraicGeometry.Spec ↧k) T'.I T'.E m ∧ S.NoEmptyCenters }) (σ : { S : T.X.left.BlowUpSequence // S.IsOrderSeq (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I T.E m ∧ S.NoEmptyCenters }) (hσ : ↑σ' = (↑σ).pullback h) (hj' : j < Fintype.card T'.E.ι) (hj : j < Fintype.card T.E.ι) : (↑σ').concat (((bd j).functor k).seq (T'.induced ↑σ' ⋯ (Fin.last (↑σ').length)) ⋯) = ((↑σ).concat (((bd j).functor k).seq (T.induced ↑σ ⋯ (Fin.last (↑σ).length)) ⋯)).pullback h

The inductive step of step21Seq_pullback_of_surjective, on the whole Step 2.1 values (sequence with its proofs): if the sequence after j rounds on the pulled-back data is the pull-back of the sequence after j rounds, so is the sequence after j + 1 rounds, by pullback_concat and the field commutesWithSmooth (first clause) of the boundary-clearing data on the induced triples at the last stage.

theorem Hironaka.BO.step21Seq_pullback_of_surjective {k : Type u} [Field k] [CharZero k] {n m : ℕ} (T : AlgebraicGeometry.Triple k) (hn : T.HasDimLE n) (hmax : T.I.maxOrd ≤ ↑m) (bd : (j : ℕ) → BDData n m j) {T' : AlgebraicGeometry.Triple k} (hn' : T'.HasDimLE n) (hmax' : T'.I.maxOrd ≤ ↑m) (h : T'.X.left ⟶ T.X.left) [AlgebraicGeometry.Smooth h] (hs : Function.Surjective ⇑h) (hpb : T'.IsPullbackOf T h) (j : ℕ) : ↑(step21Seq T' hn' hmax' bd j) = (↑(step21Seq T hn hmax bd j)).pullback h

Step 2.1 commutes with smooth surjections ([Kol07, 104, Step 2.3], "functoriality in Step 2.1 by the corresponding functoriality in (102)"; the first clause of [Kol07, 34.1]): round by round through the concatenation, by the field commutesWithSmooth of the boundary-clearing data on the induced triples.

theorem Hironaka.BO.step21Seq_baseChange_succ_aux {k : Type u} [Field k] [CharZero k] {n m : ℕ} (T : AlgebraicGeometry.Triple k) (hn : T.HasDimLE n) (hmax : T.I.maxOrd ≤ ↑m) (bd : (j : ℕ) → BDData n m j) {L : Type u} [Field L] [CharZero L] {T' : AlgebraicGeometry.Triple L} (hn' : T'.HasDimLE n) (hmax' : T'.I.maxOrd ≤ ↑m) (σ : k →+* L) (p : T'.X.left ⟶ T.X.left) (hbc : T'.IsBaseChangeOf T σ p) {j : ℕ} (τ' : { S : T'.X.left.BlowUpSequence // S.IsOrderSeq (T'.X.left ↘ AlgebraicGeometry.Spec ↧L) T'.I T'.E m ∧ S.NoEmptyCenters }) (τ : { S : T.X.left.BlowUpSequence // S.IsOrderSeq (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I T.E m ∧ S.NoEmptyCenters }) (hτ : ↑τ' = (↑τ).pullback p) (hj' : j < Fintype.card T'.E.ι) (hj : j < Fintype.card T.E.ι) : (↑τ').concat (((bd j).functor L).seq (T'.induced ↑τ' ⋯ (Fin.last (↑τ').length)) ⋯) = ((↑τ).concat (((bd j).functor k).seq (T.induced ↑τ ⋯ (Fin.last (↑τ).length)) ⋯)).pullback p

The inductive step of step21Seq_baseChange, on the whole Step 2.1 values: pullback_concat and the field commutesWithBaseChange of the boundary-clearing data on the induced triples at the last stage.

theorem Hironaka.BO.step21Seq_baseChange {k : Type u} [Field k] [CharZero k] {n m : ℕ} (T : AlgebraicGeometry.Triple k) (hn : T.HasDimLE n) (hmax : T.I.maxOrd ≤ ↑m) (bd : (j : ℕ) → BDData n m j) {L : Type u} [Field L] [CharZero L] {T' : AlgebraicGeometry.Triple L} (hn' : T'.HasDimLE n) (hmax' : T'.I.maxOrd ≤ ↑m) (σ : k →+* L) (p : T'.X.left ⟶ T.X.left) (hbc : T'.IsBaseChangeOf T σ p) (j : ℕ) : ↑(step21Seq T' hn' hmax' bd j) = (↑(step21Seq T hn hmax bd j)).pullback p

Step 2.1 commutes with change of fields ([Kol07, 104, Step 2.3]; [Kol07, 34.2]): round by round through the concatenation, by the field commutesWithBaseChange of the boundary-clearing data on the induced triples.