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).
- to_SheafedSpace : algebraic_geometry.SheafedSpace CommRing
- local_ring : ∀ (x : ↥(self.to_SheafedSpace.to_PresheafedSpace.carrier)), local_ring ↥(self.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 morphisms induced on stalks are local ring homomorphisms.
Instances for algebraic_geometry.LocallyRingedSpace
- algebraic_geometry.LocallyRingedSpace.has_sizeof_inst
- algebraic_geometry.LocallyRingedSpace.has_coe_to_sort
- algebraic_geometry.LocallyRingedSpace.quiver
- algebraic_geometry.LocallyRingedSpace.category_theory.category
- algebraic_geometry.LocallyRingedSpace.category_theory.limits.has_coproducts
- algebraic_geometry.LocallyRingedSpace.category_theory.limits.has_coequalizers
- algebraic_geometry.LocallyRingedSpace.category_theory.limits.has_colimits
An alias for to_SheafedSpace
, where the result type is a RingedSpace
.
This allows us to use dot-notation for the RingedSpace
namespace.
Equations
The underlying topological space of a locally ringed space.
Equations
The structure sheaf of a locally ringed space.
Equations
- X.𝒪 = X.to_SheafedSpace.sheaf
- val : X.to_SheafedSpace ⟶ Y.to_SheafedSpace
- prop : ∀ (x : ↥(X.to_SheafedSpace.to_PresheafedSpace)), is_local_ring_hom (algebraic_geometry.PresheafedSpace.stalk_map self.val x)
A morphism of locally ringed spaces is a morphism of ringed spaces such that the morphims induced on stalks are local ring homomorphisms.
Instances for algebraic_geometry.LocallyRingedSpace.hom
- algebraic_geometry.LocallyRingedSpace.hom.has_sizeof_inst
- algebraic_geometry.LocallyRingedSpace.hom.inhabited
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
.
Equations
Instances for algebraic_geometry.LocallyRingedSpace.stalk_map
The identity morphism on a locally ringed space.
Equations
Composition of morphisms of locally ringed spaces.
The category of locally ringed spaces.
Equations
- algebraic_geometry.LocallyRingedSpace.category_theory.category = {to_category_struct := {to_quiver := {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_1, map_comp' := algebraic_geometry.LocallyRingedSpace.forget_to_SheafedSpace._proof_2}
Instances for algebraic_geometry.LocallyRingedSpace.forget_to_SheafedSpace
- algebraic_geometry.LocallyRingedSpace.forget_to_SheafedSpace.category_theory.faithful
- algebraic_geometry.LocallyRingedSpace.forget_to_SheafedSpace.category_theory.reflects_isomorphisms
- algebraic_geometry.LocallyRingedSpace.is_open_immersion.forget_preserves_pullback_of_left
- algebraic_geometry.LocallyRingedSpace.is_open_immersion.forget_reflects_pullback_of_left
- algebraic_geometry.LocallyRingedSpace.is_open_immersion.forget_preserves_pullback_of_right
- algebraic_geometry.LocallyRingedSpace.is_open_immersion.forget_reflects_pullback_of_right
- algebraic_geometry.LocallyRingedSpace.forget_to_SheafedSpace.category_theory.limits.preserves_colimits_of_shape
- algebraic_geometry.LocallyRingedSpace.preserves_coequalizer
- algebraic_geometry.LocallyRingedSpace.forget_to_SheafedSpace.category_theory.limits.preserves_colimits
- algebraic_geometry.LocallyRingedSpace.glue_data.algebraic_geometry.LocallyRingedSpace.forget_to_SheafedSpace.category_theory.limits.preserves_limit
The forgetful functor from LocallyRingedSpace
to Top
.
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
.
Equations
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.
The restriction of a locally ringed space along an open embedding.
Equations
- X.restrict h = {to_SheafedSpace := X.to_SheafedSpace.restrict h, local_ring := _}
The canonical map from the restriction to the supspace.
Equations
- X.of_restrict h = {val := X.to_SheafedSpace.to_PresheafedSpace.of_restrict h, prop := _}
The restriction of a locally ringed space X
to the top subspace is isomorphic to X
itself.
The global sections, notated Gamma.