The absorbed strict transform and the members of the boundary

Two facts about the position of an absorbed strict transform c̃ relative to the boundary E_n at the absorbing stage n of a run of BMO_1, both needed for the isolation of the absorbed component in the loop BED (Hironaka.Resolution.Algebraic.Wlo05.Embedded; the isolation passage of the proof of [Wlo05, Theorem 4.7.1]).

• No member of the boundary contains c̃ near any of its points (notContainedInMembers_strictTransformSeq_of_absorbed): the generic point of c̃ lies on no member (the proof of [Kol07, Corollary 22], exists_genericPoint_strictTransformSeq_of_absorbed of Hironaka.Resolution.Algebraic.Wlo05.EmbeddedAbsorbed), and a containment near a point would specialise to it. This is unconditional.
• The generic point of an irreducible component of a member does not lie on c̃ (notMem_strictTransformSeq_support_of_mem_genericPoints_component): at such a point the stalk of the member is the maximal ideal, generated by one of the snc coordinates; the stalk of c̃ there is generated by other coordinates (the first point), yet lies in the maximal ideal, which contradicts the independence of a regular system of parameters unless it is the zero ideal, and the marked ideal (nonzero everywhere, contained in the centre, which equals c̃ near c̃) forbids that. The equality of the centre and c̃ used here is the CONDITIONAL stalkIdeal_center_eq_of_absorbed, so this lemma assumes ClaimKC (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedHypotheses), which is false for the transcribed order; the unconditional treatment of the isolated state is Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP2Entry. The second point is what makes the colon by c̃ invisible to the monomial part: the exponents of M(I_n) are the orders at these generic points, where the colon changes nothing.

Simple normal crossings and the total transform are those of [Kol07, Definition 24] and [Kol07, Definition 25]. Used in Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP1Step22Core, Hironaka.Resolution.Algebraic.Wlo05.EmbeddedIsolatedState and Hironaka.Resolution.Algebraic.Wlo05.EmbeddedIsolatedIdeal.

theorem Hironaka.Resolution.hasSncWith_component_of_isSnc {X : AlgebraicGeometry.Scheme} {E : X.DivisorFamily} (hE : E.IsSnc) (i : E.ι) : E.HasSncWith (E.component i)

[Kol07, Definition 24 (4)] for a member of an snc family itself: a member has simple normal crossings with the family (its stalk at a point through which it passes is generated by one of the snc coordinates).

theorem Hironaka.Resolution.notContainedInMembers_strictTransformSeq_of_absorbed {k : Type u} [Field k] [CharZero k] (T : MarkedTriple k) (hm : T.m = 1) {η : ↥T.X.left} (hηE : ∀ (i : T.E.ι), η ∉ (T.E.component i).support) (n : Fin (bmoOneRun T hm).length) (hfirst : ∀ m < ↑n, ¬CenterContains (bmoOneRun T hm) (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})) m) : NotContainedInMembers ((bmoOneRun T hm).totalTransformSeq T.E n.castSucc) ((bmoOneRun T hm).strictTransformSeq (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})) n.castSucc)

No member of the boundary at stage n contains c̃ near any of its points (the last sentence of [Kol07, Definition 24] for the absorbed strict transform): the generic point of c̃ lies on no member (exists_genericPoint_strictTransformSeq_of_absorbed), and a containment of stalks at a point of c̃ would generize to it.

theorem Hironaka.Resolution.notMem_strictTransformSeq_support_of_mem_genericPoints_component {k : Type u} [Field k] [CharZero k] (T : MarkedTriple k) (hm : T.m = 1) {η : ↥T.X.left} (hη : η ∈ T.I.support.genericPoints) (hηE : ∀ (i : T.E.ι), η ∉ (T.E.component i).support) (hIc : T.I.stalkIdeal η = (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})).stalkIdeal η) (n : Fin (bmoOneRun T hm).length) (habs : CenterContains (bmoOneRun T hm) (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})) ↑n) (hfirst : ∀ m < ↑n, ¬CenterContains (bmoOneRun T hm) (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})) m) (hKC : ClaimKC k) (i : ((bmoOneRun T hm).totalTransformSeq T.E n.castSucc).ι) {ζ : ↥((bmoOneRun T hm).stage n.castSucc)} (hζ : ζ ∈ (((bmoOneRun T hm).totalTransformSeq T.E n.castSucc).component i).support.genericPoints) : ζ ∉ ((bmoOneRun T hm).strictTransformSeq (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})) n.castSucc).support

The generic point of an irreducible component of a member of the boundary at stage n does not lie on the absorbed strict transform c̃ — conditional on ClaimKC, which is false for the transcribed order (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedHypotheses). At such a point ζ the stalk of the member is the maximal ideal (stalkIdeal_eq_maximalIdeal_of_mem_genericPoints), generated by one snc coordinate z_c; if ζ ∈ c̃, then the stalk of c̃ is (z_j : j ∈ s) with c ∉ s (notContainedInMembers_strictTransformSeq_of_absorbed) and s ≠ ∅ (the marked ideal is nonzero at ζ and lies in the centre, whose stalk is that of c̃ by stalkIdeal_center_eq_of_absorbed), so some z_j with j ≠ c lies in (z_c), impossible for a regular system of parameters.