The dictionary, continued: components of a regular closed subscheme

General facts about a closed subscheme Z of a scheme X with IsRegular Z.subscheme, without a structure morphism: its stalk ideal at a point of it is prime (Hironaka.Sequence.isPrime_stalkIdeal_of_isRegular); the reduced ideal of the component through x has the subscheme's stalk (stalkIdeal_vanishingIdeal_closure_eq_of_isRegular_subscheme); the finprod over the components of the powers of their reduced stalks is the power of the stalk at the exponent of the one component through x (finprod_stalk_eq_of_specializes_of_isRegular_subscheme); two components through a common point coincide (Hironaka.Sequence.eq_of_specializes_of_isRegular); and, for a simple normal crossing family [Kol07, Definition 24] with a regular stalk at a generic point η of a component of E^i, no other member passes through η (notMem_support_of_ne_of_isSnc).

These lemmas serve the monomial part of an ideal along a simple normal crossing divisor and the combinatorics of its components (Hironaka/Resolution/Algebraic/Monomial/, Hironaka/Resolution/Algebraic/MarkedOrderReduction/), whose modules import this one and whose namespace Hironaka.Monomial the declarations carry; their forms for a scheme smooth over a field are in Hironaka/Resolution/Algebraic/Snc/ComponentStalks.lean.

theorem Hironaka.Monomial.stalkIdeal_vanishingIdeal_closure_eq_of_isRegular_subscheme {X : AlgebraicGeometry.Scheme} {D : X.IdealSheafData} (hD : AlgebraicGeometry.IsRegular D.subscheme) {η x : ↥X} (hη : η ∈ D.support.genericPoints) (hηx : η ⤳ x) : (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})).stalkIdeal x = D.stalkIdeal x

The reduced ideal of the component through x of a member with a regular subscheme has the member's stalk at x: it is a minimal prime over the member's stalk, which is prime (Hironaka.Sequence.isPrime_stalkIdeal_of_isRegular). The general form of Snc.stalkIdeal_vanishingIdeal_closure_eq_of_specializes, whose smooth form is a corollary.

theorem Hironaka.Monomial.finprod_stalk_eq_of_specializes_of_isRegular_subscheme {X : AlgebraicGeometry.Scheme} {D : X.IdealSheafData} (hD : AlgebraicGeometry.IsRegular D.subscheme) {η₀ x : ↥X} (hη₀ : η₀ ∈ D.support.genericPoints) (h₀ : η₀ ⤳ x) (a : ↥X → ℕ) : ∏ᶠ (η : ↥X) (_ : η ∈ D.support.genericPoints), (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})).stalkIdeal x ^ a η = D.stalkIdeal x ^ a η₀

At a point x of a member with a regular subscheme, the product over the member's components of the powers of their reduced stalks is the power of the member's stalk at the exponent of the one component through x: two components through x coincide, their reduced stalks both being the member's. The general form of Snc.finprod_stalk_eq_of_specializes.

theorem Hironaka.Monomial.notMem_support_of_ne_of_isSnc {X : AlgebraicGeometry.Scheme} {E : X.DivisorFamily} (hE : E.IsSnc) {i j : E.ι} (hji : j ≠ i) {η : ↥X} (hreg : IsRegularLocalRing ↑(X.presheaf.stalk η)) (hη : η ∈ (E.component i).support.genericPoints) : η ∉ (E.component j).support

No member other than E^j passes through a generic point η of a component of E^j when the stalk at η is regular: 𝔪_η = (E^j)_η = (z_c) and another member would have (z_{c'}) ⊆ (z_c) with c' ≠ c. The general form of Snc.notMem_support_of_ne, whose smooth form is a corollary.