# The category of locally ringed spaces #

We define (bundled) locally ringed spaces (as SheafedSpace CommRing along with the fact that the stalks are local rings), and morphisms between these (morphisms in SheafedSpace with IsLocalRingHom on the stalk maps).

structure AlgebraicGeometry.LocallyRingedSpaceextends :
Type (u + 1)

A LocallyRingedSpace is a topological space equipped with a sheaf of commutative rings such that all the stalks are local rings.

A morphism of locally ringed spaces is a morphism of ringed spaces such that the morphisms induced on stalks are local ring homomorphisms.

• carrier : TopCat
• presheaf : TopCat.Presheaf CommRingCat self.toPresheafedSpace
• IsSheaf : self.presheaf.IsSheaf
• localRing : ∀ (x : self.toPresheafedSpace), LocalRing (self.presheaf.stalk x)

Stalks of a locally ringed space are local rings.

Instances For
theorem AlgebraicGeometry.LocallyRingedSpace.localRing (x : self.toPresheafedSpace) :
LocalRing (self.presheaf.stalk x)

Stalks of a locally ringed space are local rings.

An alias for toSheafedSpace, where the result type is a RingedSpace. This allows us to use dot-notation for the RingedSpace namespace.

Equations
• X.toRingedSpace = X.toSheafedSpace
Instances For

The underlying topological space of a locally ringed space.

Equations
• X.toTopCat = X.toPresheafedSpace
Instances For
Equations
• =

The structure sheaf of a locally ringed space.

Equations
• X.𝒪 = X.sheaf
Instances For
theorem AlgebraicGeometry.LocallyRingedSpace.Hom.ext_iff {x : X.Hom Y} {y : X.Hom Y} :
x = y x.val = y.val
theorem AlgebraicGeometry.LocallyRingedSpace.Hom.ext {x : X.Hom Y} {y : X.Hom Y} (val : x.val = y.val) :
x = y

A morphism of locally ringed spaces is a morphism of ringed spaces such that the morphisms induced on stalks are local ring homomorphisms.

• val : X.toSheafedSpace Y.toSheafedSpace

the underlying morphism between ringed spaces

• prop : ∀ (x : X.toPresheafedSpace),

the underlying morphism induces a local ring homomorphism on stalks

Instances For
theorem AlgebraicGeometry.LocallyRingedSpace.Hom.prop (self : X.Hom Y) (x : X.toPresheafedSpace) :

the underlying morphism induces a local ring homomorphism on stalks

theorem AlgebraicGeometry.LocallyRingedSpace.Hom.ext'_iff {f : X Y} {g : X Y} :
f = g f.val = g.val
theorem AlgebraicGeometry.LocallyRingedSpace.Hom.ext' {f : X Y} {g : X Y} (h : f.val = g.val) :
f = g
noncomputable def AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (f : X.Hom Y) (x : X.toTopCat) :
Y.presheaf.stalk (f.val.base x) X.presheaf.stalk x

A morphism of locally ringed spaces f : X ⟶ Y induces a local ring homomorphism from Y.stalk (f x) to X.stalk x for any x : X.

Equations
• f.stalkMap x =
Instances For
Equations
• =
Equations
• =

The identity morphism on a locally ringed space.

Equations
Instances For
Equations
• X.instInhabitedHom = { default := X.id }
def AlgebraicGeometry.LocallyRingedSpace.comp (f : X.Hom Y) (g : Y.Hom Z) :
X.Hom Z

Composition of morphisms of locally ringed spaces.

Equations
Instances For

The category of locally ringed spaces.

Equations
• One or more equations did not get rendered due to their size.
@[simp]
@[simp]

The forgetful functor from LocallyRingedSpace to SheafedSpace CommRing.

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

The forgetful functor from LocallyRingedSpace to Top.

Equations
Instances For
theorem AlgebraicGeometry.LocallyRingedSpace.comp_val_c_app (f : X Y) (g : Y Z) (U : (TopologicalSpace.Opens Z.toTopCat)ᵒᵖ) :
.val.c.app U = CategoryTheory.CategoryStruct.comp (g.val.c.app U) (f.val.c.app (Opposite.op ((TopologicalSpace.Opens.map g.val.base).obj )))
@[simp]
theorem AlgebraicGeometry.LocallyRingedSpace.homOfSheafedSpaceHomOfIsIso_val (f : X.toSheafedSpace Y.toSheafedSpace) :
def AlgebraicGeometry.LocallyRingedSpace.homOfSheafedSpaceHomOfIsIso (f : X.toSheafedSpace Y.toSheafedSpace) :
X Y

Given two locally ringed spaces X and Y, an isomorphism between X and Y as sheafed spaces can be lifted to a morphism X ⟶ Y as locally ringed spaces.

See also isoOfSheafedSpaceIso.

Equations
• = { val := f, prop := }
Instances For
def AlgebraicGeometry.LocallyRingedSpace.isoOfSheafedSpaceIso (f : X.toSheafedSpace Y.toSheafedSpace) :
X Y

Given two locally ringed spaces X and Y, an isomorphism between X and Y as sheafed spaces can be lifted to an isomorphism X ⟶ Y as locally ringed spaces.

This is related to the property that the functor forgetToSheafedSpace reflects isomorphisms. In fact, it is slightly stronger as we do not require f to come from a morphism between locally ringed spaces.

Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
• =
@[simp]
theorem AlgebraicGeometry.LocallyRingedSpace.restrict_presheaf_obj {U : TopCat} {f : U X✝.toTopCat} (h : ) (X : ) :
(X✝.restrict h).presheaf.obj X = X✝.presheaf.obj (Opposite.op (.functor.obj ))
@[simp]
theorem AlgebraicGeometry.LocallyRingedSpace.restrict_carrier {U : TopCat} {f : U X.toTopCat} (h : ) :
(X.restrict h).toPresheafedSpace = U
@[simp]
theorem AlgebraicGeometry.LocallyRingedSpace.restrict_presheaf_map {U : TopCat} {f : U X.toTopCat} (h : ) :
∀ {X_1 Y : } (f_1 : X_1 Y), (X.restrict h).presheaf.map f_1 = X.presheaf.map (.functor.map f_1.unop).op

The restriction of a locally ringed space along an open embedding.

Equations
• X.restrict h = { toSheafedSpace := X.restrict h, localRing := }
Instances For
def AlgebraicGeometry.LocallyRingedSpace.ofRestrict {U : TopCat} {f : U X.toTopCat} (h : ) :
X.restrict h X

The canonical map from the restriction to the subspace.

Equations
• X.ofRestrict h = { val := X.ofRestrict h, prop := }
Instances For

The restriction of a locally ringed space X to the top subspace is isomorphic to X itself.

Equations
Instances For

The global sections, notated Gamma.

Equations
Instances For
@[simp]
@[simp]
theorem AlgebraicGeometry.LocallyRingedSpace.Γ_map (f : X Y) :
= f.unop.val.c.app

The empty locally ringed space.

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

The canonical map from the empty locally ringed space.

Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
• AlgebraicGeometry.LocallyRingedSpace.instUniqueHomEmptyCollection = { default := X.emptyTo, uniq := }

The empty space is initial in LocallyRingedSpace.

Equations
Instances For
theorem AlgebraicGeometry.LocallyRingedSpace.preimage_basicOpen (f : X Y) {U : TopologicalSpace.Opens Y.toTopCat} (s : (Y.presheaf.obj (Opposite.op U))) :
(TopologicalSpace.Opens.map f.val.base).obj (Y.toRingedSpace.basicOpen s) = X.toRingedSpace.basicOpen ((f.val.c.app (Opposite.op U)) s)
theorem AlgebraicGeometry.LocallyRingedSpace.basicOpen_zero (U : TopologicalSpace.Opens X.toPresheafedSpace) :
X.toRingedSpace.basicOpen 0 =
@[simp]
theorem AlgebraicGeometry.LocallyRingedSpace.basicOpen_eq_bot_of_isNilpotent (U : TopologicalSpace.Opens X.toPresheafedSpace) (f : (X.presheaf.obj (Opposite.op U))) (hf : ) :
X.toRingedSpace.basicOpen f =
instance AlgebraicGeometry.LocallyRingedSpace.component_nontrivial (U : TopologicalSpace.Opens X.toPresheafedSpace) [hU : Nonempty U] :
Nontrivial (X.presheaf.obj (Opposite.op U))
Equations
• =
@[simp]
theorem AlgebraicGeometry.LocallyRingedSpace.iso_hom_val_base_inv_val_base_apply (e : X Y) (x : X.toTopCat) :
e.inv.val.base (e.hom.val.base x) = x
@[simp]
theorem AlgebraicGeometry.LocallyRingedSpace.iso_inv_val_base_hom_val_base_apply (e : X Y) (y : Y.toTopCat) :
e.hom.val.base (e.inv.val.base y) = y
@[simp]
theorem AlgebraicGeometry.LocallyRingedSpace.stalkMap_comp (f : X Y) (g : Y Z) (x : X.toTopCat) :
theorem AlgebraicGeometry.LocallyRingedSpace.stalkSpecializes_stalkMap_assoc (f : X Y) (x : X.toTopCat) (x' : X.toTopCat) (h : x x') {Z : CommRingCat} (h : X.presheaf.stalk x Z) :
CategoryTheory.CategoryStruct.comp (Y.presheaf.stalkSpecializes ) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (X.presheaf.stalkSpecializes h✝) h)
theorem AlgebraicGeometry.LocallyRingedSpace.stalkSpecializes_stalkMap (f : X Y) (x : X.toTopCat) (x' : X.toTopCat) (h : x x') :
CategoryTheory.CategoryStruct.comp (Y.presheaf.stalkSpecializes ) = CategoryTheory.CategoryStruct.comp (X.presheaf.stalkSpecializes h)
theorem AlgebraicGeometry.LocallyRingedSpace.stalkSpecializes_stalkMap_apply (f : X Y) (x : X.toTopCat) (x' : X.toTopCat) (h : x x') (y : (Y.presheaf.stalk (f.val.base x'))) :
((Y.presheaf.stalkSpecializes ) y) = (X.presheaf.stalkSpecializes h)
theorem AlgebraicGeometry.LocallyRingedSpace.stalkMap_congr_assoc (f : X Y) (g : X Y) (hfg : f = g) (x : X.toTopCat) (x' : X.toTopCat) (hxx' : x = x') {Z : CommRingCat} (h : X.presheaf.stalk x' Z) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (X.presheaf.stalkSpecializes ) h) = CategoryTheory.CategoryStruct.comp (Y.presheaf.stalkSpecializes )
theorem AlgebraicGeometry.LocallyRingedSpace.stalkMap_congr (f : X Y) (g : X Y) (hfg : f = g) (x : X.toTopCat) (x' : X.toTopCat) (hxx' : x = x') :
CategoryTheory.CategoryStruct.comp (X.presheaf.stalkSpecializes ) = CategoryTheory.CategoryStruct.comp (Y.presheaf.stalkSpecializes )
theorem AlgebraicGeometry.LocallyRingedSpace.stalkMap_congr_hom_assoc (f : X Y) (g : X Y) (hfg : f = g) (x : X.toTopCat) {Z : CommRingCat} (h : X.presheaf.stalk x Z) :
= CategoryTheory.CategoryStruct.comp (Y.presheaf.stalkSpecializes )
theorem AlgebraicGeometry.LocallyRingedSpace.stalkMap_congr_hom (f : X Y) (g : X Y) (hfg : f = g) (x : X.toTopCat) :
= CategoryTheory.CategoryStruct.comp (Y.presheaf.stalkSpecializes )
theorem AlgebraicGeometry.LocallyRingedSpace.stalkMap_congr_point_assoc (f : X Y) (x : X.toTopCat) (x' : X.toTopCat) (hxx' : x = x') {Z : CommRingCat} (h : X.presheaf.stalk x' Z) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (X.presheaf.stalkSpecializes ) h) = CategoryTheory.CategoryStruct.comp (Y.presheaf.stalkSpecializes )
theorem AlgebraicGeometry.LocallyRingedSpace.stalkMap_congr_point (f : X Y) (x : X.toTopCat) (x' : X.toTopCat) (hxx' : x = x') :
CategoryTheory.CategoryStruct.comp (X.presheaf.stalkSpecializes ) = CategoryTheory.CategoryStruct.comp (Y.presheaf.stalkSpecializes )
@[simp]
theorem AlgebraicGeometry.LocallyRingedSpace.stalkMap_hom_inv_assoc (e : X Y) (y : Y.toTopCat) {Z : CommRingCat} (h : Y.presheaf.stalk y Z) :
@[simp]
theorem AlgebraicGeometry.LocallyRingedSpace.stalkMap_hom_inv (e : X Y) (y : Y.toTopCat) :
CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap e.hom (e.inv.val.base y)) = Y.presheaf.stalkSpecializes
@[simp]
theorem AlgebraicGeometry.LocallyRingedSpace.stalkMap_hom_inv_apply (e : X Y) (y : Y.toTopCat) (z : (Y.presheaf.stalk (e.hom.val.base (e.inv.val.base y)))) :
((AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap e.hom (e.inv.val.base y)) z) = (Y.presheaf.stalkSpecializes ) z
@[simp]
theorem AlgebraicGeometry.LocallyRingedSpace.stalkMap_inv_hom_assoc (e : X Y) (x : X.toTopCat) {Z : CommRingCat} (h : X.presheaf.stalk x Z) :
@[simp]
theorem AlgebraicGeometry.LocallyRingedSpace.stalkMap_inv_hom (e : X Y) (x : X.toTopCat) :
CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap e.inv (e.hom.val.base x)) = X.presheaf.stalkSpecializes
@[simp]
theorem AlgebraicGeometry.LocallyRingedSpace.stalkMap_inv_hom_apply (e : X Y) (x : X.toTopCat) (y : (X.presheaf.stalk (e.inv.val.base (e.hom.val.base x)))) :
((AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap e.inv (e.hom.val.base x)) y) = (X.presheaf.stalkSpecializes ) y
theorem AlgebraicGeometry.LocallyRingedSpace.stalkMap_germ_assoc (f : X Y) (U : TopologicalSpace.Opens Y.toTopCat) (x : ((TopologicalSpace.Opens.map f.val.base).obj U)) {Z : CommRingCat} (h : X.presheaf.stalk x Z) :
CategoryTheory.CategoryStruct.comp (Y.presheaf.germ f.val.base x, ) = CategoryTheory.CategoryStruct.comp (f.val.c.app (Opposite.op U)) (CategoryTheory.CategoryStruct.comp (X.presheaf.germ x) h)
theorem AlgebraicGeometry.LocallyRingedSpace.stalkMap_germ (f : X Y) (U : TopologicalSpace.Opens Y.toTopCat) (x : ((TopologicalSpace.Opens.map f.val.base).obj U)) :
CategoryTheory.CategoryStruct.comp (Y.presheaf.germ f.val.base x, ) = CategoryTheory.CategoryStruct.comp (f.val.c.app (Opposite.op U)) (X.presheaf.germ x)
theorem AlgebraicGeometry.LocallyRingedSpace.stalkMap_germ_apply (f : X Y) (U : TopologicalSpace.Opens Y.toTopCat) (x : ((TopologicalSpace.Opens.map f.val.base).obj U)) (y : (Y.presheaf.obj (Opposite.op U))) :
((Y.presheaf.germ f.val.base x, ) y) = (X.presheaf.germ x) ((f.val.c.app (Opposite.op U)) y)
@[simp]
theorem AlgebraicGeometry.LocallyRingedSpace.stalkMap_germ'_assoc (f : X Y) (U : TopologicalSpace.Opens Y.toTopCat) (x : X.toTopCat) (hx : f.val.base x U) {Z : CommRingCat} (h : X.presheaf.stalk x Z) :
CategoryTheory.CategoryStruct.comp (Y.presheaf.germ f.val.base x, hx) = CategoryTheory.CategoryStruct.comp (f.val.c.app (Opposite.op U)) (CategoryTheory.CategoryStruct.comp (X.presheaf.germ x, hx) h)
@[simp]
theorem AlgebraicGeometry.LocallyRingedSpace.stalkMap_germ' (f : X Y) (U : TopologicalSpace.Opens Y.toTopCat) (x : X.toTopCat) (hx : f.val.base x U) :
CategoryTheory.CategoryStruct.comp (Y.presheaf.germ f.val.base x, hx) = CategoryTheory.CategoryStruct.comp (f.val.c.app (Opposite.op U)) (X.presheaf.germ x, hx)
@[simp]
theorem AlgebraicGeometry.LocallyRingedSpace.stalkMap_germ'_apply (f : X Y) (U : TopologicalSpace.Opens Y.toTopCat) (x : X.toTopCat) (hx : f.val.base x U) (y : (Y.presheaf.obj (Opposite.op U))) :
((Y.presheaf.germ f.val.base x, hx) y) = (X.presheaf.germ x, hx) ((f.val.c.app (Opposite.op U)) y)
noncomputable def AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso {U : TopCat} {f : U X.toTopCat} (h : ) (x : U) :
(X.restrict h).presheaf.stalk x X.presheaf.stalk (f x)

For an open embedding f : U ⟶ X and a point x : U, we get an isomorphism between the stalk of X at f x and the stalk of the restriction of X along f at t x.

Equations
• X.restrictStalkIso h x = X.restrictStalkIso h x
Instances For
@[simp]
theorem AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_hom_eq_germ_assoc {U : TopCat} {f : U X.toTopCat} (h : ) (V : ) (x : U) (hx : x V) {Z : CommRingCat} (h : X.presheaf.stalk (f x) Z) :
CategoryTheory.CategoryStruct.comp ((X.restrict h✝).presheaf.germ x, hx) (CategoryTheory.CategoryStruct.comp (X.restrictStalkIso h✝ x).hom h) = CategoryTheory.CategoryStruct.comp (X.presheaf.germ f x, ) h
@[simp]
theorem AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_hom_eq_germ {U : TopCat} {f : U X.toTopCat} (h : ) (V : ) (x : U) (hx : x V) :
CategoryTheory.CategoryStruct.comp ((X.restrict h).presheaf.germ x, hx) (X.restrictStalkIso h x).hom = X.presheaf.germ f x,
theorem AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_hom_eq_germ_apply {U : TopCat} {f : U X.toTopCat} (h : ) (V : ) (x : U) (hx : x V) (y : ((X.restrict h).presheaf.obj (Opposite.op V))) :
(X.restrictStalkIso h x).hom (((X.restrict h).presheaf.germ x, hx) y) = (X.presheaf.germ f x, ) y
@[simp]
theorem AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_inv_eq_germ_assoc {U : TopCat} {f : U X.toTopCat} (h : ) (V : ) (x : U) (hx : x V) {Z : CommRingCat} (h : (X.restrict h✝).presheaf.stalk x Z) :
CategoryTheory.CategoryStruct.comp (X.presheaf.germ f x, ) (CategoryTheory.CategoryStruct.comp (X.restrictStalkIso h✝ x).inv h) = CategoryTheory.CategoryStruct.comp ((X.restrict h✝).presheaf.germ x, hx) h
@[simp]
theorem AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_inv_eq_germ {U : TopCat} {f : U X.toTopCat} (h : ) (V : ) (x : U) (hx : x V) :
CategoryTheory.CategoryStruct.comp (X.presheaf.germ f x, ) (X.restrictStalkIso h x).inv = (X.restrict h).presheaf.germ x, hx
theorem AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_inv_eq_germ_apply {U : TopCat} {f : U X.toTopCat} (h : ) (V : ) (x : U) (hx : x V) (y : (X.presheaf.obj (Opposite.op (.functor.obj V)))) :
(X.restrictStalkIso h x).inv ((X.presheaf.germ f x, ) y) = ((X.restrict h).presheaf.germ x, hx) y
theorem AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_inv_eq_ofRestrict {U : TopCat} {f : U X.toTopCat} (h : ) (x : U) :
(X.restrictStalkIso h x).inv = AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (X.ofRestrict h) x