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 of schemes is just a morphism of the underlying locally ringed spaces.
- carrier : TopCat
- presheaf : TopCat.Presheaf CommRingCat ↑s.toPresheafedSpace
- IsSheaf : TopCat.Presheaf.IsSheaf s.presheaf
- localRing : ∀ (x : ↑↑s.toPresheafedSpace), LocalRing ↑(TopCat.Presheaf.stalk s.presheaf x)
- 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))
We define Scheme
as an 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 locally ringed space, to Spec.toLocallyRingedSpace.obj (op R)
for some R : CommRingCat
.
Instances For
A morphism between schemes is a morphism between the underlying locally ringed spaces.
Instances For
Schemes are a full subcategory of locally ringed spaces.
The structure sheaf of a scheme.
Instances For
The forgetful functor from Scheme
to LocallyRingedSpace
.
Instances For
forgetful functor to TopCat
is the same as coercion
Instances For
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)
.
Instances For
The spectrum of a commutative ring, as a scheme.
Instances For
The induced map of a ring homomorphism on the ring spectra, as a morphism of schemes.
Instances For
The spectrum, as a contravariant functor from commutative rings to schemes.
Instances For
The global sections, notated Gamma.
Instances For
The subset of the underlying space where the given section does not vanish.