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.


A morphism between schemes is a morphism between the underlying locally ringed spaces.

@[protected, instance]

Schemes are a full subcategory of locally ringed spaces.

@[protected, reducible]

The structure sheaf of a 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

The empty scheme.