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
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
Scheme as a
X : LocallyRingedSpace,
along with a proof that every point has an open neighbourhood
so that that the restriction of
U is isomorphic, as a space with a presheaf of commutative rings,
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.)
Schemes are a full subcategory of locally ringed spaces.