mathlib documentation


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.

structure algebraic_geometry.Scheme  :
Type (u_1+1)

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 locally ringed space, to Spec.to_LocallyRingedSpace.obj (op R) for some R : CommRing.

Instances for algebraic_geometry.Scheme
theorem algebraic_geometry.Scheme.comp_val {X Y Z : algebraic_geometry.Scheme} (f : X Y) (g : Y Z) :
(f g).val = f.val g.val

The induced map of a ring homomorphism on the ring spectra, as a morphism of schemes.


The spectrum, as a contravariant functor from commutative rings to schemes.

Instances for algebraic_geometry.Scheme.Spec