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).
Future work
- Define the restriction along an open embedding
- to_SheafedSpace : algebraic_geometry.SheafedSpace CommRing
- local_ring : ∀ (x : ↥(c.to_SheafedSpace.to_PresheafedSpace.carrier)), local_ring ↥(c.to_SheafedSpace.to_PresheafedSpace.presheaf.stalk x)
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 morphims induced on stalks are local ring homomorphisms.
The underlying topological space of a locally ringed space.
Equations
Equations
- algebraic_geometry.LocallyRingedSpace.has_coe_to_sort = {S := Type u, coe := λ (X : algebraic_geometry.LocallyRingedSpace), ↥(X.to_Top)}
The structure sheaf of a locally ringed space.
Equations
- X.𝒪 = X.to_SheafedSpace.sheaf
A morphism of locally ringed spaces is a morphism of ringed spaces such that the morphims induced on stalks are local ring homomorphisms.
Equations
- X.hom Y = {f // ∀ (x : ↥(X.to_SheafedSpace.to_PresheafedSpace)), is_local_ring_hom (algebraic_geometry.PresheafedSpace.stalk_map f x)}
The stalk of a locally ringed space, just as a CommRing.
Equations
- X.stalk x = X.to_SheafedSpace.to_PresheafedSpace.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.
The identity morphism on a locally ringed space.
Equations
- X.id = ⟨𝟙 X.to_SheafedSpace, _⟩
Composition of morphisms of locally ringed spaces.
The category of locally ringed spaces.
Equations
- algebraic_geometry.LocallyRingedSpace.category_theory.category = {to_category_struct := {to_has_hom := {hom := algebraic_geometry.LocallyRingedSpace.hom}, id := algebraic_geometry.LocallyRingedSpace.id, comp := λ (X Y Z : algebraic_geometry.LocallyRingedSpace) (f : X ⟶ Y) (g : Y ⟶ Z), algebraic_geometry.LocallyRingedSpace.comp f g}, id_comp' := algebraic_geometry.LocallyRingedSpace.category_theory.category._proof_1, comp_id' := algebraic_geometry.LocallyRingedSpace.category_theory.category._proof_2, assoc' := algebraic_geometry.LocallyRingedSpace.category_theory.category._proof_3}
The forgetful functor from LocallyRingedSpace to SheafedSpace CommRing.
Equations
- algebraic_geometry.LocallyRingedSpace.forget_to_SheafedSpace = {obj := λ (X : algebraic_geometry.LocallyRingedSpace), X.to_SheafedSpace, map := λ (X Y : algebraic_geometry.LocallyRingedSpace) (f : X ⟶ Y), f.val, map_id' := algebraic_geometry.LocallyRingedSpace.forget_to_SheafedSpace._proof_5, map_comp' := algebraic_geometry.LocallyRingedSpace.forget_to_SheafedSpace._proof_6}
The global sections, notated Gamma.