Ringed spaces #

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

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, inline]

abbrev AlgebraicGeometry.RingedSpace :

TypeMax

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

Equations

AlgebraicGeometry.RingedSpace = AlgebraicGeometry.SheafedSpace CommRingCat

Instances For

source

@[simp]

theorem AlgebraicGeometry.RingedSpace.res_zero {X : AlgebraicGeometry.RingedSpace} {U V : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (hUV : U ≤ V) :

TopCat.Presheaf.restrictOpen 0 U hUV = 0

source

instance AlgebraicGeometry.RingedSpace.instCoeSortType :

CoeSort AlgebraicGeometry.RingedSpace (Type u_1)

Equations

AlgebraicGeometry.RingedSpace.instCoeSortType = { coe := fun (X : AlgebraicGeometry.RingedSpace) => ↑↑X.toPresheafedSpace }

source

theorem 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) (h : (X.presheaf.germ U ↑x ⋯).hom f = 0) :

∃ (V : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (i : V ⟶ U) (_ : ↑x ∈ V), (X.presheaf.map i.op).hom 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.

source

theorem AlgebraicGeometry.RingedSpace.isUnit_res_of_isUnit_germ (X : AlgebraicGeometry.RingedSpace) (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (f : ↑(X.presheaf.obj (Opposite.op U))) (x : ↑↑X.toPresheafedSpace) (hx : x ∈ U) (h : IsUnit ((X.presheaf.germ U x hx).hom f)) :

∃ (V : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (i : V ⟶ U) (_ : x ∈ V), IsUnit ((X.presheaf.map i.op).hom 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 CommRingCat.germ_res_apply {X : TopCat} (F : TopCat.Presheaf CommRingCat X) {U V : TopologicalSpace.Opens ↑X} (i : U ⟶ V) (x : ↑X) (hx : x ∈ U) (s : ↑(F.obj (Opposite.op V))) :

(F.germ U x hx).hom ((F.map i.op).hom s) = (F.germ V x ⋯).hom s

Specialize TopCat.Presheaf.germ_res_apply to sheaves of rings.

This is unfortunately needed because the results on presheaves are stated using the ConcreteCategory.instFunLike instance, which is not reducibly equal to the actual coercion of morphisms in CommRingCat to functions.

source

theorem CommRingCat.germ_res_apply' {X : TopCat} (F : TopCat.Presheaf CommRingCat X) {U V : TopologicalSpace.Opens ↑X} (i : Opposite.op V ⟶ Opposite.op U) (x : ↑X) (hx : x ∈ U) (s : ↑(F.obj (Opposite.op V))) :

(F.germ U x hx).hom ((F.map i).hom s) = (F.germ V x ⋯).hom s

Specialize TopCat.Presheaf.germ_res_apply' to sheaves of rings.

source

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

IsUnit f

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

source

def AlgebraicGeometry.RingedSpace.basicOpen (X : AlgebraicGeometry.RingedSpace) {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (f : ↑(X.presheaf.obj (Opposite.op U))) :

TopologicalSpace.Opens ↑↑X.toPresheafedSpace

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

X.basicOpen f = { carrier := {x : ↑↑X.toPresheafedSpace | ∃ (hx : x ∈ U), IsUnit ((X.presheaf.germ U x hx).hom f)}, is_open' := ⋯ }

Instances For

source

theorem AlgebraicGeometry.RingedSpace.mem_basicOpen (X : AlgebraicGeometry.RingedSpace) {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (f : ↑(X.presheaf.obj (Opposite.op U))) (x : ↑↑X.toPresheafedSpace) (hx : x ∈ U) :

x ∈ X.basicOpen f ↔ IsUnit ((X.presheaf.germ U x hx).hom f)

source

@[simp]

theorem AlgebraicGeometry.RingedSpace.mem_basicOpen' (X : AlgebraicGeometry.RingedSpace) {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (f : ↑(X.presheaf.obj (Opposite.op U))) (x : ↥U) :

↑x ∈ X.basicOpen f ↔ IsUnit ((X.presheaf.germ U ↑x ⋯).hom f)

A variant of mem_basicOpen with bundled x : U.

source

@[simp]

theorem AlgebraicGeometry.RingedSpace.mem_top_basicOpen (X : AlgebraicGeometry.RingedSpace) (f : ↑(X.presheaf.obj (Opposite.op ⊤))) (x : ↑↑X.toPresheafedSpace) :

x ∈ X.basicOpen f ↔ IsUnit ((X.presheaf.Γgerm x).hom f)

source

theorem AlgebraicGeometry.RingedSpace.basicOpen_le (X : AlgebraicGeometry.RingedSpace) {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (f : ↑(X.presheaf.obj (Opposite.op U))) :

X.basicOpen f ≤ U

source

theorem AlgebraicGeometry.RingedSpace.isUnit_res_basicOpen (X : AlgebraicGeometry.RingedSpace) {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (f : ↑(X.presheaf.obj (Opposite.op U))) :

IsUnit ((X.presheaf.map (CategoryTheory.homOfLE ⋯).op).hom f)

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

source

@[simp]

theorem AlgebraicGeometry.RingedSpace.basicOpen_res (X : AlgebraicGeometry.RingedSpace) {U V : (TopologicalSpace.Opens ↑↑X.toPresheafedSpace)ᵒᵖ} (i : U ⟶ V) (f : ↑(X.presheaf.obj U)) :

X.basicOpen ((X.presheaf.map i).hom f) = Opposite.unop V ⊓ X.basicOpen f

source

@[simp]

theorem AlgebraicGeometry.RingedSpace.basicOpen_res_eq (X : AlgebraicGeometry.RingedSpace) {U V : (TopologicalSpace.Opens ↑↑X.toPresheafedSpace)ᵒᵖ} (i : U ⟶ V) [CategoryTheory.IsIso i] (f : ↑(X.presheaf.obj U)) :

X.basicOpen ((X.presheaf.map i).hom f) = X.basicOpen f

source

@[simp]

theorem AlgebraicGeometry.RingedSpace.basicOpen_mul (X : AlgebraicGeometry.RingedSpace) {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (f g : ↑(X.presheaf.obj (Opposite.op U))) :

X.basicOpen (f * g) = X.basicOpen f ⊓ X.basicOpen g

source

@[simp]

theorem AlgebraicGeometry.RingedSpace.basicOpen_pow (X : AlgebraicGeometry.RingedSpace) {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (f : ↑(X.presheaf.obj (Opposite.op U))) (n : ℕ) (h : 0 < n) :

X.basicOpen (f ^ n) = X.basicOpen f

source

theorem AlgebraicGeometry.RingedSpace.basicOpen_of_isUnit (X : AlgebraicGeometry.RingedSpace) {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} {f : ↑(X.presheaf.obj (Opposite.op U))} (hf : IsUnit f) :

X.basicOpen f = U

source

def AlgebraicGeometry.RingedSpace.zeroLocus (X : AlgebraicGeometry.RingedSpace) {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (s : Set ↑(X.presheaf.obj (Opposite.op U))) :

Set ↑↑X.toPresheafedSpace

The zero locus of a set of sections s over an open set U is the closed set consisting of the complement of U and of all points of U, where all elements of f vanish.

Equations