Theorems · Theorem · algebraic geometry

AlgebraicGeometry.RingedSpace.exists_res_eq_zero_of_germ_eq_zero

∀ (X : AlgebraicGeometry.RingedSpace) (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace)
  (f : ↑(X.presheaf.obj (Opposite.op U))) (x : ↥U),
  (CategoryTheory.ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) f = 0 →
    ∃ V i, ∃ (_ : ↑x ∈ V), (CategoryTheory.ConcreteCategory.hom (X.presheaf.map i.op)) f = 0

If the germ of a section f is zero in the stalk at x, then f is zero on some neighbourhood around x.

Defined in

Mathlib.Geometry.RingedSpace.Basic

Cited by

1 results in Mathlib

Foundations

Depth 75 from the axioms · uses propext, Classical.choice, Quot.sound