The core of Step 2.2: CP1 along the raw output of Lemma 102

[Kol07, Lemma 102] on a triple (X, I, E) with a member H = E^j of maximal contact for (I, 1) blows up Z_{-1}, the components of H along which I has order ≥ 1, and pushes forward the inductive run on the strict transform of H. For the reduced component c̄ ⊆ V(I) ⊆ H of a generic point η of V(I) off the other members, the statement CP1 of the embedded desingularization (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedChainRelative) along this raw output for (I, E − E^j) follows from CP1 for the inductive run (the hypothesis hcp1, the stage below):

• Case A: Z_{-1} contains c̃. Then c̄ is a component of H (mem_genericPoints_of_Zminus1_le), a smooth divisor with the stalks of H (isSmoothDivisor_vanishingIdeal_closure_of_mem_genericPoints, stalkIdeal_vanishingIdeal_closure_eq_of_isSmoothDivisor), and chainRelativeAt_of_le_isSmoothDivisor (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedChainCaseA) gives the chain form at the first stage; later stages are excluded by the stop rule.
• Case B: the first blow-up does not contain c̃. On H the run is cons (Z_{-1}|_H) (B …), its first blow-up does not contain the level component (cp1For_cons_of_not_centerContains), and hcp1 on the restricted triple, whose ideal and boundary are exactly the level data after the first blow-up, gives CP1 for the tail; cp1For_pushforward (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP1Pushforward) carries it to X.

This is Step 2.2 of the proof of [Kol07, Theorem 103] read for CP1; the argument is not in the literature. Used in Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP1Step22.

theorem Hironaka.Resolution.cp1For_rawSeq_of_cp1 {k : Type u} [Field k] [CharZero k] {n : ℕ} {Dom : MarkedTriple k → Prop} (B : OrderGeSeqAssignment k Dom) (T : AlgebraicGeometry.Triple k) (m : ℕ) (hm1 : m = 1) (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') (hcp1 : ∀ (T' : MarkedTriple k) (hT' : Dom 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.seq T' hT') T'.I T'.E η') (hH : AlgebraicGeometry.IsSmoothDivisor (T.E.component j)) (hHJ : T.E.component j ≤ T.I) {η : ↥T.X.left} (hη : η ∈ T.I.support.genericPoints) (hηE : ∀ (i : (T.E.erase j).ι), η ∉ ((T.E.erase j).component i).support) (hIc : T.I.stalkIdeal η = (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})).stalkIdeal η) : CP1For (BD.rawSeq T m j hI hmax hn B hDom) T.I (T.E.erase j) η

The core of Step 2.2 (the proof of [Kol07, Lemma 102] read for CP1): for a triple (X, I, E) with max-ord I = m = 1, a member H = E^j that is a smooth hypersurface with H ⊆ V(I), and a generic point η of V(I) off the other members with I_η its reduced ideal, the raw output of Lemma 102 satisfies CP1 for (I, E − E^j) at η, given CP1 for the inductive run B at the mark 1.