The first centre of Step 2 when the hypersurface has an absorbed component

Step 2 of the proof of [Kol07, Theorem 103] on a triple (X, I, ∅) with max-ord I = 1 and a smooth hypersurface Y of maximal contact is [Kol07, Lemma 102] at the position of Y (Step 2.1 being empty for an empty boundary): its FIRST blow-up is π_{-1}, the blow-up of Z_{-1}(I, 1, Y), the union of the irreducible components of Y along which I has order ≥ 1 — when there is one (Z_{-1} ≠ 𝒪_X), the deletion of empty blow-ups [Kol07, 32] keeps it:

• dataFunctor_seq_eq_cons_of_Zminus1_ne_top: at the level of BD_{n,1,j} (dataFunctor, through the tuning identity at the mark 1);
• maxContactCase_bdData_eq_cons_of_Zminus1_ne_top: at the level of Step 2 with the data of Lemma 102 (the unfolding of maxContactCase for E = ∅; [Kol07, 104, Step 2.4]: "If E = ∅ then Step 2.1 does nothing").

This is the complementary case to maxContactCase_bdData_eq_pushforward (Z_{-1} = 𝒪_X, the descent along the closed embedding). Used by the core lemma of the smooth case (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedNilCore): the generic point of an absorbed component of Y is a generic point of V(I) lying in the first centre.

theorem Hironaka.Resolution.rawSeq_eraseEmpty_eq_cons_of_Zminus1_ne_top {k : Type u} [Field k] [CharZero k] {n : ℕ} {Dom : MarkedTriple k → Prop} (B : OrderGeSeqAssignment k Dom) (T : AlgebraicGeometry.Triple k) (m : ℕ) (j : T.E.ι) (hI : AlgebraicGeometry.Scheme.IdealSheafData.IsDBalanced (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I m) (hmax : T.I.maxOrd = ↑m) (hn : T.HasDimLE n) (hDom : ∀ (T' : MarkedTriple k), T'.HasDimLE (n - 1) → T'.m = m → Dom T') (hZ : BD.Zminus1 T.I m (T.E.component j) ≠ ⊤) : ∃ (D : T.X.left.IdealSheafData) (rest : D.blowUp.BlowUpSequence), (BD.rawSeq T m j hI hmax hn B hDom).eraseEmpty = AlgebraicGeometry.Scheme.BlowUpSequence.cons T.X.left D rest ∧ D = BD.Zminus1 T.I m (T.E.component j)

On the standing class of [Kol07, Lemma 102], when some component of E^j carries I of order ≥ m (Z_{-1} ≠ 𝒪_X), the output with its empty blow-ups deleted starts with π_{-1} — the blow-up of Z_{-1} (map_centerS), kept by the deletion since it is nonempty (the proof of Lemma 102).

theorem Hironaka.Resolution.dataFunctor_seq_eq_cons_of_Zminus1_ne_top {k : Type u} [Field k] [CharZero k] {n : ℕ} {Dom : MarkedTriple k → Prop} (B : OrderGeSeqAssignment k Dom) (T : AlgebraicGeometry.Triple k) {j : ℕ} (hj : j < Fintype.card T.E.ι) (hDom : ∀ (T' : MarkedTriple k), T'.HasDimLE (n - 1) → T'.m = IsLocalRing.tuningParam 1 → Dom T') (hT : AlgebraicGeometry.Triple.BDClass n 1 j T) (h1 : T.I.maxOrd = ↑1) (hZ : BD.Zminus1 T.I 1 (T.E.nth ⟨j, hj⟩) ≠ ⊤) : ∃ (D : T.X.left.IdealSheafData) (rest : D.blowUp.BlowUpSequence), (BD.dataFunctor n 1 j ⋯ B hDom).seq T hT = AlgebraicGeometry.Scheme.BlowUpSequence.cons T.X.left D rest ∧ D = BD.Zminus1 T.I 1 (T.E.nth ⟨j, hj⟩)

At the mark 1, on a triple of BDClass n 1 j with max-ord I = 1 whose j-th member E^j has a component along which I has order ≥ 1 (Z_{-1} ≠ 𝒪_X), BD_{n,1,j} starts with the blow-up of Z_{-1} — the tuning at the mark 1 is the identity (W_tuningParam_one, tuningParam_one).

theorem Hironaka.Resolution.step22_eq_cons_of_Zminus1_ne_top_aux {k : Type u} [Field k] [CharZero k] {n : ℕ} (T : AlgebraicGeometry.Triple k) {Y : T.X.left.IdealSheafData} (hE : IsEmpty T.E.ι) (Dom : (k : Type u) → [inst : Field k] → [CharZero k] → MarkedTriple k → Prop) (B : (k : Type u) → [inst : Field k] → [inst_1 : CharZero k] → OrderGeSeqAssignment k (Dom k)) (hDom : ∀ (m : ℕ) (k : Type u) [inst : Field k] [inst_1 : CharZero k] (T' : MarkedTriple k), T'.HasDimLE (n - 1) → T'.m = IsLocalRing.tuningParam m → Dom k T') (hB : ∀ (k : Type u) [inst : Field k] [inst_1 : CharZero k] (T' : MarkedTriple k) (hT' : Dom k T'), ((B k).endTriple T' hT').I.maxOrd < ↑T'.m) (hsm : ∀ (k : Type u) [inst : Field k] [inst_1 : CharZero k], (B k).CommutesWithSmooth) (hbc : ∀ (k L : Type u) [inst : Field k] [inst_1 : CharZero k] [inst_2 : Field L] [inst_3 : CharZero L] (σ : k →+* L), (B k).CommutesWithBaseChange (B L) σ) (S₁ : T.X.left.BlowUpSequence) (hS₁ : S₁.IsOrderSeq (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I T.E 1) (e₀ : S₁ = AlgebraicGeometry.Scheme.BlowUpSequence.nil T.X.left) (hsnc : ((S₁.exceptionalFamily T.E).append (S₁.strictTransformSeq Y (Fin.last S₁.length))).IsSnc) (j₂ : ℕ) (hj₂ : j₂ = 0) (hT₂ : AlgebraicGeometry.Triple.BDClass n 1 j₂ (BO.step22TripleOfSeq T S₁ hS₁ hsnc)) (h1 : T.I.maxOrd = ↑1) (hZ : BD.Zminus1 T.I 1 Y ≠ ⊤) : ∃ (D : T.X.left.IdealSheafData) (rest : D.blowUp.BlowUpSequence), S₁.concat ((BO.step22Functor (fun (m j : ℕ) => BD.bdData n m j Dom B ⋯ hB hsm hbc) 1 j₂ ⋯).seq (BO.step22TripleOfSeq T S₁ hS₁ hsnc) hT₂) = AlgebraicGeometry.Scheme.BlowUpSequence.cons T.X.left D rest ∧ D = BD.Zminus1 T.I 1 Y

[Kol07, 104, Step 2.4] ("If E = ∅ then Step 2.1 does nothing"), generalised over the Step 2.1 sequence as step22_closedEmbedding_aux: for S₁ = nil, Step 2.2 with the data at the mark 1 on the Step 2.2 triple of Y starts with the blow-up of Z_{-1}(I, 1, Y) when the latter is not the unit ideal.

theorem Hironaka.Resolution.maxContactCase_bdData_eq_cons_of_Zminus1_ne_top {k : Type u} [Field k] [CharZero k] {n : ℕ} (T : AlgebraicGeometry.Triple k) {Y : T.X.left.IdealSheafData} (hY : AlgebraicGeometry.IsSmoothDivisor Y) (hle : AlgebraicGeometry.Scheme.IdealSheafData.IsMaximalContact (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I 1 Y) (hE : IsEmpty T.E.ι) (Dom : (k : Type u) → [inst : Field k] → [CharZero k] → MarkedTriple k → Prop) (B : (k : Type u) → [inst : Field k] → [inst_1 : CharZero k] → OrderGeSeqAssignment k (Dom k)) (hDom : ∀ (m : ℕ) (k : Type u) [inst : Field k] [inst_1 : CharZero k] (T' : MarkedTriple k), T'.HasDimLE (n - 1) → T'.m = IsLocalRing.tuningParam m → Dom k T') (hB : ∀ (k : Type u) [inst : Field k] [inst_1 : CharZero k] (T' : MarkedTriple k) (hT' : Dom k T'), ((B k).endTriple T' hT').I.maxOrd < ↑T'.m) (hsm : ∀ (k : Type u) [inst : Field k] [inst_1 : CharZero k], (B k).CommutesWithSmooth) (hbc : ∀ (k L : Type u) [inst : Field k] [inst_1 : CharZero k] [inst_2 : Field L] [inst_3 : CharZero L] (σ : k →+* L), (B k).CommutesWithBaseChange (B L) σ) (hT : AlgebraicGeometry.Triple.BOClass n 1 T) (h1 : T.I.maxOrd = ↑1) (hZ : BD.Zminus1 T.I 1 Y ≠ ⊤) : ∃ (D : T.X.left.IdealSheafData) (rest : D.blowUp.BlowUpSequence), (BO.maxContactCase T hT hY hle fun (m j : ℕ) => BD.bdData n m j Dom B ⋯ hB hsm hbc) = AlgebraicGeometry.Scheme.BlowUpSequence.cons T.X.left D rest ∧ D = BD.Zminus1 T.I 1 Y

Step 2 of the proof of [Kol07, Theorem 103] with the proof of [Kol07, Lemma 102]: on a triple (X, I, ∅) with max-ord I = 1 and a smooth hypersurface Y of maximal contact along which some component of Y has I of order ≥ 1 (Z_{-1}(I, 1, Y) ≠ 𝒪_X), BO^Y_{n,1}(X, I, ∅) with the data of Lemma 102 starts with the blow-up of Z_{-1}(I, 1, Y). The complementary case is maxContactCase_bdData_eq_pushforward.