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

Equations
• = (X.toLocallyRingedSpace Y.toLocallyRingedSpace)
Instances For

Schemes are a full subcategory of locally ringed spaces.

Equations
• One or more equations did not get rendered due to their size.
@[inline, reducible]

The structure sheaf of a scheme.

Equations
Instances For
Equations
@[simp]

The forgetful functor from Scheme to LocallyRingedSpace.

Equations
Instances For
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem AlgebraicGeometry.Scheme.forgetToTop_obj :
= X.toSheafedSpace

The forgetful functor from Scheme to TopCat.

Equations
Instances For
Equations

forgetful functor to TopCat is the same as coercion

Equations
• = ( = X.toPresheafedSpace)
Instances For
@[simp]
@[simp]
theorem AlgebraicGeometry.Scheme.id_app (U : (TopologicalSpace.Opens X.toPresheafedSpace)ᵒᵖ) :
.val.c.app U = X.presheaf.map
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 )
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 .op) (CategoryTheory.CategoryStruct.comp (f.val.c.app ()) (X.presheaf.map .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 =
@[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 .op) (CategoryTheory.inv (f.val.c.app (Opposite.op ((TopologicalSpace.Opens.map .val.base).obj U))))
theorem AlgebraicGeometry.Scheme.inv_val_c_app_top (f : X Y) :
.val.c.app () = CategoryTheory.inv (f.val.c.app ())
@[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).

Equations
Instances For

The spectrum of a commutative ring, as a scheme.

Equations
• = { toLocallyRingedSpace := , local_affine := }
Instances For
@[simp]

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

Equations
Instances For

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

Equations
• One or more equations did not get rendered due to their size.
Instances For

The empty scheme.

Equations
• One or more equations did not get rendered due to their size.
Instances For

The global sections, notated Gamma.

Equations
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 ()
theorem AlgebraicGeometry.Scheme.Γ_map_op (f : X Y) :
f.op = f.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.

Equations
Instances For
@[simp]
theorem AlgebraicGeometry.Scheme.mem_basicOpen {U : TopologicalSpace.Opens X.toPresheafedSpace} (f : (X.presheaf.obj ())) (x : U) :
x X.basicOpen f 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) :
x X.basicOpen f ∃ (m : x U), 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) :
x X.basicOpen f 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 : ) :
X.basicOpen ((X.presheaf.map i) f) = V X.basicOpen f
@[simp]
theorem AlgebraicGeometry.Scheme.basicOpen_res_eq {V : TopologicalSpace.Opens X.toPresheafedSpace} {U : TopologicalSpace.Opens X.toPresheafedSpace} (f : (X.presheaf.obj ())) (i : ) :
X.basicOpen ((X.presheaf.map i) f) = X.basicOpen f
theorem AlgebraicGeometry.Scheme.basicOpen_le {U : TopologicalSpace.Opens X.toPresheafedSpace} (f : (X.presheaf.obj ())) :
X.basicOpen f U
theorem AlgebraicGeometry.Scheme.basicOpen_restrict {V : TopologicalSpace.Opens X.toPresheafedSpace} {U : TopologicalSpace.Opens X.toPresheafedSpace} (i : V U) (f : (X.presheaf.obj ())) :
X.basicOpen () X.basicOpen f
@[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 (Y.basicOpen r) = X.basicOpen ((f.val.c.app ()) r)
@[simp]
theorem AlgebraicGeometry.Scheme.basicOpen_zero (U : TopologicalSpace.Opens X.toPresheafedSpace) :
X.basicOpen 0 =
@[simp]
theorem AlgebraicGeometry.Scheme.basicOpen_mul {U : TopologicalSpace.Opens X.toPresheafedSpace} (f : (X.presheaf.obj ())) (g : (X.presheaf.obj ())) :
X.basicOpen (f * g) = X.basicOpen f X.basicOpen g
theorem AlgebraicGeometry.Scheme.basicOpen_of_isUnit {U : TopologicalSpace.Opens X.toPresheafedSpace} {f : (X.presheaf.obj ())} (hf : ) :
X.basicOpen f = U
instance AlgebraicGeometry.Scheme.algebra_section_section_basicOpen {U : TopologicalSpace.Opens X.toPresheafedSpace} (f : (X.presheaf.obj ())) :
Algebra (X.presheaf.obj ()) (X.presheaf.obj (Opposite.op (X.basicOpen f)))
Equations
theorem AlgebraicGeometry.basicOpen_eq_of_affine {R : CommRingCat} (f : R) :
().basicOpen (().inv f) =
@[simp]
theorem AlgebraicGeometry.basicOpen_eq_of_affine' {R : CommRingCat} (f : (.presheaf.obj ())) :
().basicOpen f = PrimeSpectrum.basicOpen (().hom f)
theorem AlgebraicGeometry.Scheme.Spec_map_presheaf_map_eqToHom {U : TopologicalSpace.Opens X.toPresheafedSpace} {V : TopologicalSpace.Opens X.toPresheafedSpace} (h : U = V) (W : (TopologicalSpace.Opens ( (Opposite.op (X.presheaf.obj ()))).toPresheafedSpace)ᵒᵖ) :
( (X.presheaf.map .op).op).val.c.app W =