The maximal-contact case of order reduction under an arbitrary smooth morphism

Clause (2) of [Kol07, Theorem 103] with the second clause of [Kol07, 34.1], for the maximal-contact case: for an arbitrary smooth morphism h : Y ⟶ X, BO^{h⁻¹H}_{n,m}(Y, h^*I, h⁻¹E) is the pull-back of BO^H_{n,m}(X, I, E) with the empty blow-ups deleted, under the hypothesis hind : ∀ m, BDFamily.IndifferentToEmptyMembers (bd m) that the boundary-clearing data of [Kol07, Lemma 102] at every mark are indifferent to empty boundary members (Hironaka/Resolution/Algebraic/OrderReduction/EmptyIndifferent.lean).

• Step 2.1 is Hironaka/Resolution/Algebraic/OrderReduction/Step21EraseEmpty.lean.
• Step 2.2 (step22Seq_eraseEmpty_pullback_aux): the Step 2.2 triple of the erased pull-back, (X'_r, I'_r, F'_r + H'_r), becomes, once its boundary is replaced by the inverse image of F_r + H_r along the last-stage isomorphism and the last-stage lift (step22Erased), an exact pull-back of the Step 2.2 triple of H; F'_r + H'_r is that boundary with the unit-ideal members deleted, H'_r at the last position on both sides (exists_embedding_step22Erased, exceptionalFamily_eraseEmpty_embeds, strictTransformSeq_eraseEmpty_last). The hypothesis hind at the mark s(m) and the second clause of [Kol07, 34.1] for Lemma 102 on the tuned exact pull-back give the equality when both maximal orders are m; when the pulled-back maximal order drops below m, the erased pull-back is a smooth blow-up sequence of order s(m) for a tuned ideal of maximal order < s(m) without empty blow-ups, hence empty (eq_nil_of_isOrderSeq_of_maxOrd_lt, maxOrd_tuned_lt).
• step2Seq_eraseEmpty_pullback assembles both steps through pullback_concat and eraseEmpty_concat; maxContactCase_eraseEmpty_pullback reads the result back through the tuning of Step 1, the case max-ord h^*I < m ≤ max-ord I by the same emptiness argument.

theorem Hironaka.BO.maxOrd_W_lt_of_maxOrd_lt {k : Type u} [Field k] [CharZero k] {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧k) (n : ℕ) [AlgebraicGeometry.SmoothOfRelativeDimension n f] (I : X.IdealSheafData) {m : ℕ} (hm : 1 ≤ m) (hI : I.maxOrd < ↑m) {s : ℕ} (hs : 1 ≤ s) : (AlgebraicGeometry.Scheme.IdealSheafData.W f I m s).maxOrd < ↑s

Where the maximal order is below the mark, the maximal coefficient ideal is the unit ideal, of maximal order 0 < s (ord_W_eq_zero_of_ord_lt).

theorem Hironaka.BO.maxOrd_tuned_lt {k : Type u} [Field k] [CharZero k] {T : AlgebraicGeometry.Triple k} {m : ℕ} (hm : 1 ≤ m) (hI : T.I.maxOrd < ↑m) : (T.tuned m hm).I.maxOrd < ↑(IsLocalRing.tuningParam m)

The tuned triple of a triple of maximal order below the mark has maximal order below s(m).

theorem Hironaka.BO.step22Family_pullback_eq {k : Type u} [Field k] (T : AlgebraicGeometry.Triple k) {T' : AlgebraicGeometry.Triple k} (h : T'.X.left ⟶ T.X.left) [AlgebraicGeometry.Smooth h] (hpb : T'.IsPullbackOf T h) (S₁ : T.X.left.BlowUpSequence) (H : T.X.left.IdealSheafData) : ((S₁.pullback h).exceptionalFamily T'.E).append ((S₁.pullback h).strictTransformSeq (H.comap h) (Fin.last (S₁.pullback h).length)) = ((S₁.exceptionalFamily T.E).append (S₁.strictTransformSeq H (Fin.last S₁.length))).comap (S₁.pullbackLastHom h)

The Step 2.2 boundary of the pulled-back sequence is the inverse image of the Step 2.2 boundary along the last-stage lift (exceptionalFamily_pullback, strictTransformSeq_pullback_last).

theorem Hironaka.BO.isSnc_step22Family_pullback {k : Type u} [Field k] [CharZero k] {m : ℕ} (T : AlgebraicGeometry.Triple k) {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) {H : T.X.left.IdealSheafData} (hsnc : ((S₁.exceptionalFamily T.E).append (S₁.strictTransformSeq H (Fin.last S₁.length))).IsSnc) : (((S₁.pullback h).exceptionalFamily T'.E).append ((S₁.pullback h).strictTransformSeq (H.comap h) (Fin.last (S₁.pullback h).length))).IsSnc

The Step 2.2 boundary of the pulled-back sequence has normal crossings.

theorem Hironaka.BO.isSnc_step22Erased_E {k : Type u} [Field k] [CharZero k] {m : ℕ} (T : AlgebraicGeometry.Triple k) {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) (hP : (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) : ((((S₁.pullback h).exceptionalFamily T'.E).append ((S₁.pullback h).strictTransformSeq (H.comap h) (Fin.last (S₁.pullback h).length))).comap (S₁.pullback h).eraseEmptyLastHom).IsSnc

The inverse image of the Step 2.2 boundary of the pulled-back sequence along the last-stage isomorphism has normal crossings.

noncomputable def Hironaka.BO.step22Erased {k : Type u} [Field k] [CharZero k] {m : ℕ} (T : AlgebraicGeometry.Triple k) {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) (hP : (S₁.pullback h).IsOrderSeq (T'.X.left ↘ AlgebraicGeometry.Spec ↧k) T'.I T'.E m) (hP' : (S₁.pullback h).eraseEmpty.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 the erased pull-back with its boundary replaced by the inverse image of the Step 2.2 boundary of the pull-back along the last-stage isomorphism: the exact pull-back of the Step 2.2 triple of H (isPullbackOf_step22Erased_comp). The boundary F'_r + H'_r of the actual Step 2.2 triple is this one with the unit-ideal members deleted (exists_embedding_step22Erased).

Equations

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

theorem Hironaka.BO.isPullbackOf_step22Erased {k : Type u} [Field k] [CharZero k] {m : ℕ} (T : AlgebraicGeometry.Triple k) {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) (hP : (S₁.pullback h).IsOrderSeq (T'.X.left ↘ AlgebraicGeometry.Spec ↧k) T'.I T'.E m) (hP' : (S₁.pullback h).eraseEmpty.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) : (step22Erased T h hpb hS₁ hP hP' hsnc).IsPullbackOf (step22TripleOfSeq T' (S₁.pullback h) hP ⋯) (S₁.pullback h).eraseEmptyLastHom

step22Erased is the exact pull-back of the Step 2.2 triple of the pulled-back sequence along the last-stage isomorphism.

theorem Hironaka.BO.isPullbackOf_step22Erased_comp {k : Type u} [Field k] [CharZero k] {m : ℕ} (T : AlgebraicGeometry.Triple k) {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) (hP : (S₁.pullback h).IsOrderSeq (T'.X.left ↘ AlgebraicGeometry.Spec ↧k) T'.I T'.E m) (hP' : (S₁.pullback h).eraseEmpty.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) : (step22Erased T h hpb hS₁ hP hP' hsnc).IsPullbackOf (step22TripleOfSeq T S₁ hS₁ hsnc) (CategoryTheory.CategoryStruct.comp (S₁.pullback h).eraseEmptyLastHom (S₁.pullbackLastHom h))

step22Erased is the exact pull-back of the Step 2.2 triple of H along the last-stage isomorphism followed by the last-stage lift of h.

theorem Hironaka.BO.smooth_step22Erased_hom {k : Type u} [Field k] [CharZero k] {m : ℕ} (T : AlgebraicGeometry.Triple k) {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) (hP : (S₁.pullback h).IsOrderSeq (T'.X.left ↘ AlgebraicGeometry.Spec ↧k) T'.I T'.E m) (hP' : (S₁.pullback h).eraseEmpty.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.Smooth (CategoryTheory.CategoryStruct.comp (S₁.pullback h).eraseEmptyLastHom (S₁.pullbackLastHom h))

The structure map of step22Erased to the Step 2.2 triple of H is smooth.

theorem Hironaka.BO.bdClass_step22Erased {k : Type u} [Field k] [CharZero k] {n m : ℕ} (T : AlgebraicGeometry.Triple k) {T' : AlgebraicGeometry.Triple k} (hn' : T'.HasDimLE n) (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) (hP : (S₁.pullback h).IsOrderSeq (T'.X.left ↘ AlgebraicGeometry.Spec ↧k) T'.I T'.E m) (hP' : (S₁.pullback h).eraseEmpty.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) {j : ℕ} (hT₂ : AlgebraicGeometry.Triple.BDClass n m j (step22TripleOfSeq T S₁ hS₁ hsnc)) : AlgebraicGeometry.Triple.BDClass n m j (step22Erased T h hpb hS₁ hP hP' hsnc)

step22Erased lies in the boundary-clearing class at every position at which the Step 2.2 triple of H does.

theorem Hironaka.BO.step22Erased_update_eq {k : Type u} [Field k] [CharZero k] {m : ℕ} (T : AlgebraicGeometry.Triple k) (hm : 1 ≤ m) {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) (hP : (S₁.pullback h).IsOrderSeq (T'.X.left ↘ AlgebraicGeometry.Spec ↧k) T'.I T'.E m) (hP' : (S₁.pullback h).eraseEmpty.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).eraseEmpty.exceptionalFamily T'.E).append ((S₁.pullback h).eraseEmpty.strictTransformSeq (H.comap h) (Fin.last (S₁.pullback h).eraseEmpty.length))).IsSnc) : (let __src := (step22Erased T h hpb hS₁ hP hP' hsnc).tuned m hm; { X := __src.X, smoothOfRelativeDimension := ⋯, I := __src.I, isNonzeroEverywhere := ⋯, E := ((S₁.pullback h).eraseEmpty.exceptionalFamily T'.E).append ((S₁.pullback h).eraseEmpty.strictTransformSeq (H.comap h) (Fin.last (S₁.pullback h).eraseEmpty.length)), isSnc := hsnc' }) = (step22TripleOfSeq T' (S₁.pullback h).eraseEmpty hP' hsnc').tuned m hm

Restoring the erased boundary in step22Erased gives back the Step 2.2 triple of the erased pullback (structure eta).

theorem Hironaka.BO.exists_embedding_step22Erased {k : Type u} [Field k] [CharZero k] {m : ℕ} (T : AlgebraicGeometry.Triple k) {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) (hP : (S₁.pullback h).IsOrderSeq (T'.X.left ↘ AlgebraicGeometry.Spec ↧k) T'.I T'.E m) (hP' : (S₁.pullback h).eraseEmpty.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) (hj' : Fintype.card ((S₁.pullback h).eraseEmpty.exceptionalFamily T'.E).ι < Fintype.card (((S₁.pullback h).eraseEmpty.exceptionalFamily T'.E).append ((S₁.pullback h).eraseEmpty.strictTransformSeq (H.comap h) (Fin.last (S₁.pullback h).eraseEmpty.length))).ι) (hj : Fintype.card ((S₁.pullback h).exceptionalFamily T'.E).ι < Fintype.card (step22Erased T h hpb hS₁ hP hP' hsnc).E.ι) : ∃ (e : (((S₁.pullback h).eraseEmpty.exceptionalFamily T'.E).append ((S₁.pullback h).eraseEmpty.strictTransformSeq (H.comap h) (Fin.last (S₁.pullback h).eraseEmpty.length))).ι ↪o (step22Erased T h hpb hS₁ hP hP' hsnc).E.ι), (∀ (i : (((S₁.pullback h).eraseEmpty.exceptionalFamily T'.E).append ((S₁.pullback h).eraseEmpty.strictTransformSeq (H.comap h) (Fin.last (S₁.pullback h).eraseEmpty.length))).ι), (step22Erased T h hpb hS₁ hP hP' hsnc).E.component (e i) = (((S₁.pullback h).eraseEmpty.exceptionalFamily T'.E).append ((S₁.pullback h).eraseEmpty.strictTransformSeq (H.comap h) (Fin.last (S₁.pullback h).eraseEmpty.length))).component i) ∧ (∀ b ∉ Set.range ⇑e, (step22Erased T h hpb hS₁ hP hP' hsnc).E.component b = ⊤) ∧ e ((((S₁.pullback h).eraseEmpty.exceptionalFamily T'.E).append ((S₁.pullback h).eraseEmpty.strictTransformSeq (H.comap h) (Fin.last (S₁.pullback h).eraseEmpty.length))).nthIdx ⟨Fintype.card ((S₁.pullback h).eraseEmpty.exceptionalFamily T'.E).ι, hj'⟩) = (step22Erased T h hpb hS₁ hP hP' hsnc).E.nthIdx ⟨Fintype.card ((S₁.pullback h).exceptionalFamily T'.E).ι, hj⟩

The Step 2.2 boundary F'_r + H'_r of the erased pull-back embeds into the boundary of step22Erased as a deletion of unit-ideal members, H'_r ↦ H_r at the last positions (exceptionalFamily_eraseEmpty_embeds, strictTransformSeq_eraseEmpty_last, monoEquivOfFin_lex_inr_last).

theorem Hironaka.BO.step22Seq_eraseEmpty_pullback_aux {k : Type u} [Field k] [CharZero k] {n m : ℕ} (T : AlgebraicGeometry.Triple k) (bd : (m j : ℕ) → BDData n m j) (hm : 1 ≤ m) {T' : AlgebraicGeometry.Triple k} (hn' : T'.HasDimLE n) (h : T'.X.left ⟶ T.X.left) [AlgebraicGeometry.Smooth h] (hpb : T'.IsPullbackOf T h) (hind : ∀ (m : ℕ), BDFamily.IndifferentToEmptyMembers (bd m)) {S₁ : T.X.left.BlowUpSequence} (hS₁ : S₁.IsOrderSeq (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I T.E m) (hP : (S₁.pullback h).IsOrderSeq (T'.X.left ↘ AlgebraicGeometry.Spec ↧k) T'.I T'.E m) (hP' : (S₁.pullback h).eraseEmpty.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).eraseEmpty.exceptionalFamily T'.E).append ((S₁.pullback h).eraseEmpty.strictTransformSeq (H.comap h) (Fin.last (S₁.pullback h).eraseEmpty.length))).IsSnc) {j j' : ℕ} (hj : j = Fintype.card ((S₁.pullback h).exceptionalFamily T'.E).ι) (hj' : j' = Fintype.card ((S₁.pullback h).eraseEmpty.exceptionalFamily T'.E).ι) (hT₂ : AlgebraicGeometry.Triple.BDClass n m j (step22TripleOfSeq T S₁ hS₁ hsnc)) (hT₂' : AlgebraicGeometry.Triple.BDClass n m j' (step22TripleOfSeq T' (S₁.pullback h).eraseEmpty hP' hsnc')) : (step22Functor bd m j' hm).seq (step22TripleOfSeq T' (S₁.pullback h).eraseEmpty hP' hsnc') hT₂' = (((step22Functor bd m j hm).seq (step22TripleOfSeq T S₁ hS₁ hsnc) hT₂).pullback (S₁.pullbackLastHom h)).eraseEmpty.pullback (S₁.pullback h).eraseEmptyLastHom

Step 2.2 on the erased pull-back is the erased pull-back of Step 2.2, carried along the last-stage isomorphism ([Kol07, 104, Step 2.3] with the second clause of [Kol07, 34.1]; the boundary-clearing functor of [Kol07, Lemma 102] at the mark through the re-tuning): the indifference hind at the mark s(m), at the position of H'_r against that of H_r, the second clause of [Kol07, 34.1] for the boundary-clearing data on the tuned exact pull-back, and the emptiness of the erased pull-back when the maximal order of the pull-back drops below m.

theorem Hironaka.BO.step2Seq_eraseEmpty_pullback_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} (hn' : T'.HasDimLE n) (h : T'.X.left ⟶ T.X.left) [AlgebraicGeometry.Smooth h] (hpb : T'.IsPullbackOf T h) (hind : ∀ (m : ℕ), BDFamily.IndifferentToEmptyMembers (bd m)) (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).eraseEmpty) (hsnc' : ((S₁'.exceptionalFamily T'.E).append (S₁'.strictTransformSeq (H.comap h) (Fin.last S₁'.length))).IsSnc) (j' : ℕ) (hj' : j' = Fintype.card (S₁'.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).eraseEmpty

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

theorem Hironaka.BO.step2Seq_eraseEmpty_pullback {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)) (hpb : T'.IsPullbackOf T h) (hind : ∀ (m : ℕ), BDFamily.IndifferentToEmptyMembers (bd m)) : step2Seq T' hn' hmax' bd hm hH' hle' = ((step2Seq T hn hmax bd hm hH hle).pullback h).eraseEmpty

For an arbitrary smooth morphism h, Step 2 on the pulled-back data is the pull-back of Step 2 with the empty blow-ups deleted ([Kol07, 104, Step 2.3] with the second clause of [Kol07, 34.1]).

theorem Hironaka.BO.maxContactCase_eraseEmpty_pullback {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) (hind : ∀ (m : ℕ), BDFamily.IndifferentToEmptyMembers (bd m)) {T' : AlgebraicGeometry.Triple k} (hT' : AlgebraicGeometry.Triple.BOClass n m T') (h : T'.X.left ⟶ T.X.left) [AlgebraicGeometry.Smooth 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).eraseEmpty

The maximal-contact case of order reduction commutes with arbitrary smooth morphisms (clause (2) of [Kol07, Theorem 103] with the second clause of [Kol07, 34.1]): for every smooth h, BO^{h⁻¹H}_{n,m}(Y, h^*I, h⁻¹E) is the pull-back of BO^H_{n,m}(X, I, E) with its empty blow-ups deleted, under the hypothesis hind that the boundary-clearing data of [Kol07, Lemma 102] at every mark are indifferent to empty boundary members.