CP3 along Step 2.2

Step 2.2 of the proof of [Kol07, Theorem 103] (item 104, Step 2.2) applies [Kol07, Lemma 102] at the position of H_r on the Step 2.2 triple (X_r, I_r, F_r + H_r), through the re-tuning at the mark 1 (the identity). The statement CP3 of the embedded desingularization (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedChainRelative) along it for (I_r, E_r), E_r the FULL total transform of E:

• along the raw output of Lemma 102 over H_r for the family F_r = (F_r + H_r) − H_r (cp3For_rawSeq_erase_of_le): the first centre Z₋₁ by the ring-level classification (centerClassifiedAt_of_stalkIdeal_le_of_isSncAt_append; F_r + H_r snc at q from isSnc_erase_append, the stalk of Z₋₁ by stalkIdeal_Zminus1_eq, and I_r ≤ H_r at q from the order 1 of I_r at the generic point of the component of H_r through q, mem_support_Zminus1_iff_ord_eq, stalkIdeal_vanishingIdeal_closure_eq_of_isSmoothDivisor); the later centres by the pointwise pass centerClassifiedAt_of_comap_chain (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP3Chain) with the identities of [Kol07, Lemma 62] as in cp3For_rawSeq_member, the snc of the transform of F_r with that of H_r from the snc of the transform of the full family (isSncAt_of_injective, exists_embeds_totalTransformSeq'), the maximal contact carried along (strictTransformSeq_le_markedTransformSeq_MC) and the stalk of I_r proper at a point of a centre (the centre has order ≥ 1);
• the family bridge cp3For_of_embeds (centerClassifiedAt_iff_of_embeds): F_r ↪ E_r, the members of E_r outside F_r being the birational transforms of the original members, which miss V(I_r) at the end of Step 2.1 (disjoint_support_markedTransformSeq_step21_final, Hironaka.Resolution.Algebraic.Wlo05.EmbeddedStep21Passage) and hence every later centre (disjoint_support_markedTransformSeq_strictTransformSeq; a centre lies in V(I_i));
• the assembly (cp3For_step22_aux, cp3For_step22): below the mark the re-tuned Lemma 102 is empty (step22Functor_seq_of_maxOrd_lt); at the mark, max-ord I = 1 too (below it Step 2.1 is empty and I_r = I), the value is the raw output with its empty blow-ups deleted (step22Functor_seq_of_maxOrd_eq, functor_seq_congr_mark, dataFunctor_seq_of_maxOrd_eq, functor_seq), cp3For_eraseEmpty deletes them, and the tuned ideal is I_r (W_tuningParam_one, [Kol07, Remark 67]).

This argument is not in the literature. Used in Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP3Tower.

theorem Hironaka.Resolution.cp3For_of_embeds {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (I : X.IdealSheafData) {E₁ E₂ : X.DivisorFamily} (e₀ : E₁.ι → E₂.ι) (he₀ : Function.Injective e₀) (hcomp₀ : ∀ (a : E₁.ι), E₂.component (e₀ a) = E₁.component a) (hmiss : ∀ (i : Fin S.length), ∀ q ∈ (S.center i).support, ∀ a ∉ Set.range e₀, q ∉ ((S.totalTransformSeq E₂ i.castSucc).component (S.originalIdx E₂ i.castSucc a)).support) (h : CP3For S I E₁) : CP3For S I E₂

CP3For transports to a bigger family whose extra members miss every point of a centre (the counterpart of cp1For_of_embeds).

theorem Hironaka.Resolution.cp3For_rawSeq_erase_of_le {k : Type u} [Field k] [CharZero k] {N : ℕ} {Dom' : MarkedTriple k → Prop} (B' : OrderGeSeqAssignment k Dom') (T : AlgebraicGeometry.Triple k) (j : T.E.ι) (hI : AlgebraicGeometry.Scheme.IdealSheafData.IsDBalanced (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I 1) (hmax : T.I.maxOrd = 1) (hn : T.HasDimLE N) (hDom' : ∀ (T' : MarkedTriple k), T'.HasDimLE (N - 1) → T'.m = 1 → Dom' T') (hcp3 : ∀ (T' : MarkedTriple k) (hT' : Dom' T'), T'.m = 1 → CP3For (B'.seq T' hT') T'.I T'.E) (hHJ : T.E.component j ≤ T.I) : CP3For (BD.rawSeq T 1 j hI hmax hn B' hDom') T.I (T.E.erase j)

The pass over a hypersurface of maximal contact, classified for the boundary without it: CP3 along the raw output of Lemma 102 over the member Eʲ ⊆ V(I) (i.e. Eʲ ≤ I) for the outer data (I, E − Eʲ) from CP3 for the inductive run.

theorem Hironaka.Resolution.cp3For_rawSeq_erase_of_le_of_eq_one {k : Type u} [Field k] [CharZero k] {N : ℕ} {Dom' : MarkedTriple k → Prop} (B' : OrderGeSeqAssignment k Dom') (T : AlgebraicGeometry.Triple k) (j : T.E.ι) (m : ℕ) (hm1 : m = 1) (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') (hcp3 : ∀ (T' : MarkedTriple k) (hT' : Dom' T'), T'.m = 1 → CP3For (B'.seq T' hT') T'.I T'.E) (hHJ : T.E.component j ≤ T.I) : CP3For (BD.rawSeq T m j hI hmax hn B' hDom') T.I (T.E.erase j)

The pass with the mark carried as a variable (the mark of the tuned triple is tuningParam 1).

theorem Hironaka.Resolution.cp3For_step22_aux {k : Type u} [Field k] [CharZero k] {N : ℕ} (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) σ) (T : AlgebraicGeometry.Triple k) (hmax : T.I.maxOrd ≤ 1) {H : T.X.left.IdealSheafData} (hH : AlgebraicGeometry.IsSmoothDivisor H) (hle : AlgebraicGeometry.Scheme.IdealSheafData.IsMaximalContact (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I 1 H) (S₁ : T.X.left.BlowUpSequence) (hS₁ : S₁.IsOrderSeq (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I T.E 1) (hne : S₁.NoEmptyCenters) (hsnc : ((S₁.exceptionalFamily T.E).append (S₁.strictTransformSeq H (Fin.last S₁.length))).IsSnc) (hT₂ : AlgebraicGeometry.Triple.BDClass N 1 (Fintype.card (S₁.exceptionalFamily T.E).ι) (BO.step22TripleOfSeq T S₁ hS₁ hsnc)) (hpass : T.I.maxOrd = 1 → ∀ (i : ℕ) (hi : i < Fintype.card T.E.ι), Disjoint ↑(S₁.markedTransformSeq T.I 1 (Fin.last S₁.length)).support ↑(S₁.strictTransformSeq (T.E.nth ⟨i, hi⟩) (Fin.last S₁.length)).support) (hcp3 : ∀ (T' : MarkedTriple k) (hT' : Dom k T'), T'.m = 1 → CP3For ((B k).seq T' hT') T'.I T'.E) : CP3For ((BO.step22Functor (fun (m j : ℕ) => BD.bdData N m j Dom B ⋯ hB hsm hbc) 1 (Fintype.card (S₁.exceptionalFamily T.E).ι) ⋯).seq (BO.step22TripleOfSeq T S₁ hS₁ hsnc) hT₂) (S₁.markedTransformSeq T.I 1 (Fin.last S₁.length)) (S₁.totalTransformSeq T.E (Fin.last S₁.length))

CP3 along the re-tuned functor of Lemma 102 at the mark 1 on the Step 2.2 triple of an arbitrary Step 2.1 run S₁, for (I_r, E_r) ([Kol07, 104, Step 2.2]; the proof of [Kol07, Lemma 102]) — given CP3 for the inductive input B at the mark 1 and the passage fact that the transforms of the original members miss V(I_r) when max-ord I = 1.

theorem Hironaka.Resolution.cp3For_step22 {k : Type u} [Field k] [CharZero k] {N : ℕ} (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) σ) (T : AlgebraicGeometry.Triple k) (hn : T.HasDimLE N) (hmax : T.I.maxOrd ≤ 1) {H : T.X.left.IdealSheafData} (hH : AlgebraicGeometry.IsSmoothDivisor H) (hle : AlgebraicGeometry.Scheme.IdealSheafData.IsMaximalContact (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I 1 H) (hcp3 : ∀ (T' : MarkedTriple k) (hT' : Dom k T'), T'.m = 1 → CP3For ((B k).seq T' hT') T'.I T'.E) : CP3For (BO.step22 T hn hmax (fun (m j : ℕ) => BD.bdData N m j Dom B ⋯ hB hsm hbc) ⋯ hH hle) ((↑(BO.step21Seq T hn hmax (fun (j : ℕ) => BD.bdData N 1 j Dom B ⋯ hB hsm hbc) (Fintype.card T.E.ι))).markedTransformSeq T.I 1 (Fin.last (↑(BO.step21Seq T hn hmax (fun (j : ℕ) => BD.bdData N 1 j Dom B ⋯ hB hsm hbc) (Fintype.card T.E.ι))).length)) ((↑(BO.step21Seq T hn hmax (fun (j : ℕ) => BD.bdData N 1 j Dom B ⋯ hB hsm hbc) (Fintype.card T.E.ι))).totalTransformSeq T.E (Fin.last (↑(BO.step21Seq T hn hmax (fun (j : ℕ) => BD.bdData N 1 j Dom B ⋯ hB hsm hbc) (Fintype.card T.E.ι))).length))

CP3 along Step 2.2 ([Kol07, 104, Step 2.2]; the proof of [Kol07, Lemma 102]) with the data bdData, given CP3 for the inductive input B at the mark 1: CP3 along Step 2.2 for (I_r, E_r), E_r the FULL total transform of E.