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 of schemes is just a morphism of the underlying locally ringed spaces.
- carrier : TopCat
- IsSheaf : TopCat.Presheaf.IsSheaf s.presheaf
- local_affine : ∀ (x : ↑(AlgebraicGeometry.LocallyRingedSpace.toTopCat s.toLocallyRingedSpace)), ∃ U R, Nonempty (AlgebraicGeometry.LocallyRingedSpace.restrict s.toLocallyRingedSpace (_ : OpenEmbedding ↑(TopologicalSpace.Opens.inclusion U.obj)) ≅ AlgebraicGeometry.Spec.toLocallyRingedSpace.obj (Opposite.op R))
Scheme as an
X : LocallyRingedSpace,
along with a proof that every point has an open neighbourhood
so that that the restriction of
U is isomorphic,
as a locally ringed space, to
Spec.toLocallyRingedSpace.obj (op R)
R : CommRingCat.
The forgetful functor from
Given a morphism of schemes
f : X ⟶ Y, and open sets
U ⊆ Y,
V ⊆ f ⁻¹' U,
this is the induced map
Γ(Y, U) ⟶ Γ(X, V).