mathlib documentation

algebraic_geometry.Scheme

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.

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

Equations

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

Equations