The initial state of the loop BED: the irreducible components of Y

The initial state of the loop BED of Hironaka.Resolution.Algebraic.Wlo05.Embedded: the members are the reduced ideals of the irreducible components of Y (componentIdeals), each the vanishing ideal of the closure of a generic point of V(I_Y), at which the reduced I_Y is the maximal ideal (stalkIdeal_eq_maximalIdeal_of_mem_genericPoints_of_isReduced: every prime over the stalk is a generic point specializing to it); the boundary is empty; nothing is protected yet (embeddedStateData_componentIdeals). The support of I_Y is the union of the supports of the members (coe_support_eq_biUnion_componentIdeals).

The clauses of [Wlo05, Theorem 1.0.2] about the final strict transform of Y are derived from the end result of the loop in Hironaka.Resolution.Algebraic.Wlo05.EmbeddedEndBridge, and the proof of the theorem supplies that end result from CP1–CP6 (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCPBridge).

theorem Hironaka.Resolution.stalkIdeal_eq_maximalIdeal_of_mem_genericPoints_of_isReduced {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) [AlgebraicGeometry.IsReduced I.subscheme] {η : ↥X} (hη : η ∈ I.support.genericPoints) : I.stalkIdeal η = IsLocalRing.maximalIdeal ↑(X.presheaf.stalk η)

The stalk of a reduced ideal at a generic point of its support is the maximal ideal: the stalk is radical, and every prime over it contains a minimal prime over it, the stalk of the reduced ideal of the closure of a generic point specializing to η — which is η itself.

theorem Hironaka.Resolution.mem_componentIdeals_iff {k : Type u} [Field k] (TX : AlgebraicGeometry.Triple k) {c : TX.X.left.IdealSheafData} : c ∈ componentIdeals TX ↔ ∃ η ∈ TX.I.support.genericPoints, c = AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})

The members of the initial state are the reduced ideals of the irreducible components of V(I_Y).

theorem Hironaka.Resolution.embeddedStateData_componentIdeals {k : Type u} [Field k] (TX : AlgebraicGeometry.Triple k) (hE : IsEmpty TX.E.ι) [AlgebraicGeometry.IsReduced TX.I.subscheme] : EmbeddedStateData TX.I TX.E (componentIdeals TX) ∅

The invariant of the loop at the start (the components of [Wlo05, Theorem 4.7.1]): the state of the loop for (X, I_Y, ∅) with the irreducible components of Y as members and nothing protected.

theorem Hironaka.Resolution.coe_support_eq_biUnion_componentIdeals {k : Type u} [Field k] (TX : AlgebraicGeometry.Triple k) : ↑TX.I.support = ⋃ c ∈ componentIdeals TX, ↑c.support

The support of I_Y is the union of the supports of its irreducible components.