Ringed spaces #
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.
@[reducible]
The type of Ringed spaces, as an abbreviation for SheafedSpace CommRing
.
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)) :
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
.
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.
def
algebraic_geometry.RingedSpace.basic_open
(X : algebraic_geometry.RingedSpace)
{U : topological_space.opens ↥X}
(f : ↥(X.to_PresheafedSpace.presheaf.obj (opposite.op U))) :
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.
@[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)
@[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)
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
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.
@[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
@[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
@[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
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