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).
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
- AlgebraicGeometry.LocallyRingedSpace.instCategory
- AlgebraicGeometry.LocallyRingedSpace.instCoeSortType
- AlgebraicGeometry.LocallyRingedSpace.instEmptyCollection
- AlgebraicGeometry.LocallyRingedSpace.instHasCoequalizers
- AlgebraicGeometry.LocallyRingedSpace.instHasColimits
- AlgebraicGeometry.LocallyRingedSpace.instHasCoproducts
- AlgebraicGeometry.LocallyRingedSpace.instQuiver
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
The underlying topological space of a locally ringed space.
Equations
- X.toTopCat = ↑X.toPresheafedSpace
Equations
- AlgebraicGeometry.LocallyRingedSpace.instCoeSortType = { coe := fun (X : AlgebraicGeometry.LocallyRingedSpace) => ↑X.toTopCat }
Equations
- ⋯ = ⋯
The structure sheaf of a locally ringed space.
Equations
- X.𝒪 = X.sheaf
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), IsLocalRingHom (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap self.val x)
the underlying morphism induces a local ring homomorphism on stalks
the underlying morphism induces a local ring homomorphism on stalks
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 = AlgebraicGeometry.PresheafedSpace.Hom.stalkMap f.val x
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
The identity morphism on a locally ringed space.
Equations
- X.id = { val := CategoryTheory.CategoryStruct.id X.toSheafedSpace, prop := ⋯ }
Equations
- X.instInhabitedHom = { default := X.id }
Composition of morphisms of locally ringed spaces.
Equations
- AlgebraicGeometry.LocallyRingedSpace.comp f g = { val := CategoryTheory.CategoryStruct.comp f.val g.val, prop := ⋯ }
The category of locally ringed spaces.
Equations
- One or more equations did not get rendered due to their size.
The forgetful functor from LocallyRingedSpace
to SheafedSpace CommRing
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
- AlgebraicGeometry.LocallyRingedSpace.GlueData.instPreservesLimitSheafedSpaceCommRingCatWalkingCospanCospanFForgetToSheafedSpace
- AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forgetPreservesPullbackOfLeft
- AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forgetPreservesPullbackOfRight
- AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forgetReflectsPullbackOfLeft
- AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forgetReflectsPullbackOfRight
- AlgebraicGeometry.LocallyRingedSpace.instFaithfulSheafedSpaceCommRingCatForgetToSheafedSpace
- AlgebraicGeometry.LocallyRingedSpace.instPreservesColimitsOfShapeSheafedSpaceCommRingCatDiscreteForgetToSheafedSpace
- AlgebraicGeometry.LocallyRingedSpace.instReflectsIsomorphismsSheafedSpaceCommRingCatForgetToSheafedSpace
- AlgebraicGeometry.LocallyRingedSpace.preservesCoequalizer
- AlgebraicGeometry.LocallyRingedSpace.preservesColimits_forgetToSheafedSpace
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 isoOfSheafedSpaceIso
.
Equations
- AlgebraicGeometry.LocallyRingedSpace.homOfSheafedSpaceHomOfIsIso f = { val := f, prop := ⋯ }
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.
Equations
- ⋯ = ⋯
The restriction of a locally ringed space along an open embedding.
Equations
- X.restrict h = { toSheafedSpace := X.restrict h, localRing := ⋯ }
The canonical map from the restriction to the subspace.
Equations
- X.ofRestrict h = { val := X.ofRestrict h, prop := ⋯ }
The restriction of a locally ringed space X
to the top subspace is isomorphic to X
itself.
Equations
- X.restrictTopIso = AlgebraicGeometry.LocallyRingedSpace.isoOfSheafedSpaceIso X.restrictTopIso
The global sections, notated Gamma.
Equations
- AlgebraicGeometry.LocallyRingedSpace.Γ = AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace.op.comp AlgebraicGeometry.SheafedSpace.Γ
The empty locally ringed space.
Equations
- One or more equations did not get rendered due to their size.
The canonical map from the empty locally ringed space.
Equations
- One or more equations did not get rendered due to their size.
Equations
- AlgebraicGeometry.LocallyRingedSpace.instUniqueHomEmptyCollection = { default := X.emptyTo, uniq := ⋯ }
The empty space is initial in LocallyRingedSpace
.
Equations
- ⋯ = ⋯
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
Equations
- ⋯ = ⋯