Nowhere dense subschemes have ideal sheaves nonzero at every point

Hironaka's hypothesis on the algebraic subscheme W ⊆ X in [Hir64, Corollary 3], and on the center of a monoidal transformation, is topological: "the set of points of W is nowhere dense in the underlying topological space of X" (Mathlib's IsNowhereDense). Kollár's triples [Kol07, Definition 31 and Notation 64] and the predicate IsNonzeroEverywhere used in the main theorems ask instead that the ideal sheaf of W be nonzero at every point. On a locally Noetherian scheme the first implies the second (isNonzeroEverywhere_of_isNowhereDense_support): a stalk of the ideal sheaf zero at x gives zero germs of the finitely many local generators, which then vanish on a neighbourhood of x (TopCat.Presheaf.germ_eq), so the ideal sheaf vanishes near x and V(W) has interior. The converse (a nonzero stalk at every point makes the support nowhere dense) is not needed; isNonzeroEverywhere_iff_irreducibleComponents of Hironaka/Scheme/BlowUpSequence/InducedData.lean is the form in terms of irreducible components.

theorem AlgebraicGeometry.isNonzeroEverywhere_of_isNowhereDense_support {X : Scheme} [IsLocallyNoetherian X] (W : X.IdealSheafData) (hW : IsNowhereDense ↑W.support) : W.IsNonzeroEverywhere

On a locally Noetherian scheme, a closed subscheme with nowhere dense underlying set (Hironaka's hypothesis in [Hir64, Corollary 3]) has an ideal sheaf with nonzero stalks (Kollár's convention in [Kol07, Notation 64]): a zero stalk at x kills each of the finitely many local generators on a neighbourhood of x (TopCat.Presheaf.germ_eq), so the ideal sheaf vanishes on a neighbourhood of x, which then lies in the support.