The category of schemes
A scheme is a locally ringed space such that every point is contained in some open set
where there is an isomorphism of presheaves between the restriction to that open set,
and the structure sheaf of Spec R, for some commutative ring R.
A morphism is schemes is just a morphism of the underlying locally ringed spaces.
- X : algebraic_geometry.LocallyRingedSpace
- local_affine : ∀ (x : ↥(c.X.to_SheafedSpace.to_PresheafedSpace.carrier)), ∃ (U : topological_space.opens ↥(c.X.to_SheafedSpace.to_PresheafedSpace.carrier)) (m : x ∈ U) (R : CommRing) (i : c.X.to_SheafedSpace.to_PresheafedSpace.restrict U.inclusion _ ≅ algebraic_geometry.Spec.PresheafedSpace R), true
We define Scheme as a X : LocallyRingedSpace,
along with a proof that every point has an open neighbourhood U
so that that the restriction of X to U is isomorphic, as a space with a presheaf of commutative rings,
to Spec.PresheafedSpace R for some R : CommRing.
(Note we're not asking in the definition that this is an isomorphism as locally ringed spaces, although that is a consequence.)
Every Scheme is a LocallyRingedSpace.
Equations
- S.to_LocallyRingedSpace = {to_SheafedSpace := S.X.to_SheafedSpace, local_ring := _}
Spec R as a Scheme.
Equations
- algebraic_geometry.Scheme.Spec R = {X := {to_SheafedSpace := (algebraic_geometry.Spec.LocallyRingedSpace R).to_SheafedSpace, local_ring := _}, local_affine := _}
The empty scheme, as Spec 0.
Equations
Schemes are a full subcategory of locally ringed spaces.
The global sections, notated Gamma.