# mathlib3documentation

algebraic_geometry.Scheme

# 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.

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
@[nolint]

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

Equations
@[protected, instance]

Schemes are a full subcategory of locally ringed spaces.

Equations
@[protected, reducible]

The structure sheaf of a Scheme.

The forgetful functor from Scheme to LocallyRingedSpace.

Equations
Instances for algebraic_geometry.Scheme.forget_to_LocallyRingedSpace
@[simp]
@[simp]

The forgetful functor from Scheme to Top.

Equations
Instances for algebraic_geometry.Scheme.forget_to_Top
@[simp]
@[simp]
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
@[simp]
theorem algebraic_geometry.Scheme.comp_val_base_apply {X Y Z : algebraic_geometry.Scheme} (f : X Y) (g : Y Z)  :
((f g).val.base) x = (g.val.base) ((f.val.base) x)
theorem algebraic_geometry.Scheme.comp_val_c_app_assoc {X Y Z : algebraic_geometry.Scheme} (f : X Y) (g : Y Z) {X' : CommRing} (f' : U X') :
(f g).val.c.app U f' = g.val.c.app U f.val.c.app U) f'
@[simp]
theorem algebraic_geometry.Scheme.comp_val_c_app {X Y Z : algebraic_geometry.Scheme} (f : X Y) (g : Y Z)  :
(f g).val.c.app U = g.val.c.app U f.val.c.app U)
theorem algebraic_geometry.Scheme.congr_app {X Y : algebraic_geometry.Scheme} {f g : X Y} (e : f = g)  :
theorem algebraic_geometry.Scheme.app_eq {X Y : algebraic_geometry.Scheme} (f : X Y) (e : U = V) :
@[protected, instance]
@[simp]
@[reducible]

Given a morphism of schemes f : X ⟶ Y, and open sets U ⊆ Y, V ⊆ f ⁻¹' U, this is the induced map Γ(Y, U) ⟶ Γ(X, V).

The spectrum of a commutative ring, as a scheme.

Equations
noncomputable def algebraic_geometry.Scheme.Spec_map {R S : CommRing} (f : R S) :

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) :
noncomputable def algebraic_geometry.Scheme.Spec  :

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

Equations
Instances for algebraic_geometry.Scheme.Spec

The empty scheme.

Equations
@[protected, instance]
Equations
@[protected, instance]
Equations

The global sections, notated Gamma.

Equations
@[simp]

The subset of the underlying space where the given section does not vanish.

Equations
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]