Step 2.3 of order reduction: functoriality of Step 2 and of the maximal-contact case

[Kol07, 104, Step 2.3] ("as we noted in (34), the functoriality package is local") and clause (2) of [Kol07, Theorem 103]: BO_{n,m} commutes with smooth morphisms ([Kol07, 34.1]) and with change of fields ([Kol07, 34.2]). For the maximal-contact case BO^H_{n,m} (maxContactCase, Hironaka/Resolution/Algebraic/OrderReduction/Step22RestrictToHypersurface.lean) the package is assembled from the functoriality of Step 2.1 (Hironaka/Resolution/Algebraic/OrderReduction/Step21Functorial.lean) and the fields of the boundary-clearing data of [Kol07, Lemma 102] at the mark on the tuned Step 2.2 triple:

• the Step 2.2 triple of the pulled-back data, built on the pulled-back Step 2.1 sequence, is the pull-back of the Step 2.2 triple along the last-stage lift (isPullbackOf_step22TripleOfSeq, isBaseChangeOf_step22TripleOfSeq): the induced triples by isPullbackOf_induced_last, the boundary F_r + H_r by exceptionalFamily_pullback, strictTransformSeq_pullback at the last stage and comap_append;
• hence Step 2.2 commutes (step22Seq_pullback_of_surjective_aux, step22Seq_baseChange_aux): at the mark, which is preserved by a smooth surjection (maxOrd_comap_le_of_smooth, maxOrd_le_maxOrd_comap_of_surjective) and by a change of fields (maxOrd_comap_of_isPullback_specMap), by Lemma 102 at s(m) on the tuned triples, whose pull-back relation is isPullbackOf_tuned, resp. isBaseChangeOf_tuned; below the mark both sides are empty;
• Step 2 is the concatenation (step2Seq_pullback_of_surjective, step2Seq_baseChange; the Step 2.1 sequence of the pulled-back data is rewritten through the generalised step22TripleOfSeq), and BO^H_{n,m} follows through the case split of maxContactCase on the mark (maxContactCase_pullback_of_surjective, maxContactCase_baseChange).

The second clause of [Kol07, 34.1], for an arbitrary smooth morphism with the empty blow-ups deleted, is maxContactCase_eraseEmpty_pullback in Hironaka/Resolution/Algebraic/OrderReduction/Step2EraseEmpty.lean.

@[reducible, inline]

noncomputable abbrev Hironaka.BO.step22TripleOfSeq {k : Type u} [Field k] [CharZero k] {m : ℕ} (T : AlgebraicGeometry.Triple k) (S₁ : T.X.left.BlowUpSequence) (hS₁ : S₁.IsOrderSeq (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I T.E m) {H : T.X.left.IdealSheafData} (hsnc : ((S₁.exceptionalFamily T.E).append (S₁.strictTransformSeq H (Fin.last S₁.length))).IsSnc) : AlgebraicGeometry.Triple k

The Step 2.2 triple of H built from an arbitrary sequence S₁ of order m, given with its order proof and the normal-crossings proof of its boundary F_r + H_r; step22Triple is this at the Step 2.1 sequence.

Equations

• One or more equations did not get rendered due to their size.

theorem Hironaka.BO.isPullbackOf_step22TripleOfSeq {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) {H : T.X.left.IdealSheafData} (hsnc : ((S₁.exceptionalFamily T.E).append (S₁.strictTransformSeq H (Fin.last S₁.length))).IsSnc) (hsnc' : (((S₁.pullback h).exceptionalFamily T'.E).append ((S₁.pullback h).strictTransformSeq (H.comap h) (Fin.last (S₁.pullback h).length))).IsSnc) : (step22TripleOfSeq T' (S₁.pullback h) hS₁' hsnc').IsPullbackOf (step22TripleOfSeq T S₁ hS₁ hsnc) (S₁.pullbackLastHom h)

The Step 2.2 triple of h⁻¹H on the pulled-back Step 2.1 sequence is the pull-back of the Step 2.2 triple of H along the last-stage lift.

theorem Hironaka.BO.isBaseChangeOf_step22TripleOfSeq {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) {H : T.X.left.IdealSheafData} (hsnc : ((S₁.exceptionalFamily T.E).append (S₁.strictTransformSeq H (Fin.last S₁.length))).IsSnc) (hsnc' : (((S₁.pullback p).exceptionalFamily T'.E).append ((S₁.pullback p).strictTransformSeq (H.comap p) (Fin.last (S₁.pullback p).length))).IsSnc) : (step22TripleOfSeq T' (S₁.pullback p) hS₁' hsnc').IsBaseChangeOf (step22TripleOfSeq T S₁ hS₁ hsnc) σ (S₁.pullbackLastHom p)

The Step 2.2 triple of p⁻¹H on the base-changed Step 2.1 sequence is the base change of the Step 2.2 triple of H along the last-stage lift ([Kol07, 34.2]).

theorem Hironaka.BO.step22Seq_pullback_of_surjective_aux {k : Type u} [Field k] [CharZero k] {n m : ℕ} (bd : (m j : ℕ) → BDData n m j) (hm : 1 ≤ m) {T T' : AlgebraicGeometry.Triple k} (h : T'.X.left ⟶ T.X.left) [AlgebraicGeometry.Smooth h] (hs : Function.Surjective ⇑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) {H : T.X.left.IdealSheafData} (hsnc : ((S₁.exceptionalFamily T.E).append (S₁.strictTransformSeq H (Fin.last S₁.length))).IsSnc) (hsnc' : (((S₁.pullback h).exceptionalFamily T'.E).append ((S₁.pullback h).strictTransformSeq (H.comap h) (Fin.last (S₁.pullback h).length))).IsSnc) (j : ℕ) (hT₂ : AlgebraicGeometry.Triple.BDClass n m j (step22TripleOfSeq T S₁ hS₁ hsnc)) (hT₂' : AlgebraicGeometry.Triple.BDClass n m j (step22TripleOfSeq T' (S₁.pullback h) hS₁' hsnc')) : (step22Functor bd m j hm).seq (step22TripleOfSeq T' (S₁.pullback h) hS₁' hsnc') hT₂' = ((step22Functor bd m j hm).seq (step22TripleOfSeq T S₁ hS₁ hsnc) hT₂).pullback (S₁.pullbackLastHom h)

Step 2.2 (the boundary-clearing functor of [Kol07, Lemma 102] at the mark through the re-tuning) commutes with a smooth surjection between Step 2.2 triples related by the last-stage lift.

theorem Hironaka.BO.step22Seq_baseChange_aux {k : Type u} [Field k] [CharZero k] {n m : ℕ} (bd : (m j : ℕ) → BDData n m j) (hm : 1 ≤ 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) {H : T.X.left.IdealSheafData} (hsnc : ((S₁.exceptionalFamily T.E).append (S₁.strictTransformSeq H (Fin.last S₁.length))).IsSnc) (hsnc' : (((S₁.pullback p).exceptionalFamily T'.E).append ((S₁.pullback p).strictTransformSeq (H.comap p) (Fin.last (S₁.pullback p).length))).IsSnc) (j : ℕ) (hT₂ : AlgebraicGeometry.Triple.BDClass n m j (step22TripleOfSeq T S₁ hS₁ hsnc)) (hT₂' : AlgebraicGeometry.Triple.BDClass n m j (step22TripleOfSeq T' (S₁.pullback p) hS₁' hsnc')) : (step22Functor bd m j hm).seq (step22TripleOfSeq T' (S₁.pullback p) hS₁' hsnc') hT₂' = ((step22Functor bd m j hm).seq (step22TripleOfSeq T S₁ hS₁ hsnc) hT₂).pullback (S₁.pullbackLastHom p)

Step 2.2 commutes with a change of fields between Step 2.2 triples related by the last-stage lift ([Kol07, 34.2]).

theorem Hironaka.BO.step2Seq_pullback_of_surjective_aux {k : Type u} [Field k] [CharZero k] {n m : ℕ} (T : AlgebraicGeometry.Triple k) (hn : T.HasDimLE n) (hmax : T.I.maxOrd ≤ ↑m) (bd : (m j : ℕ) → BDData n m j) (hm : 1 ≤ m) {H : T.X.left.IdealSheafData} (hH : AlgebraicGeometry.IsSmoothDivisor H) (hle : AlgebraicGeometry.Scheme.IdealSheafData.IsMaximalContact (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I m H) {T' : AlgebraicGeometry.Triple k} (h : T'.X.left ⟶ T.X.left) [AlgebraicGeometry.Smooth h] (hs : Function.Surjective ⇑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) (e₁ : S₁' = (↑(step21Seq T hn hmax (bd m) (Fintype.card T.E.ι))).pullback h) (hsnc' : ((S₁'.exceptionalFamily T'.E).append (S₁'.strictTransformSeq (H.comap h) (Fin.last S₁'.length))).IsSnc) (j' : ℕ) (hj' : j' = Fintype.card ((↑(step21Seq T hn hmax (bd m) (Fintype.card T.E.ι))).exceptionalFamily T.E).ι) (hT₂' : AlgebraicGeometry.Triple.BDClass n m j' (step22TripleOfSeq T' S₁' hS₁' hsnc')) : S₁'.concat ((step22Functor bd m j' hm).seq (step22TripleOfSeq T' S₁' hS₁' hsnc') hT₂') = (step2Seq T hn hmax bd hm hH hle).pullback h

Step 2 on the pulled-back data, generalised over its Step 2.1 sequence S₁' with S₁' = S₁.pullback h: it is the pull-back of Step 2.

theorem Hironaka.BO.step2Seq_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 : (m j : ℕ) → BDData n m j) (hm : 1 ≤ m) {H : T.X.left.IdealSheafData} (hH : AlgebraicGeometry.IsSmoothDivisor H) (hle : AlgebraicGeometry.Scheme.IdealSheafData.IsMaximalContact (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I m H) {T' : AlgebraicGeometry.Triple k} (hn' : T'.HasDimLE n) (hmax' : T'.I.maxOrd ≤ ↑m) (h : T'.X.left ⟶ T.X.left) [AlgebraicGeometry.Smooth h] (hH' : AlgebraicGeometry.IsSmoothDivisor (H.comap h)) (hle' : AlgebraicGeometry.Scheme.IdealSheafData.IsMaximalContact (T'.X.left ↘ AlgebraicGeometry.Spec ↧k) T'.I m (H.comap h)) (hs : Function.Surjective ⇑h) (hpb : T'.IsPullbackOf T h) : step2Seq T' hn' hmax' bd hm hH' hle' = (step2Seq T hn hmax bd hm hH hle).pullback h

Step 2 commutes with smooth surjections ([Kol07, 104, Step 2.3] with the first clause of [Kol07, 34.1]).

theorem Hironaka.BO.step2Seq_baseChange_aux {k : Type u} [Field k] [CharZero k] {n m : ℕ} (T : AlgebraicGeometry.Triple k) (hn : T.HasDimLE n) (hmax : T.I.maxOrd ≤ ↑m) (bd : (m j : ℕ) → BDData n m j) (hm : 1 ≤ m) {H : T.X.left.IdealSheafData} (hH : AlgebraicGeometry.IsSmoothDivisor H) (hle : AlgebraicGeometry.Scheme.IdealSheafData.IsMaximalContact (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I m H) {L : Type u} [Field L] [CharZero L] {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 ↧L) T'.I T'.E m) (e₁ : S₁' = (↑(step21Seq T hn hmax (bd m) (Fintype.card T.E.ι))).pullback p) (hsnc' : ((S₁'.exceptionalFamily T'.E).append (S₁'.strictTransformSeq (H.comap p) (Fin.last S₁'.length))).IsSnc) (j' : ℕ) (hj' : j' = Fintype.card ((↑(step21Seq T hn hmax (bd m) (Fintype.card T.E.ι))).exceptionalFamily T.E).ι) (hT₂' : AlgebraicGeometry.Triple.BDClass n m j' (step22TripleOfSeq T' S₁' hS₁' hsnc')) : S₁'.concat ((step22Functor bd m j' hm).seq (step22TripleOfSeq T' S₁' hS₁' hsnc') hT₂') = (step2Seq T hn hmax bd hm hH hle).pullback p

Step 2 on the base-changed data, generalised over its Step 2.1 sequence.

theorem Hironaka.BO.step2Seq_baseChange {k : Type u} [Field k] [CharZero k] {n m : ℕ} (T : AlgebraicGeometry.Triple k) (hn : T.HasDimLE n) (hmax : T.I.maxOrd ≤ ↑m) (bd : (m j : ℕ) → BDData n m j) (hm : 1 ≤ m) {H : T.X.left.IdealSheafData} (hH : AlgebraicGeometry.IsSmoothDivisor H) (hle : AlgebraicGeometry.Scheme.IdealSheafData.IsMaximalContact (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I m H) {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) (hH' : AlgebraicGeometry.IsSmoothDivisor (H.comap p)) (hle' : AlgebraicGeometry.Scheme.IdealSheafData.IsMaximalContact (T'.X.left ↘ AlgebraicGeometry.Spec ↧L) T'.I m (H.comap p)) : step2Seq T' hn' hmax' bd hm hH' hle' = (step2Seq T hn hmax bd hm hH hle).pullback p

Step 2 commutes with change of fields ([Kol07, 34.2]).

theorem Hironaka.BO.maxContactCase_pullback_of_surjective {k : Type u} [Field k] [CharZero k] {n m : ℕ} (T : AlgebraicGeometry.Triple k) (hT : AlgebraicGeometry.Triple.BOClass n m T) {H : T.X.left.IdealSheafData} (hH : AlgebraicGeometry.IsSmoothDivisor H) (hle : AlgebraicGeometry.Scheme.IdealSheafData.IsMaximalContact (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I m H) (bd : (m j : ℕ) → BDData n m j) {T' : AlgebraicGeometry.Triple k} (hT' : AlgebraicGeometry.Triple.BOClass n m T') (h : T'.X.left ⟶ T.X.left) [AlgebraicGeometry.Smooth h] (hs : Function.Surjective ⇑h) (hpb : T'.IsPullbackOf T h) (hH' : AlgebraicGeometry.IsSmoothDivisor (H.comap h)) (hle' : AlgebraicGeometry.Scheme.IdealSheafData.IsMaximalContact (T'.X.left ↘ AlgebraicGeometry.Spec ↧k) T'.I m (H.comap h)) : maxContactCase T' hT' hH' hle' bd = (maxContactCase T hT hH hle bd).pullback h

The maximal-contact case of order reduction commutes with smooth surjections (clause (2) of [Kol07, Theorem 103] with the first clause of [Kol07, 34.1]).

theorem Hironaka.BO.maxContactCase_baseChange {k : Type u} [Field k] [CharZero k] {n m : ℕ} (T : AlgebraicGeometry.Triple k) (hT : AlgebraicGeometry.Triple.BOClass n m T) {H : T.X.left.IdealSheafData} (hH : AlgebraicGeometry.IsSmoothDivisor H) (hle : AlgebraicGeometry.Scheme.IdealSheafData.IsMaximalContact (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I m H) (bd : (m j : ℕ) → BDData n m j) {L : Type u} [Field L] [CharZero L] {T' : AlgebraicGeometry.Triple L} (hT' : AlgebraicGeometry.Triple.BOClass n m T') (σ : k →+* L) (p : T'.X.left ⟶ T.X.left) (hbc : T'.IsBaseChangeOf T σ p) (hH' : AlgebraicGeometry.IsSmoothDivisor (H.comap p)) (hle' : AlgebraicGeometry.Scheme.IdealSheafData.IsMaximalContact (T'.X.left ↘ AlgebraicGeometry.Spec ↧L) T'.I m (H.comap p)) : maxContactCase T' hT' hH' hle' bd = (maxContactCase T hT hH hle bd).pullback p

The maximal-contact case of order reduction commutes with change of fields (clause (2) of [Kol07, Theorem 103] with [Kol07, 34.2]).