The reduced closure of a point: members, smooth divisors, Z_{-1}

Elementary tools about c̄ := V(closure {η}), the reduced closure of a point η, for the proof of the statement CP1 of the embedded desingularization (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedChainRelative): the chain form depends on the stratum only through its stalk (chainRelativeAt_congr_stalkIdeal); when η lies on no member of E, no member contains c̄ near any of its points (notContainedInMembers_vanishingIdeal_closure — a containment of stalks at x would put η, which specialises to x, on the member); a smooth divisor H is locally irreducible, so at a point of the closure of one of its generic points ξ the reduced ideal of that closure is H's own stalk and the closure is a smooth divisor (stalkIdeal_vanishingIdeal_closure_eq_of_isSmoothDivisor, isSmoothDivisor_vanishingIdeal_closure_of_mem_genericPoints); and when the subscheme Z_{-1}(I, 1, H) of the proof of [Kol07, Lemma 102] (the components of H along which I has order ≥ 1) contains c̄ for a generic point η of V(I), η is a generic point of H (mem_genericPoints_of_Zminus1_le). Used in Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP1Step22Core, Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP1Absorbed, Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP1Cover and the EmbeddedCP3* modules.

theorem Hironaka.Resolution.chainRelativeAt_congr_stalkIdeal {X : AlgebraicGeometry.Scheme} {E : X.DivisorFamily} {I Γ Γ' : X.IdealSheafData} {p : ↥X} (h : Γ.stalkIdeal p = Γ'.stalkIdeal p) : ChainRelativeAt E I Γ p ↔ ChainRelativeAt E I Γ' p

The chain form depends on Γ only through its stalk at p.

theorem Hironaka.Resolution.notContainedInMembers_vanishingIdeal_closure {X : AlgebraicGeometry.Scheme} (E : X.DivisorFamily) {η : ↥X} (hη : ∀ (j : E.ι), η ∉ (E.component j).support) : NotContainedInMembers E (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η}))

The closure of a point lying on no member of E is contained in no member of E near any of its points (the last sentence of [Kol07, Definition 24] for the reduced closure of a point): E^j_x ⊆ I(c̄)_x would give E^j_η ⊆ I(c̄)_η = 𝔪_η at the generic point η, which specialises to x.

theorem Hironaka.Resolution.stalkIdeal_vanishingIdeal_closure_eq_of_isSmoothDivisor {X : AlgebraicGeometry.Scheme} {H : X.IdealSheafData} (hH : AlgebraicGeometry.IsSmoothDivisor H) {ξ x : ↥X} (hξ : ξ ∈ H.support.genericPoints) (hx : ξ ⤳ x) : (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {ξ})).stalkIdeal x = H.stalkIdeal x

A smooth divisor is locally irreducible — at a point x of the closure of one of its generic points ξ, the reduced ideal of that closure is the divisor's own stalk: H_x is prime (𝒪_{X,x} / H_x is regular, hence a domain) and I(closure ξ)_x is a minimal prime over it.

theorem Hironaka.Resolution.isSmoothDivisor_vanishingIdeal_closure_of_mem_genericPoints {X : AlgebraicGeometry.Scheme} {H : X.IdealSheafData} (hH : AlgebraicGeometry.IsSmoothDivisor H) {ξ : ↥X} (hξ : ξ ∈ H.support.genericPoints) : AlgebraicGeometry.IsSmoothDivisor (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {ξ}))

The component of a smooth divisor through one of its generic points is a smooth divisor — its stalks are the divisor's.

theorem Hironaka.Resolution.mem_genericPoints_of_Zminus1_le {X : AlgebraicGeometry.Scheme} [TopologicalSpace.NoetherianSpace ↥X] (I H : X.IdealSheafData) {η : ↥X} (hη : η ∈ I.support.genericPoints) (hle : BD.Zminus1 I 1 H ≤ AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})) : η ∈ H.support.genericPoints

When Z_{-1}(I, 1, H) (the proof of [Kol07, Lemma 102]) contains the closure of a generic point η of V(I), that closure is a component of H — η lies on Z_{-1}, so under a generic point ξ of H with ord_ξ I ≥ 1; ξ ∈ V(I) specialises to the generic point η, so ξ = η.