Theorems · Theorem · algebraic geometry

AlgebraicGeometry.RingedSpace.isUnit_of_isUnit_germ

∀ (X : AlgebraicGeometry.RingedSpace) (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace)
  (f : ↑(X.presheaf.obj (Opposite.op U))),
  (∀ (x : ↑↑X.toPresheafedSpace) (hx : x ∈ U),
      IsUnit ((CategoryTheory.ConcreteCategory.hom (X.presheaf.germ U x hx)) f)) →
    IsUnit f

If a section f is a unit in each stalk, f must be a unit.

Defined in

Mathlib.Geometry.RingedSpace.Basic

Cited by

1 results in Mathlib

Foundations

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