The initial invariant of a smooth Y

For a smooth reduced Y = V(I) in a triple (X, I, ∅), the loop's initial state (X, I, componentIdeals) satisfies the invariant of Hironaka.Resolution.Algebraic.Wlo05.EmbeddedNilInvariant (invariant_componentIdeals): the components of Y — the reduced ideals of the closures of the generic points of supp I — have pairwise disjoint supports and multiply to I (prod_componentFamily_eq, pairwise_disjoint_support_componentFamily, for the regular Y: isRegular_of_smooth), and I is regular stalkwise (isRegularLocalRing_quotient_stalkIdeal). The loop's member set is the image of the component family's index type (componentIdeals_eq_image_univ; the component map is injective on the generic points since a generic point is determined by its closure).

Given the core lemma, the empty succession follows: BED(X, I_Y, ∅) has length 0 (length_bedAux_eq_zero_of_invariant), hence is the empty succession (bed_eq_nil_of_smooth_of_core); the core lemma is proved in Hironaka.Resolution.Algebraic.Wlo05.EmbeddedNilCore.

theorem Hironaka.Resolution.componentIdeals_eq_image_univ {k : Type u} [Field k] (T : AlgebraicGeometry.Triple k) [TopologicalSpace.NoetherianSpace ↥T.X.left] : componentIdeals T = Finset.image T.I.componentFamily.component Finset.univ

The loop's member set is the image of the component family's index type.

theorem Hironaka.Resolution.componentFamily_component_injective {k : Type u} [Field k] (T : AlgebraicGeometry.Triple k) [TopologicalSpace.NoetherianSpace ↥T.X.left] : Function.Injective T.I.componentFamily.component

The component map is injective on the generic points: a generic point is determined by the support of its component (its closure).

theorem Hironaka.Resolution.prod_componentIdeals_eq {k : Type u} [Field k] (T : AlgebraicGeometry.Triple k) [TopologicalSpace.NoetherianSpace ↥T.X.left] (hZ : AlgebraicGeometry.IsRegular T.I.subscheme) : ∏ c ∈ componentIdeals T, c = T.I

For a regular Y = V(I) the product of the loop's members is I (prod_componentFamily_eq).

theorem Hironaka.Resolution.pairwise_disjoint_componentIdeals {k : Type u} [Field k] (T : AlgebraicGeometry.Triple k) [TopologicalSpace.NoetherianSpace ↥T.X.left] (hZ : AlgebraicGeometry.IsRegular T.I.subscheme) : (↑(componentIdeals T)).Pairwise fun (a b : T.X.left.IdealSheafData) => Disjoint a.support b.support

For a regular Y = V(I) the loop's members have pairwise disjoint supports (pairwise_disjoint_support_componentFamily).

theorem Hironaka.Resolution.invariant_componentIdeals {k : Type u} [Field k] [CharZero k] (T : AlgebraicGeometry.Triple k) (hE : IsEmpty T.E.ι) (hY : AlgebraicGeometry.Smooth (CategoryTheory.CategoryStruct.comp T.I.subschemeι (T.X.left ↘ AlgebraicGeometry.Spec ↧k))) : Invariant T.I T.E (componentIdeals T)

The initial invariant — for a smooth Y = V(I) in a triple with empty boundary, the loop's initial state (X, I, componentIdeals) satisfies the invariant.

theorem Hironaka.Resolution.bed_eq_nil_of_smooth_of_core {k : Type u} [Field k] [CharZero k] (hcore : Core k) (TX : AlgebraicGeometry.Triple k) (hE : IsEmpty TX.E.ι) (hY : AlgebraicGeometry.Smooth (CategoryTheory.CategoryStruct.comp TX.I.subschemeι (TX.X.left ↘ AlgebraicGeometry.Spec ↧k))) : BED TX = AlgebraicGeometry.Scheme.BlowUpSequence.nil TX.X.left

The empty succession given the core lemma — for a smooth reduced Y the embedded desingularization sequence BED(X, I_Y, ∅) is the empty succession ([Wlo05, 4.6]: at a smooth point of Y the invariant is terminal).