The dictionary, continued: generic points, reduced ideals of components, and nonvanishing

General facts on a scheme X about the reduced ideal vanishingIdeal (closure {η}) of an irreducible component with generic point η: its stalk is the unit ideal off the closure (stalkIdeal_vanishingIdeal_closure_eq_top_of_not_specializes) and the maximal ideal at η (stalkIdeal_vanishingIdeal_closure_self); η is a generic point of its support; a point of a closed set lies on one of its components (exists_genericPoint_specializes). Further, the stalk of a finprod of ideal sheaves (stalkIdeal_finprod_mem); two facts about a divisor family that need only the family (Snc.genericPoints_component_finite, the one-line corollary of Closeds.genericPoints_finite; Snc.finprod_stalk_eq_one_of_notMem, the product over the components of a member is the unit ideal off the member; DivisorFamily.mem_support_iff_exists); and three generalities on IsNonzeroEverywhere, the condition that an ideal sheaf be nonzero on every irreducible component in the sense of [Kol07, Definition 31]: overideals of a nonvanishing ideal sheaf are nonvanishing, a nonvanishing ideal sheaf has finite order (Krull's intersection theorem), an invertible ideal sheaf is nonvanishing.

These lemmas serve the splitting of an ideal into its monomial and nonmonomial parts along a simple normal crossing divisor [Kol07, Definition–Lemma 110], in the marked order reduction.

Generic points and the reduced ideal of a component

theorem Hironaka.BMO.stalkIdeal_vanishingIdeal_closure_eq_top_of_not_specializes {X : AlgebraicGeometry.Scheme} {η x : ↥X} (h : ¬η ⤳ x) : (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})).stalkIdeal x = ⊤

The reduced ideal of a component not through x has the unit stalk at x.

theorem Hironaka.BMO.exists_genericPoint_specializes {X : AlgebraicGeometry.Scheme} (Z : TopologicalSpace.Closeds ↥X) {x : ↥X} (hx : x ∈ Z) : ∃ η ∈ Z.genericPoints, η ⤳ x

A point of a closed set lies on one of its irreducible components (Closeds.exists_mem_genericPoints_specializes).

theorem Hironaka.BMO.stalkIdeal_finprod_mem {X : AlgebraicGeometry.Scheme} {s : Set ↥X} (hs : s.Finite) (g : ↥X → X.IdealSheafData) (x : ↥X) : (∏ᶠ (η : ↥X) (_ : η ∈ s), g η).stalkIdeal x = ∏ᶠ (η : ↥X) (_ : η ∈ s), (g η).stalkIdeal x

The stalk of a finprod over a finite set of ideal sheaves is the finprod of the stalks.

theorem Hironaka.BMO.stalkIdeal_vanishingIdeal_closure_self {X : AlgebraicGeometry.Scheme} (η : ↥X) : (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})).stalkIdeal η = IsLocalRing.maximalIdeal ↑(X.presheaf.stalk η)

The reduced ideal of the closure of a point has, at that point, the maximal ideal as its stalk (stalkIdeal_vanishingIdeal_closure_singleton and the localization at the prime of the point).

theorem Hironaka.BMO.isGenericPoint_support_vanishingIdeal_closure {X : AlgebraicGeometry.Scheme} (η : ↥X) : IsGenericPoint η ↑(AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})).support

The generic point of a component is a generic point of the component's support.

IsNonzeroEverywhere

theorem Hironaka.BMO.isNonzeroEverywhere_of_le {X : AlgebraicGeometry.Scheme} {I J : X.IdealSheafData} (hle : I ≤ J) (hI : I.IsNonzeroEverywhere) : J.IsNonzeroEverywhere

A nonvanishing ideal sheaf's overideals are nonvanishing.

theorem Hironaka.BMO.ord_ne_top_of_isNonzeroEverywhere {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsLocallyNoetherian X] {J : X.IdealSheafData} (hJ : J.IsNonzeroEverywhere) (x : ↥X) : J.ord x ≠ ⊤

The order of a nonvanishing ideal sheaf is finite (Krull's intersection theorem: a nonzero ideal of a Noetherian local ring lies in no 𝔪^r for r large).

theorem Hironaka.BMO.isNonzeroEverywhere_of_isInvertible {X : AlgebraicGeometry.Scheme} {K : X.IdealSheafData} (hK : K.IsInvertible) : K.IsNonzeroEverywhere

An invertible ideal sheaf is nonzero at every point.

A divisor family: finitely many components, the inner product off a member

theorem Hironaka.BMO.Snc.genericPoints_component_finite {X : AlgebraicGeometry.Scheme} (E : X.DivisorFamily) [TopologicalSpace.NoetherianSpace ↥X] (i : E.ι) : (E.component i).support.genericPoints.Finite

The generic points of a member's support are finitely many on a Noetherian scheme (Closeds.genericPoints_finite).

theorem Hironaka.BMO.Snc.finprod_stalk_eq_one_of_notMem {X : AlgebraicGeometry.Scheme} (E : X.DivisorFamily) {i : E.ι} {x : ↥X} (hx : x ∉ (E.component i).support) (a : ↥X → ℕ) : ∏ᶠ (η : ↥X) (_ : η ∈ (E.component i).support.genericPoints), (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})).stalkIdeal x ^ a η = 1

At a point off E^i the product over the components of E^i of powers of their reduced stalks is the unit ideal.

theorem AlgebraicGeometry.Scheme.DivisorFamily.mem_support_iff_exists {X : Scheme} (E : X.DivisorFamily) (x : ↥X) : x ∈ E.support ↔ ∃ (i : E.ι), x ∈ (E.component i).support

A point lies in the support of a divisor family iff it lies on one of the members.