The isolated ideal has the K-shape

The scheme form of the statement CP2 of the embedded desingularization (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedChainRelative): on a scheme smooth over k (locally Noetherian, with regular local stalks), if I is chain-relative monomial along Γ at p (ChainRelativeAt), then the colon I : Γ has the K-shape along Γ at p (ChainRelativeKAt). The stalk of the colon is the colon of the stalks on a locally Noetherian scheme (stalkIdeal_colon_of_isLocallyNoetherian), and in the regular local stalk the colon of the chain ideal by the chain is the K-shape (chainIdeal_colon_span_eq', Hironaka.Resolution.Algebraic.Wlo05.ChainIdealColonRegular). This is what the isolation of the loop (isolatedTriple, Hironaka.Resolution.Algebraic.Wlo05.Embedded: the colon by the reduced ideal of the absorbed strict transforms, which is Γ's ideal near Γ by CP1) produces at the entry into the protected state (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP2Entry).

theorem Hironaka.Resolution.ChainCoords.apply_eq_zero_of_mem_range {X : AlgebraicGeometry.Scheme} {E : X.DivisorFamily} {Γ : X.IdealSheafData} {p : ↥X} {n : ℕ} {z : Fin n → ↑(X.presheaf.stalk p)} {c : { j : E.ι // p ∈ (E.component j).support } → Fin n} {r : ℕ} {σ : Fin (r + 1) → Fin n} {a : Fin (r + 1) → Fin n → ℕ} (h : ChainCoords E Γ p z c σ a) (i : Fin (r + 1)) (k : Fin n) (hk : k ∈ Set.range σ) : a i k = 0

The exponent vectors of chain coordinates vanish on the chain's own coordinates.

theorem Hironaka.Resolution.chainRelativeKAt_colon {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.Smooth f] {E : X.DivisorFamily} {I Γ : X.IdealSheafData} {p : ↥X} (h : ChainRelativeAt E I Γ p) : ChainRelativeKAt E (I.colon Γ) Γ p

CP2 on the scheme: on a scheme smooth over k, the colon by Γ of an ideal chain-relative monomial along Γ at p has the K-shape along Γ at p.