CP3 along the raw output of Lemma 102 over a member

[Kol07, Lemma 102] on a triple (X, I, E) with max-ord I = 1 and a member Eʲ: blow up Z₋₁, the union of the components of Eʲ inside V(I), then push forward the inductive run on the strict transform of Eʲ (rawSeq, Hironaka.Resolution.Algebraic.BoundaryClearing.Restriction). For the statement CP3 of the embedded desingularization (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedChainRelative) its centres are classified at every point for the outer data (I, E) from the inductive classification:

• at a point q of Z₋₁ (stage 0; map_centerS) the stalk of the centre is the stalk of Eʲ (stalkIdeal_Zminus1_eq), the coordinate z (c j) of the member — the stratum of level 0 with s = {c j}, whose admissibility condition (★) b (c j) ≠ 0 is the order of I at the generic point of the component of Eʲ through q, which is 1 because that component lies in Z₋₁ (mem_support_Zminus1_iff_ord_eq) — read through the exponent identity toNat_ord_eq_of_stalkIdeal_eq_span_mul for either shape;
• at a point of a later centre — the push-forward of a centre of the inductive run along the stage inclusion g (center_pushforward_mk, support_map) — the identities of [Kol07, Lemma 62] read the outer boundary E − Eʲ and the outer marked transform on the strict transform of Eʲ as the data of the inductive run (pullback_pushforward, pullbackStageHom_pushforward_heq_mk, totalTransformSeq_comap_pullbackStageHom_of_forall_lt with (E − Eʲ) + Eʲ snc, IsOrderGeSeq.markedTransformSeq_comap_pullbackStageHom_mk); the total transform of E − Eʲ embeds in that of E with the transform of Eʲ as the only member outside the range (exists_embeds_totalTransformSeq, component_originalIdx = the kernel of g); the family of the inductive run is snc (isSnc_restrictedFamily) and its marked ideal nonzero (isNonzeroEverywhere_markedTransformSeq); and the pointwise pass centerClassifiedAt_of_comap_member (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP3Pass) lifts the inductive classification.

No smoothness of Eʲ and no inclusion Eʲ ≤ I is assumed: the passes of Step 2.1 of the proof of [Kol07, Theorem 103] have neither. This argument is not in the literature. Used in Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP3Step21 and Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP3Step22.

theorem Hironaka.Resolution.cp3For_rawSeq_member {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) : CP3For (BD.rawSeq T 1 j hI hmax hn B' hDom') T.I T.E

CP3 along the raw output of Lemma 102 over a member Eʲ for the outer data (I, E), from CP3 for the values of the inductive functor B' at the mark 1 ([Kol07, Lemma 102] and [Kol07, Lemma 62]): at a point of Z₋₁ the stratum of level 0 given by the coordinate of Eʲ; at a point of a later centre the pointwise pass centerClassifiedAt_of_comap_member on the stage inclusion, with the identities of Lemma 62.