# mathlibdocumentation

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 (max (u_1+1) (u_2+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 space with a presheaf of commutative rings, to 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.)

Every Scheme is a LocallyRingedSpace.

Equations
@[instance]

Schemes are a full subcategory of locally ringed spaces.

Equations

The spectrum of a commutative ring, as a scheme.

Equations

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

Equations
@[simp]
theorem algebraic_geometry.Scheme.Spec_map_comp {R S T : CommRing} (f : R S) (g : S T) :
@[simp]

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

Equations
@[simp]

The empty scheme, as Spec 0.

Equations
@[instance]
Equations
@[instance]
Equations

The global sections, notated Gamma.

Equations
@[simp]