The chain form when the centre is the component itself #
The case of the statement CP1 of the embedded desingularization
(Hironaka.Resolution.Algebraic.Wlo05.EmbeddedChainRelative) in which the absorbing centre is the
strict transform c̃ of the reduced component itself (Step 2 of the proof of [Kol07, Theorem 107]:
the centre of the round of order 1 is the cosupport of the nonmonomial part): a smooth
hypersurface Γ having simple normal crossings with the boundary E and contained in no member of
E, with J ⊆ Γ and the nonmonomial part N(J) of order ≤ 1 along Γ. Then at every point p
of Γ the ideal J is in chain form along Γ with the chain Γ's own coordinates and unit level
monomials: J_p = M(J)_p · Γ_p (chainRelativeAt_of_le_isSmoothDivisor).
The proof is local algebra in the regular local ring 𝒪_{X,p}. HasSncWith provides coordinates
with Γ_p = (z_j : j ∈ s); NotContainedInMembers puts no member's coordinate in s, so the
enumeration of s is a chain avoiding the members; the splitting J = N(J) · M(J) with M(J)_p a
monomial in the members' coordinates, coprime to the prime Γ_p, gives N(J)_p ⊆ Γ_p; and the
ring lemma eq_span_singleton_of_le_of_exists_notMem_sq (Γ_p principal, N(J)_p ⊄ 𝔪² from
ord_p N(J) ≤ 1) gives N(J)_p = Γ_p. The monomial part is restored by
chainRelativeAt_mul_monomial. Used in Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP1Step22Core.
The chain form when the centre is the component itself: on X smooth over k with E snc, a
smooth divisor Γ having snc with E and contained in no member of E near its points, with
J ≤ Γ and the nonmonomial part of J of order ≤ 1 at the points of Γ, carries the chain form
of J at every point of Γ: J_p = M(J)_p · Γ_p, the chain being Γ's own coordinates with unit
level monomials.