# Documentation

Mathlib.AlgebraicGeometry.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 AlgebraicGeometry.Schemeextends :
Type (u_1 + 1)

We define Scheme as an 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.toLocallyRingedSpace.obj (op R) for some R : CommRingCat.

Instances For

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

Instances For

Schemes are a full subcategory of locally ringed spaces.

@[inline, reducible]

The structure sheaf of a scheme.

Instances For
@[simp]

The forgetful functor from Scheme to LocallyRingedSpace.

Instances For
@[simp]
theorem AlgebraicGeometry.Scheme.forgetToTop_obj :
= ().obj X.toSheafedSpace

The forgetful functor from Scheme to TopCat.

Instances For

forgetful functor to TopCat is the same as coercion

Instances For
@[simp]
theorem AlgebraicGeometry.Scheme.id_val_base :
().val.base = CategoryTheory.CategoryStruct.id X.toPresheafedSpace
@[simp]
theorem AlgebraicGeometry.Scheme.id_app (U : (TopologicalSpace.Opens X.toPresheafedSpace)ᵒᵖ) :
().val.c.app U = X.presheaf.map (CategoryTheory.eqToHom (_ : U = U))
theorem AlgebraicGeometry.Scheme.comp_val_assoc (f : X Y) (g : Y Z) (h : Z.toSheafedSpace Z) :
theorem AlgebraicGeometry.Scheme.comp_coeBase_assoc (f : X Y) (g : Y Z) {Z : TopCat} (h : Z.toPresheafedSpace Z) :
@[simp]
theorem AlgebraicGeometry.Scheme.comp_coeBase (f : X Y) (g : Y Z) :
().val.base = CategoryTheory.CategoryStruct.comp f.val.base g.val.base
theorem AlgebraicGeometry.Scheme.comp_val_base_assoc (f : X Y) (g : Y Z) {Z : TopCat} (h : Z.toPresheafedSpace Z) :
theorem AlgebraicGeometry.Scheme.comp_val_base (f : X Y) (g : Y Z) :
().val.base = CategoryTheory.CategoryStruct.comp f.val.base g.val.base
theorem AlgebraicGeometry.Scheme.comp_val_base_apply (f : X Y) (g : Y Z) (x : X.toPresheafedSpace) :
().val.base x = g.val.base (f.val.base x)
theorem AlgebraicGeometry.Scheme.comp_val_c_app_assoc (f : X Y) (g : Y Z) (U : (TopologicalSpace.Opens Z.toPresheafedSpace)ᵒᵖ) {Z : CommRingCat} (h : (().val.base _* X.presheaf).obj U Z) :
@[simp]
theorem AlgebraicGeometry.Scheme.comp_val_c_app (f : X Y) (g : Y Z) (U : (TopologicalSpace.Opens Z.toPresheafedSpace)ᵒᵖ) :
().val.c.app U = CategoryTheory.CategoryStruct.comp (g.val.c.app U) (f.val.c.app ((TopologicalSpace.Opens.map g.val.base).op.obj U))
theorem AlgebraicGeometry.Scheme.congr_app {f : X Y} {g : X Y} (e : f = g) (U : (TopologicalSpace.Opens Y.toPresheafedSpace)ᵒᵖ) :
f.val.c.app U = CategoryTheory.CategoryStruct.comp (g.val.c.app U) (X.presheaf.map (CategoryTheory.eqToHom (_ : (TopologicalSpace.Opens.map g.val.base).op.obj U = (TopologicalSpace.Opens.map f.val.base).op.obj U)))
theorem AlgebraicGeometry.Scheme.app_eq (f : X Y) {U : TopologicalSpace.Opens Y.toPresheafedSpace} {V : TopologicalSpace.Opens Y.toPresheafedSpace} (e : U = V) :
f.val.c.app () = CategoryTheory.CategoryStruct.comp (Y.presheaf.map (CategoryTheory.eqToHom (_ : V = U)).op) (CategoryTheory.CategoryStruct.comp (f.val.c.app ()) (X.presheaf.map (CategoryTheory.eqToHom (_ : (TopologicalSpace.Opens.map f.val.base).obj U = (TopologicalSpace.Opens.map f.val.base).obj V)).op))
theorem AlgebraicGeometry.Scheme.presheaf_map_eqToHom_op (U : TopologicalSpace.Opens X.toPresheafedSpace) (V : TopologicalSpace.Opens X.toPresheafedSpace) (i : U = V) :
X.presheaf.map ().op = CategoryTheory.eqToHom (_ : X.presheaf.obj () = X.presheaf.obj ())
@[simp]
theorem AlgebraicGeometry.Scheme.inv_val_c_app (f : X Y) (U : TopologicalSpace.Opens X.toPresheafedSpace) :
().val.c.app () = CategoryTheory.CategoryStruct.comp (X.presheaf.map (CategoryTheory.eqToHom (_ : ().obj U = U)).op) (CategoryTheory.inv (f.val.c.app (Opposite.op ((TopologicalSpace.Opens.map ().val.base).obj U))))
@[inline, reducible]
abbrev AlgebraicGeometry.Scheme.Hom.appLe (f : X Y) {V : TopologicalSpace.Opens X.toPresheafedSpace} {U : TopologicalSpace.Opens Y.toPresheafedSpace} (e : V (TopologicalSpace.Opens.map f.val.base).obj U) :
Y.presheaf.obj () X.presheaf.obj ()

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

Instances For

The spectrum of a commutative ring, as a scheme.

Instances For
@[simp]

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

Instances For

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

Instances For

The empty scheme.

Instances For

The global sections, notated Gamma.

Instances For
@[simp]
theorem AlgebraicGeometry.Scheme.Γ_obj :
= X.unop.presheaf.obj ()
theorem AlgebraicGeometry.Scheme.Γ_obj_op :
= X.presheaf.obj ()
@[simp]
theorem AlgebraicGeometry.Scheme.Γ_map (f : X Y) :
= f.unop.val.c.app ()
def AlgebraicGeometry.Scheme.basicOpen {U : TopologicalSpace.Opens X.toPresheafedSpace} (f : ↑(X.presheaf.obj ())) :
TopologicalSpace.Opens X.toPresheafedSpace

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

Instances For
@[simp]
theorem AlgebraicGeometry.Scheme.mem_basicOpen {U : TopologicalSpace.Opens X.toPresheafedSpace} (f : ↑(X.presheaf.obj ())) (x : { x // x U }) :
IsUnit (↑(TopCat.Presheaf.germ X.presheaf x) f)
theorem AlgebraicGeometry.Scheme.mem_basicOpen_top' {U : TopologicalSpace.Opens X.toPresheafedSpace} (f : ↑(X.presheaf.obj ())) (x : X.toPresheafedSpace) :
m, IsUnit (↑(TopCat.Presheaf.germ X.presheaf { val := x, property := m }) f)
@[simp]
theorem AlgebraicGeometry.Scheme.mem_basicOpen_top (f : ↑(X.presheaf.obj ())) (x : X.toPresheafedSpace) :
IsUnit (↑(TopCat.Presheaf.germ X.presheaf { val := x, property := trivial }) f)
@[simp]
theorem AlgebraicGeometry.Scheme.basicOpen_res {V : TopologicalSpace.Opens X.toPresheafedSpace} {U : TopologicalSpace.Opens X.toPresheafedSpace} (f : ↑(X.presheaf.obj ())) (i : ) :
AlgebraicGeometry.Scheme.basicOpen X (↑(X.presheaf.map i) f) =
@[simp]
theorem AlgebraicGeometry.Scheme.basicOpen_res_eq {V : TopologicalSpace.Opens X.toPresheafedSpace} {U : TopologicalSpace.Opens X.toPresheafedSpace} (f : ↑(X.presheaf.obj ())) (i : ) :
AlgebraicGeometry.Scheme.basicOpen X (↑(X.presheaf.map i) f) =
theorem AlgebraicGeometry.Scheme.basicOpen_le {U : TopologicalSpace.Opens X.toPresheafedSpace} (f : ↑(X.presheaf.obj ())) :
@[simp]
theorem AlgebraicGeometry.Scheme.preimage_basicOpen (f : X Y) {U : TopologicalSpace.Opens Y.toPresheafedSpace} (r : ↑(Y.presheaf.obj ())) :
(TopologicalSpace.Opens.map f.val.base).obj () = AlgebraicGeometry.Scheme.basicOpen X (↑(f.val.c.app ()) r)
@[simp]
theorem AlgebraicGeometry.Scheme.basicOpen_zero (U : TopologicalSpace.Opens X.toPresheafedSpace) :
@[simp]
theorem AlgebraicGeometry.Scheme.basicOpen_mul {U : TopologicalSpace.Opens X.toPresheafedSpace} (f : ↑(X.presheaf.obj ())) (g : ↑(X.presheaf.obj ())) :
theorem AlgebraicGeometry.Scheme.basicOpen_of_isUnit {U : TopologicalSpace.Opens X.toPresheafedSpace} {f : ↑(X.presheaf.obj ())} (hf : ) :
@[simp]
theorem AlgebraicGeometry.basicOpen_eq_of_affine' {R : CommRingCat} (f : ↑(().presheaf.obj ())) :