mathlib3 documentation


The category of schemes #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.