CP1 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 the strict transform H_r of the hypersurface of maximal contact to the triple (X_r, I_r, F_r + H_r), whose boundary is the EXCEPTIONAL sub-family F_r of the total transform E_r of the original boundary, through the re-tuning at the mark 1 (the identity). The statement CP1 of the embedded desingularization (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedChainRelative) along it for (I_r, E_r) at a generic point η of V(I_r) off E_r: the value is the functor of Lemma 102 at the mark 1 on the Step 2.2 triple (step22Functor_seq_of_maxOrd_eq, functor_seq_congr_mark, dataFunctor_seq_of_maxOrd_eq, functor_seq), the raw output with its empty blow-ups deleted; the core of Step 2.2 (cp1For_rawSeq_of_cp1, Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP1Step22Core) gives CP1 along the raw output for the tuned ideal (which is I_r: W_tuningParam_one, [Kol07, Remark 67]) and the family (F_r + H_r) − H_r; cp1For_eraseEmpty deletes the empty blow-ups; and the family bridge cp1For_of_embeds (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP1Subfamily) passes to E_r, since the members of E_r missing from F_r are the birational transforms of the original members, which miss V(I_r) at the end of Step 2.1 (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedStep21Passage) and hence miss c̃ at every later stage (the lifted generic point). Used in Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP1Step2.

theorem Hironaka.Resolution.cp1For_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 : ∀ (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) (hcp1 : ∀ (T' : MarkedTriple k) (hT' : Dom k T'), T'.m = 1 → ∀ η' ∈ T'.I.support.genericPoints, (∀ (i : T'.E.ι), η' ∉ (T'.E.component i).support) → T'.I.stalkIdeal η' = (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η'})).stalkIdeal η' → CP1For ((B k).seq T' hT') T'.I T'.E η') {η : ↥(S₁.stage (Fin.last S₁.length))} (hη : η ∈ (S₁.markedTransformSeq T.I 1 (Fin.last S₁.length)).support.genericPoints) (hηE : ∀ (i : (S₁.totalTransformSeq T.E (Fin.last S₁.length)).ι), η ∉ ((S₁.totalTransformSeq T.E (Fin.last S₁.length)).component i).support) (hIc : (S₁.markedTransformSeq T.I 1 (Fin.last S₁.length)).stalkIdeal η = (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})).stalkIdeal η) : CP1For ((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)) η

CP1 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) at a generic point η of V(I_r) off E_r — given CP1 for the inductive input B at the mark 1 and the fact that the transforms of the original members miss V(I_r).

theorem Hironaka.Resolution.cp1For_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) (hcp1 : ∀ (T' : MarkedTriple k) (hT' : Dom k T'), T'.m = 1 → ∀ η' ∈ T'.I.support.genericPoints, (∀ (i : T'.E.ι), η' ∉ (T'.E.component i).support) → T'.I.stalkIdeal η' = (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η'})).stalkIdeal η' → CP1For ((B k).seq T' hT') T'.I T'.E η') {η : ↥((↑(BO.step21Seq T hn hmax (fun (j : ℕ) => BD.bdData N 1 j Dom B ⋯ hB hsm hbc) (Fintype.card T.E.ι))).stage (Fin.last (↑(BO.step21Seq T hn hmax (fun (j : ℕ) => BD.bdData N 1 j Dom B ⋯ hB hsm hbc) (Fintype.card T.E.ι))).length))} (hη : η ∈ ((↑(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)).support.genericPoints) (hηE : ∀ (i : ((↑(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)).ι), η ∉ (((↑(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)).component i).support) (hIc : ((↑(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)).stalkIdeal η = (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})).stalkIdeal η) : CP1For (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)) η

CP1 along Step 2.2 ([Kol07, 104, Step 2.2]; the proof of [Kol07, Lemma 102]) with the data bdData, given CP1 for the inductive input B at the mark 1 (hcp1): for a point η of the input of Step 2.2 — a generic point of V(I_r) off the boundary E_r (the FULL total transform of E) with I_r the reduced ideal of its closure there — CP1 holds along Step 2.2 for (I_r, E_r).