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 is_local_ring_hom on the stalk maps).

structure AlgebraicGeometry.LocallyRingedSpaceextends AlgebraicGeometry.SheafedSpace : Type (u_1 + 1)

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

  Stalks of a locally ringed space are local rings.

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.

def AlgebraicGeometry.LocallyRingedSpace.toRingedSpace (X : AlgebraicGeometry.LocallyRingedSpace) : AlgebraicGeometry.RingedSpace

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

def AlgebraicGeometry.LocallyRingedSpace.toTopCat (X : AlgebraicGeometry.LocallyRingedSpace) : TopCat

The underlying topological space of a locally ringed space.

instance AlgebraicGeometry.LocallyRingedSpace.instCoeSortLocallyRingedSpaceType : CoeSort AlgebraicGeometry.LocallyRingedSpace (Type u_1)

instance AlgebraicGeometry.LocallyRingedSpace.instLocalRingαCommRingStalkCommRingCatInstCommRingCatLargeCategoryHasColimits_commRingCatToPresheafedSpaceToSheafedSpaceToSemiringToCommSemiringInstCommRingα (X : AlgebraicGeometry.LocallyRingedSpace) (x : ↑(AlgebraicGeometry.LocallyRingedSpace.toTopCat X)) : LocalRing ↑(AlgebraicGeometry.PresheafedSpace.stalk X.toPresheafedSpace x)

def AlgebraicGeometry.LocallyRingedSpace.𝒪 (X : AlgebraicGeometry.LocallyRingedSpace) : TopCat.Sheaf CommRingCat (AlgebraicGeometry.LocallyRingedSpace.toTopCat X)

The structure sheaf of a locally ringed space.

theorem AlgebraicGeometry.LocallyRingedSpace.Hom.ext_iff {X : AlgebraicGeometry.LocallyRingedSpace} {Y : AlgebraicGeometry.LocallyRingedSpace} (x : AlgebraicGeometry.LocallyRingedSpace.Hom X Y) (y : AlgebraicGeometry.LocallyRingedSpace.Hom X Y) : x = y ↔ x.val = y.val

theorem AlgebraicGeometry.LocallyRingedSpace.Hom.ext {X : AlgebraicGeometry.LocallyRingedSpace} {Y : AlgebraicGeometry.LocallyRingedSpace} (x : AlgebraicGeometry.LocallyRingedSpace.Hom X Y) (y : AlgebraicGeometry.LocallyRingedSpace.Hom X Y) (val : x.val = y.val) : x = y

structure AlgebraicGeometry.LocallyRingedSpace.Hom (X : AlgebraicGeometry.LocallyRingedSpace) (Y : AlgebraicGeometry.LocallyRingedSpace) : Type u_1

• val : X.toSheafedSpace ⟶ Y.toSheafedSpace

  the underlying morphism between ringed spaces

• prop : ∀ (x : ↑↑X.toPresheafedSpace), IsLocalRingHom (AlgebraicGeometry.PresheafedSpace.stalkMap s.val x)

  the underlying morphism induces a local ring homomorphism on stalks

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

instance AlgebraicGeometry.LocallyRingedSpace.instQuiverLocallyRingedSpace : Quiver AlgebraicGeometry.LocallyRingedSpace

theorem AlgebraicGeometry.LocallyRingedSpace.Hom.ext' (X : AlgebraicGeometry.LocallyRingedSpace) (Y : AlgebraicGeometry.LocallyRingedSpace) {f : X ⟶ Y} {g : X ⟶ Y} (h : f.val = g.val) : f = g

noncomputable def AlgebraicGeometry.LocallyRingedSpace.stalk (X : AlgebraicGeometry.LocallyRingedSpace) (x : ↑(AlgebraicGeometry.LocallyRingedSpace.toTopCat X)) : CommRingCat

The stalk of a locally ringed space, just as a CommRing.

instance AlgebraicGeometry.LocallyRingedSpace.stalkLocal (X : AlgebraicGeometry.LocallyRingedSpace) (x : ↑(AlgebraicGeometry.LocallyRingedSpace.toTopCat X)) : LocalRing ↑(AlgebraicGeometry.LocallyRingedSpace.stalk X x)

noncomputable def AlgebraicGeometry.LocallyRingedSpace.stalkMap {X : AlgebraicGeometry.LocallyRingedSpace} {Y : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y) (x : ↑(AlgebraicGeometry.LocallyRingedSpace.toTopCat X)) : AlgebraicGeometry.LocallyRingedSpace.stalk Y (↑f.val.base x) ⟶ AlgebraicGeometry.LocallyRingedSpace.stalk X 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.

instance AlgebraicGeometry.LocallyRingedSpace.instIsLocalRingHomαCommRingStalkCoeHomTopCatToQuiverToCategoryStructInstTopCatLargeCategoryCarrierCommRingCatInstCommRingCatLargeCategoryToPresheafedSpaceToSheafedSpaceObjTypeTypesToPrefunctorForgetConcreteCategoryFunLikeBaseValToSemiringToRingStrStalkMap {X : AlgebraicGeometry.LocallyRingedSpace} {Y : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y) (x : ↑(AlgebraicGeometry.LocallyRingedSpace.toTopCat X)) : IsLocalRingHom (AlgebraicGeometry.LocallyRingedSpace.stalkMap f x)

instance AlgebraicGeometry.LocallyRingedSpace.instIsLocalRingHomαCommRingStalkCommRingCatInstCommRingCatLargeCategoryHasColimits_commRingCatToPresheafedSpaceToSheafedSpaceCoeHomTopCatToQuiverToCategoryStructInstTopCatLargeCategoryCarrierObjTypeTypesToPrefunctorForgetConcreteCategoryFunLikeBaseValToSemiringToRingStrStalkMap {X : AlgebraicGeometry.LocallyRingedSpace} {Y : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y) (x : ↑(AlgebraicGeometry.LocallyRingedSpace.toTopCat X)) : IsLocalRingHom (AlgebraicGeometry.PresheafedSpace.stalkMap f.val x)

@[simp]

theorem AlgebraicGeometry.LocallyRingedSpace.id_val (X : AlgebraicGeometry.LocallyRingedSpace) : (AlgebraicGeometry.LocallyRingedSpace.id X).val = CategoryTheory.CategoryStruct.id X.toSheafedSpace

def AlgebraicGeometry.LocallyRingedSpace.id (X : AlgebraicGeometry.LocallyRingedSpace) : AlgebraicGeometry.LocallyRingedSpace.Hom X X

The identity morphism on a locally ringed space.

instance AlgebraicGeometry.LocallyRingedSpace.instInhabitedHom (X : AlgebraicGeometry.LocallyRingedSpace) : Inhabited (AlgebraicGeometry.LocallyRingedSpace.Hom X X)

def AlgebraicGeometry.LocallyRingedSpace.comp {X : AlgebraicGeometry.LocallyRingedSpace} {Y : AlgebraicGeometry.LocallyRingedSpace} {Z : AlgebraicGeometry.LocallyRingedSpace} (f : AlgebraicGeometry.LocallyRingedSpace.Hom X Y) (g : AlgebraicGeometry.LocallyRingedSpace.Hom Y Z) : AlgebraicGeometry.LocallyRingedSpace.Hom X Z

Composition of morphisms of locally ringed spaces.

instance AlgebraicGeometry.LocallyRingedSpace.instCategoryLocallyRingedSpace : CategoryTheory.Category.{u_1, u_1 + 1} AlgebraicGeometry.LocallyRingedSpace

The category of locally ringed spaces.

@[simp]

theorem AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace_map {X : AlgebraicGeometry.LocallyRingedSpace} {Y : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y) : AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace.map f = f.val

@[simp]

theorem AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace_obj (X : AlgebraicGeometry.LocallyRingedSpace) : AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace.obj X = X.toSheafedSpace

def AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace : CategoryTheory.Functor AlgebraicGeometry.LocallyRingedSpace (AlgebraicGeometry.SheafedSpace CommRingCat)

The forgetful functor from LocallyRingedSpace to SheafedSpace CommRing.

instance AlgebraicGeometry.LocallyRingedSpace.instFaithfulLocallyRingedSpaceInstCategoryLocallyRingedSpaceSheafedSpaceCommRingCatInstCommRingCatLargeCategoryInstCategorySheafedSpaceForgetToSheafedSpace : CategoryTheory.Faithful AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace

@[simp]

theorem AlgebraicGeometry.LocallyRingedSpace.forgetToTop_map : ∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y), AlgebraicGeometry.LocallyRingedSpace.forgetToTop.map f = (AlgebraicGeometry.SheafedSpace.forget CommRingCat).map f.val

@[simp]

theorem AlgebraicGeometry.LocallyRingedSpace.forgetToTop_obj (X : AlgebraicGeometry.LocallyRingedSpace) : AlgebraicGeometry.LocallyRingedSpace.forgetToTop.obj X = (AlgebraicGeometry.SheafedSpace.forget CommRingCat).obj X.toSheafedSpace

def AlgebraicGeometry.LocallyRingedSpace.forgetToTop : CategoryTheory.Functor AlgebraicGeometry.LocallyRingedSpace TopCat

The forgetful functor from LocallyRingedSpace to Top.

@[simp]

theorem AlgebraicGeometry.LocallyRingedSpace.comp_val {X : AlgebraicGeometry.LocallyRingedSpace} {Y : AlgebraicGeometry.LocallyRingedSpace} {Z : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryTheory.CategoryStruct.comp f g).val = CategoryTheory.CategoryStruct.comp f.val g.val

@[simp]

theorem AlgebraicGeometry.LocallyRingedSpace.comp_val_c {X : AlgebraicGeometry.LocallyRingedSpace} {Y : AlgebraicGeometry.LocallyRingedSpace} {Z : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryTheory.CategoryStruct.comp f.val g.val).c = CategoryTheory.CategoryStruct.comp g.val.c ((TopCat.Presheaf.pushforward CommRingCat g.val.base).map f.val.c)

theorem AlgebraicGeometry.LocallyRingedSpace.comp_val_c_app {X : AlgebraicGeometry.LocallyRingedSpace} {Y : AlgebraicGeometry.LocallyRingedSpace} {Z : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y) (g : Y ⟶ Z) (U : (TopologicalSpace.Opens ↑(AlgebraicGeometry.LocallyRingedSpace.toTopCat Z))ᵒᵖ) : (CategoryTheory.CategoryStruct.comp f g).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 U.unop)))

@[simp]

theorem AlgebraicGeometry.LocallyRingedSpace.homOfSheafedSpaceHomOfIsIso_val {X : AlgebraicGeometry.LocallyRingedSpace} {Y : AlgebraicGeometry.LocallyRingedSpace} (f : X.toSheafedSpace ⟶ Y.toSheafedSpace) [CategoryTheory.IsIso f] : (AlgebraicGeometry.LocallyRingedSpace.homOfSheafedSpaceHomOfIsIso f).val = f

def AlgebraicGeometry.LocallyRingedSpace.homOfSheafedSpaceHomOfIsIso {X : AlgebraicGeometry.LocallyRingedSpace} {Y : AlgebraicGeometry.LocallyRingedSpace} (f : X.toSheafedSpace ⟶ Y.toSheafedSpace) [CategoryTheory.IsIso f] : 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 iso_of_SheafedSpace_iso.

def AlgebraicGeometry.LocallyRingedSpace.isoOfSheafedSpaceIso {X : AlgebraicGeometry.LocallyRingedSpace} {Y : AlgebraicGeometry.LocallyRingedSpace} (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 forget_to_SheafedSpace reflects isomorphisms. In fact, it is slightly stronger as we do not require f to come from a morphism between locally ringed spaces.

instance AlgebraicGeometry.LocallyRingedSpace.instReflectsIsomorphismsLocallyRingedSpaceInstCategoryLocallyRingedSpaceSheafedSpaceCommRingCatInstCommRingCatLargeCategoryInstCategorySheafedSpaceForgetToSheafedSpace : CategoryTheory.ReflectsIsomorphisms AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace

instance AlgebraicGeometry.LocallyRingedSpace.is_sheafedSpace_iso {X : AlgebraicGeometry.LocallyRingedSpace} {Y : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y) [CategoryTheory.IsIso f] : CategoryTheory.IsIso f.val

@[simp]

theorem AlgebraicGeometry.LocallyRingedSpace.restrict_carrier {U : TopCat} (X : AlgebraicGeometry.LocallyRingedSpace) {f : U ⟶ AlgebraicGeometry.LocallyRingedSpace.toTopCat X} (h : OpenEmbedding ↑f) : ↑(AlgebraicGeometry.LocallyRingedSpace.restrict X h).toSheafedSpace.toPresheafedSpace = U

@[simp]

theorem AlgebraicGeometry.LocallyRingedSpace.restrict_presheaf_obj {U : TopCat} (X : AlgebraicGeometry.LocallyRingedSpace) {f : U ⟶ AlgebraicGeometry.LocallyRingedSpace.toTopCat X} (h : OpenEmbedding ↑f) (X : (TopologicalSpace.Opens ↑U)ᵒᵖ) : (AlgebraicGeometry.LocallyRingedSpace.restrict X h).toSheafedSpace.toPresheafedSpace.presheaf.obj X = X.presheaf.obj (Opposite.op ((IsOpenMap.functor (_ : IsOpenMap ↑f)).obj X.unop))

@[simp]

theorem AlgebraicGeometry.LocallyRingedSpace.restrict_presheaf_map {U : TopCat} (X : AlgebraicGeometry.LocallyRingedSpace) {f : U ⟶ AlgebraicGeometry.LocallyRingedSpace.toTopCat X} (h : OpenEmbedding ↑f) : ∀ {X Y : (TopologicalSpace.Opens ↑U)ᵒᵖ} (f : X ⟶ Y), (AlgebraicGeometry.LocallyRingedSpace.restrict X h).toSheafedSpace.toPresheafedSpace.presheaf.map f = X.presheaf.map ((IsOpenMap.functor (_ : IsOpenMap ↑f)).map f.unop).op

def AlgebraicGeometry.LocallyRingedSpace.restrict {U : TopCat} (X : AlgebraicGeometry.LocallyRingedSpace) {f : U ⟶ AlgebraicGeometry.LocallyRingedSpace.toTopCat X} (h : OpenEmbedding ↑f) : AlgebraicGeometry.LocallyRingedSpace

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

def AlgebraicGeometry.LocallyRingedSpace.ofRestrict {U : TopCat} (X : AlgebraicGeometry.LocallyRingedSpace) {f : U ⟶ AlgebraicGeometry.LocallyRingedSpace.toTopCat X} (h : OpenEmbedding ↑f) : AlgebraicGeometry.LocallyRingedSpace.restrict X h ⟶ X

The canonical map from the restriction to the supspace.

def AlgebraicGeometry.LocallyRingedSpace.restrictTopIso (X : AlgebraicGeometry.LocallyRingedSpace) : AlgebraicGeometry.LocallyRingedSpace.restrict X (_ : OpenEmbedding ↑(TopologicalSpace.Opens.inclusion ⊤)) ≅ X

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

def AlgebraicGeometry.LocallyRingedSpace.Γ : CategoryTheory.Functor AlgebraicGeometry.LocallyRingedSpaceᵒᵖ CommRingCat

The global sections, notated Gamma.

theorem AlgebraicGeometry.LocallyRingedSpace.Γ_def : AlgebraicGeometry.LocallyRingedSpace.Γ = CategoryTheory.Functor.comp AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace.op AlgebraicGeometry.SheafedSpace.Γ

@[simp]

theorem AlgebraicGeometry.LocallyRingedSpace.Γ_obj (X : AlgebraicGeometry.LocallyRingedSpaceᵒᵖ) : AlgebraicGeometry.LocallyRingedSpace.Γ.obj X = X.unop.presheaf.obj (Opposite.op ⊤)

theorem AlgebraicGeometry.LocallyRingedSpace.Γ_obj_op (X : AlgebraicGeometry.LocallyRingedSpace) : AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X) = X.presheaf.obj (Opposite.op ⊤)

@[simp]

theorem AlgebraicGeometry.LocallyRingedSpace.Γ_map {X : AlgebraicGeometry.LocallyRingedSpaceᵒᵖ} {Y : AlgebraicGeometry.LocallyRingedSpaceᵒᵖ} (f : X ⟶ Y) : AlgebraicGeometry.LocallyRingedSpace.Γ.map f = f.unop.val.c.app (Opposite.op ⊤)

theorem AlgebraicGeometry.LocallyRingedSpace.Γ_map_op {X : AlgebraicGeometry.LocallyRingedSpace} {Y : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y) : AlgebraicGeometry.LocallyRingedSpace.Γ.map f.op = f.val.c.app (Opposite.op ⊤)

theorem AlgebraicGeometry.LocallyRingedSpace.preimage_basicOpen {X : AlgebraicGeometry.LocallyRingedSpace} {Y : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y) {U : TopologicalSpace.Opens ↑(AlgebraicGeometry.LocallyRingedSpace.toTopCat Y)} (s : ↑(Y.presheaf.obj (Opposite.op U))) : (TopologicalSpace.Opens.map f.val.base).obj (AlgebraicGeometry.RingedSpace.basicOpen (AlgebraicGeometry.LocallyRingedSpace.toRingedSpace Y) s) = AlgebraicGeometry.RingedSpace.basicOpen (AlgebraicGeometry.LocallyRingedSpace.toRingedSpace X) (↑(f.val.c.app (Opposite.op U)) s)

@[simp]

theorem AlgebraicGeometry.LocallyRingedSpace.basicOpen_zero (X : AlgebraicGeometry.LocallyRingedSpace) (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) : AlgebraicGeometry.RingedSpace.basicOpen (AlgebraicGeometry.LocallyRingedSpace.toRingedSpace X) 0 = ⊥

instance AlgebraicGeometry.LocallyRingedSpace.component_nontrivial (X : AlgebraicGeometry.LocallyRingedSpace) (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) [hU : Nonempty { x // x ∈ U }] : Nontrivial ↑(X.presheaf.obj (Opposite.op U))