mathlib3 documentation

algebraic_geometry.ringed_space

Ringed spaces #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We introduce the category of ringed spaces, as an alias for SheafedSpace CommRing.

The facts collected in this file are typically stated for locally ringed spaces, but never actually make use of the locality of stalks. See for instance https://stacks.math.columbia.edu/tag/01HZ.

source
@[reducible]
def algebraic_geometry.RingedSpace  :
Type (u_1+1)

The type of Ringed spaces, as an abbreviation for SheafedSpace CommRing.

source
theorem algebraic_geometry.RingedSpace.is_unit_res_of_is_unit_germ (X : algebraic_geometry.RingedSpace) (U : topological_space.opens ↥X) (f : ↥(X.to_PresheafedSpace.presheaf.obj (opposite.op U))) (x : ↥U) (h : is_unit (⇑(X.to_PresheafedSpace.presheaf.germ x) f)) :
∃ (V : topological_space.opens ↥X) (i : V ⟶ U) (hxV : x.val ∈ V), is_unit (⇑(X.to_PresheafedSpace.presheaf.map i.op) f)

If the germ of a section f is a unit in the stalk at x, then f must be a unit on some small neighborhood around x.

source
theorem algebraic_geometry.RingedSpace.is_unit_of_is_unit_germ (X : algebraic_geometry.RingedSpace) (U : topological_space.opens ↥X) (f : ↥(X.to_PresheafedSpace.presheaf.obj (opposite.op U))) (h : ∀ (x : ↥U), is_unit (⇑(X.to_PresheafedSpace.presheaf.germ x) f)) :
is_unit f

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

source
def algebraic_geometry.RingedSpace.basic_open (X : algebraic_geometry.RingedSpace) {U : topological_space.opens ↥X} (f : ↥(X.to_PresheafedSpace.presheaf.obj (opposite.op U))) :
topological_space.opens ↥X

The basic open of a section f is the set of all points x, such that the germ of f at x is a unit.

Equations
source
@[simp]
theorem algebraic_geometry.RingedSpace.mem_basic_open (X : algebraic_geometry.RingedSpace) {U : topological_space.opens ↥X} (f : ↥(X.to_PresheafedSpace.presheaf.obj (opposite.op U))) (x : ↥U) :
↑x ∈ X.basic_open f ↔ is_unit (⇑(X.to_PresheafedSpace.presheaf.germ x) f)
source
@[simp]
theorem algebraic_geometry.RingedSpace.mem_top_basic_open (X : algebraic_geometry.RingedSpace) (f : ↥(X.to_PresheafedSpace.presheaf.obj (opposite.op ⊤))) (x : ↥X) :
x ∈ X.basic_open f ↔ is_unit (⇑(X.to_PresheafedSpace.presheaf.germ ⟨x, _⟩) f)
source
theorem algebraic_geometry.RingedSpace.basic_open_le (X : algebraic_geometry.RingedSpace) {U : topological_space.opens ↥X} (f : ↥(X.to_PresheafedSpace.presheaf.obj (opposite.op U))) :
X.basic_open f ≤ U
source
theorem algebraic_geometry.RingedSpace.is_unit_res_basic_open (X : algebraic_geometry.RingedSpace) {U : topological_space.opens ↥X} (f : ↥(X.to_PresheafedSpace.presheaf.obj (opposite.op U))) :
is_unit (⇑(X.to_PresheafedSpace.presheaf.map (category_theory.hom_of_le _).op) f)

The restriction of a section f to the basic open of f is a unit.

source
@[simp]
theorem algebraic_geometry.RingedSpace.basic_open_res (X : algebraic_geometry.RingedSpace) {U V : (topological_space.opens ↥X)ᵒᵖ} (i : U ⟶ V) (f : ↥(X.to_PresheafedSpace.presheaf.obj U)) :
X.basic_open (⇑(X.to_PresheafedSpace.presheaf.map i) f) = opposite.unop V ⊓ X.basic_open f
source
@[simp]
theorem algebraic_geometry.RingedSpace.basic_open_res_eq (X : algebraic_geometry.RingedSpace) {U V : (topological_space.opens ↥X)ᵒᵖ} (i : U ⟶ V) [category_theory.is_iso i] (f : ↥(X.to_PresheafedSpace.presheaf.obj U)) :
X.basic_open (⇑(X.to_PresheafedSpace.presheaf.map i) f) = X.basic_open f
source
@[simp]
theorem algebraic_geometry.RingedSpace.basic_open_mul (X : algebraic_geometry.RingedSpace) {U : topological_space.opens ↥X} (f g : ↥(X.to_PresheafedSpace.presheaf.obj (opposite.op U))) :
X.basic_open (f * g) = X.basic_open f ⊓ X.basic_open g
source
theorem algebraic_geometry.RingedSpace.basic_open_of_is_unit (X : algebraic_geometry.RingedSpace) {U : topological_space.opens ↥X} {f : ↥(X.to_PresheafedSpace.presheaf.obj (opposite.op U))} (hf : is_unit f) :
X.basic_open f = U