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 .

@[inline, reducible]

abbrev AlgebraicGeometry.RingedSpace : TypeMax

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

Equations

• AlgebraicGeometry.RingedSpace = AlgebraicGeometry.SheafedSpace CommRingCat

instance AlgebraicGeometry.RingedSpace.instCoeSortRingedSpaceType : CoeSort AlgebraicGeometry.RingedSpace (Type u_1)

Equations

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

theorem AlgebraicGeometry.RingedSpace.isUnit_res_of_isUnit_germ (X : AlgebraicGeometry.RingedSpace) (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (f : ↑(X.presheaf.toPrefunctor.obj (Opposite.op U))) (x : ↥U) (h : IsUnit ((TopCat.Presheaf.germ X.presheaf x) f)) : ∃ (V : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (i : V ⟶ U) (_ : ↑x ∈ V), IsUnit ((X.presheaf.toPrefunctor.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.

theorem AlgebraicGeometry.RingedSpace.isUnit_of_isUnit_germ (X : AlgebraicGeometry.RingedSpace) (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (f : ↑(X.presheaf.toPrefunctor.obj (Opposite.op U))) (h : ∀ (x : ↥U), IsUnit ((TopCat.Presheaf.germ X.presheaf x) f)) : IsUnit f

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

def AlgebraicGeometry.RingedSpace.basicOpen (X : AlgebraicGeometry.RingedSpace) {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (f : ↑(X.presheaf.toPrefunctor.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

• One or more equations did not get rendered due to their size.

@[simp]

theorem AlgebraicGeometry.RingedSpace.mem_basicOpen (X : AlgebraicGeometry.RingedSpace) {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (f : ↑(X.presheaf.toPrefunctor.obj (Opposite.op U))) (x : ↥U) : ↑x ∈ AlgebraicGeometry.RingedSpace.basicOpen X f ↔ IsUnit ((TopCat.Presheaf.germ X.presheaf x) f)

@[simp]

theorem AlgebraicGeometry.RingedSpace.mem_top_basicOpen (X : AlgebraicGeometry.RingedSpace) (f : ↑(X.presheaf.toPrefunctor.obj (Opposite.op ⊤))) (x : ↑↑X.toPresheafedSpace) : x ∈ AlgebraicGeometry.RingedSpace.basicOpen X f ↔ IsUnit ((TopCat.Presheaf.germ X.presheaf { val := x, property := (_ : x ∈ ⊤) }) f)

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

theorem AlgebraicGeometry.RingedSpace.isUnit_res_basicOpen (X : AlgebraicGeometry.RingedSpace) {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (f : ↑(X.presheaf.toPrefunctor.obj (Opposite.op U))) : IsUnit ((X.presheaf.toPrefunctor.map (CategoryTheory.homOfLE (_ : AlgebraicGeometry.RingedSpace.basicOpen X f ≤ U)).op) f)

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

@[simp]

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

@[simp]

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

@[simp]

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

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