Step 2.1 of order reduction under an arbitrary smooth morphism

Clause (2) of [Kol07, Theorem 103] with the second clause of [Kol07, 34.1]: 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. This module proves it for Step 2.1 of the proof ([Kol07, 104, Step 2.1], the sequence step21Seq), round by round through the concatenation (pullback_concat, eraseEmpty_concat): after j rounds the Step 2.1 sequence of the pulled-back data is the erased pull-back of the Step 2.1 sequence, and at the next round

• the triple induced by the erased pull-back (S.pullback h).eraseEmpty at its last stage is, up to its boundary, the exact pull-back of the triple induced by S.pullback h along the last-stage isomorphism eraseEmptyLastHom (isPullbackOf_inducedErased: the ideal by weakTransformSeq_eraseEmpty_last, the composite map by eraseEmptyLastHom_comp_composite);
• its boundary is the exact pull-back's boundary with the unit-ideal members deleted, the original positions preserved (eraseEmbeds_eraseEmpty, monoEquivOfFin_totalTransformSeq_of_lt), so the hypothesis hind : BDFamily.IndifferentToEmptyMembers bd, the indifference of the boundary-clearing data to empty boundary members (Hironaka/Resolution/Algebraic/OrderReduction/EmptyIndifferent.lean), identifies the value of the functor of [Kol07, Lemma 102] on the erased triple with its value on the exact pull-back;
• the second clause of [Kol07, 34.1] for Lemma 102 (the field commutesWithSmooth) on the exact pull-back along the smooth composite eraseEmptyLastHom ≫ pullbackLastHom, then pullback_comp and eraseEmpty_pullback_of_flat_surjective along the isomorphism.

Step 2.2 and the maximal-contact case are treated in Hironaka/Resolution/Algebraic/OrderReduction/Step2EraseEmpty.lean.

theorem Hironaka.BO.bdClass_of_isPullbackOf {k : Type u} [Field k] {n m : ℕ} {T T' : AlgebraicGeometry.Triple k} {j : ℕ} (g : T'.X.left ⟶ T.X.left) [AlgebraicGeometry.Smooth g] (hpb : T'.IsPullbackOf T g) (hT : AlgebraicGeometry.Triple.BDClass n m j T) (hn' : T'.HasDimLE n) : AlgebraicGeometry.Triple.BDClass n m j T'

The boundary-clearing class BDClass n m j is closed under exact pull-back along a smooth morphism with source of dimension ≤ n: the maximal order does not rise (maxOrd_comap_le_of_smooth) and the index set is unchanged.

theorem Hironaka.BO.isSnc_induced_E_comap_eraseEmptyLastHom {k : Type u} [Field k] [CharZero k] {m : ℕ} {T' : AlgebraicGeometry.Triple k} (P : T'.X.left.BlowUpSequence) (hP : P.IsOrderSeq (T'.X.left ↘ AlgebraicGeometry.Spec ↧k) T'.I T'.E m) : ((T'.induced P hP (Fin.last P.length)).E.comap P.eraseEmptyLastHom).IsSnc

The inverse image of the boundary induced by P along the last-stage isomorphism has normal crossings (isSnc_comap_of_smooth; the instances are supplied explicitly at the stage typing).

noncomputable def Hironaka.BO.inducedErased {k : Type u} [Field k] [CharZero k] {m : ℕ} {T' : AlgebraicGeometry.Triple k} (P : T'.X.left.BlowUpSequence) (hP : P.IsOrderSeq (T'.X.left ↘ AlgebraicGeometry.Spec ↧k) T'.I T'.E m) (hP' : P.eraseEmpty.IsOrderSeq (T'.X.left ↘ AlgebraicGeometry.Spec ↧k) T'.I T'.E m) : AlgebraicGeometry.Triple k

The triple induced by the erased sequence P.eraseEmpty at its last stage, with its boundary replaced by the inverse image, along the last-stage isomorphism, of the boundary induced by P: the exact pull-back of the triple induced by P (isPullbackOf_inducedErased). The boundary induced by P.eraseEmpty itself is this one with the unit-ideal members deleted.

Equations

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

theorem Hironaka.BO.inducedErased_update_eq {k : Type u} [Field k] [CharZero k] {m : ℕ} {T' : AlgebraicGeometry.Triple k} (P : T'.X.left.BlowUpSequence) (hP : P.IsOrderSeq (T'.X.left ↘ AlgebraicGeometry.Spec ↧k) T'.I T'.E m) (hP' : P.eraseEmpty.IsOrderSeq (T'.X.left ↘ AlgebraicGeometry.Spec ↧k) T'.I T'.E m) : (let __src := inducedErased P hP hP'; { X := __src.X, smoothOfRelativeDimension := ⋯, I := __src.I, isNonzeroEverywhere := ⋯, E := (T'.induced P.eraseEmpty hP' (Fin.last P.eraseEmpty.length)).E, isSnc := ⋯ }) = T'.induced P.eraseEmpty hP' (Fin.last P.eraseEmpty.length)

Restoring the erased boundary in inducedErased gives back the triple induced by P.eraseEmpty (structure eta).

theorem Hironaka.BO.isPullbackOf_inducedErased {k : Type u} [Field k] [CharZero k] {m : ℕ} {T' : AlgebraicGeometry.Triple k} {P : T'.X.left.BlowUpSequence} (hP : P.IsOrderSeq (T'.X.left ↘ AlgebraicGeometry.Spec ↧k) T'.I T'.E m) (hP' : P.eraseEmpty.IsOrderSeq (T'.X.left ↘ AlgebraicGeometry.Spec ↧k) T'.I T'.E m) : (inducedErased P hP hP').IsPullbackOf (T'.induced P hP (Fin.last P.length)) P.eraseEmptyLastHom

inducedErased P is the exact pull-back of the triple induced by P along the last-stage isomorphism (weakTransformSeq_eraseEmpty_last, eraseEmptyLastHom_comp_composite).

theorem Hironaka.BO.smooth_eraseEmptyLastHom_comp_pullbackLastHom {k : Type u} [Field k] [CharZero k] {m : ℕ} {T T' : AlgebraicGeometry.Triple k} (h : T'.X.left ⟶ T.X.left) [AlgebraicGeometry.Smooth 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) : AlgebraicGeometry.Smooth (CategoryTheory.CategoryStruct.comp (S.pullback h).eraseEmptyLastHom (S.pullbackLastHom h))

The smooth structure map of inducedErased P to the triple induced by S at the last stage: the last-stage isomorphism followed by the last-stage lift of h.

theorem Hironaka.BO.isPullbackOf_inducedErased_pullback {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) (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) : (inducedErased (S.pullback h) hP hP').IsPullbackOf (T.induced S hS (Fin.last S.length)) (CategoryTheory.CategoryStruct.comp (S.pullback h).eraseEmptyLastHom (S.pullbackLastHom h))

inducedErased (S.pullback h) is the exact pullback of the triple induced by S along eraseEmptyLastHom ≫ pullbackLastHom.

theorem Hironaka.BO.bdClass_inducedErased {k : Type u} [Field k] [CharZero k] {n m : ℕ} {T T' : AlgebraicGeometry.Triple k} (hn : T.HasDimLE n) (hmax : T.I.maxOrd ≤ ↑m) (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) (hne : S.NoEmptyCenters) (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) {j : ℕ} (hj : j < Fintype.card T.E.ι) : AlgebraicGeometry.Triple.BDClass n m j (inducedErased (S.pullback h) hP hP')

inducedErased (S.pullback h) lies in the boundary-clearing class at every position of the original family.

theorem Hironaka.BO.nthIdx_eraseEmpty_eq_of_originalIdx {Z : AlgebraicGeometry.Scheme} (P : Z.BlowUpSequence) (E : Z.DivisorFamily) (e : (P.eraseEmpty.totalTransformSeq E (Fin.last P.eraseEmpty.length)).ι ↪o (P.totalTransformSeq E (Fin.last P.length)).ι) (ho : ∀ (a : E.ι), e (P.eraseEmpty.originalIdx E (Fin.last P.eraseEmpty.length) a) = P.originalIdx E (Fin.last P.length) a) {j : ℕ} (hj : j < Fintype.card E.ι) (hj₁ : j < Fintype.card (P.eraseEmpty.totalTransformSeq E (Fin.last P.eraseEmpty.length)).ι) (hj₂ : j < Fintype.card (P.totalTransformSeq E (Fin.last P.length)).ι) : e ((P.eraseEmpty.totalTransformSeq E (Fin.last P.eraseEmpty.length)).nthIdx ⟨j, hj₁⟩) = (P.totalTransformSeq E (Fin.last P.length)).nthIdx ⟨j, hj₂⟩

The original position j is carried to the original position j by an embedding compatible with originalIdx (monoEquivOfFin_totalTransformSeq_of_lt).

theorem Hironaka.BO.functor_seq_induced_eraseEmpty_eq_inducedErased {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] (hpb : T'.IsPullbackOf T h) (hind : BDFamily.IndifferentToEmptyMembers bd) {S : T.X.left.BlowUpSequence} (hS : S.IsOrderSeq (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I T.E m) (hne : S.NoEmptyCenters) (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) (hne' : (S.pullback h).eraseEmpty.NoEmptyCenters) {j : ℕ} (hj : j < Fintype.card T.E.ι) (hj' : j < Fintype.card T'.E.ι) : ((bd j).functor k).seq (T'.induced (S.pullback h).eraseEmpty hP' (Fin.last (S.pullback h).eraseEmpty.length)) ⋯ = ((bd j).functor k).seq (inducedErased (S.pullback h) hP hP') ⋯

The boundary-clearing data at position j, if indifferent to empty boundary members, take the same value on the triple induced by the erased pull-back and on its exact-pull-back version inducedErased, whose boundary keeps the unit-ideal members.

theorem Hironaka.BO.functor_seq_inducedErased_eq {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) (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) (hne : S.NoEmptyCenters) (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) {j : ℕ} (hj : j < Fintype.card T.E.ι) : ((bd j).functor k).seq (inducedErased (S.pullback h) hP hP') ⋯ = ((((bd j).functor k).seq (T.induced S hS (Fin.last S.length)) ⋯).pullback (S.pullbackLastHom h)).eraseEmpty.pullback (S.pullback h).eraseEmptyLastHom

The value of the boundary-clearing data on inducedErased (S.pullback h) is the pull-back of its value on the triple induced by S, erased, then carried along the last-stage isomorphism: the second clause of [Kol07, 34.1] for [Kol07, Lemma 102] on the exact pull-back.

theorem Hironaka.BO.step21Seq_eraseEmpty_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] (hpb : T'.IsPullbackOf T h) (hind : BDFamily.IndifferentToEmptyMembers bd) {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).eraseEmpty) (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).eraseEmpty

The inductive step of step21Seq_eraseEmpty_pullback, on the whole Step 2.1 values: if the sequence after j rounds on the pulled-back data is the erased pull-back of the sequence after j rounds, so is the sequence after j + 1 rounds, by pullback_concat, eraseEmpty_concat, the indifference of bd j to the deleted unit-ideal members of the erased boundary (hind), the second clause of [Kol07, 34.1] for the boundary-clearing data on the exact pull-back of the induced triple along the smooth eraseEmptyLastHom ≫ pullbackLastHom, and eraseEmpty_pullback_of_flat_surjective along the isomorphism.

theorem Hironaka.BO.step21Seq_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 : (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] (hpb : T'.IsPullbackOf T h) (hind : BDFamily.IndifferentToEmptyMembers bd) (j : ℕ) : ↑(step21Seq T' hn' hmax' bd j) = ((↑(step21Seq T hn hmax bd j)).pullback h).eraseEmpty

For an arbitrary smooth morphism h, Step 2.1 on the pulled-back data is the pull-back of Step 2.1 with the empty blow-ups deleted (clause (2) of [Kol07, Theorem 103] with the second clause of [Kol07, 34.1], for Step 2.1), under the indifference of the boundary-clearing data to empty boundary members.