mathlib3 documentation

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)

to_LocallyRingedSpace : algebraic_geometry.LocallyRingedSpace
local_affine : ∀ (x : ↥(self.to_LocallyRingedSpace)), ∃ (U : topological_space.open_nhds x) (R : CommRing), nonempty (self.to_LocallyRingedSpace.restrict _ ≅ algebraic_geometry.Spec.to_LocallyRingedSpace.obj (opposite.op R))

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]

def algebraic_geometry.Scheme.hom (X Y : algebraic_geometry.Scheme) :

Type u_1

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

Equations

X.hom Y = (X.to_LocallyRingedSpace ⟶ Y.to_LocallyRingedSpace)

@[protected, instance]

def algebraic_geometry.Scheme.category_theory.category :

category_theory.category algebraic_geometry.Scheme

Schemes are a full subcategory of locally ringed spaces.

Equations

algebraic_geometry.Scheme.category_theory.category = {to_category_struct := {to_quiver := {hom := algebraic_geometry.Scheme.hom}, id := 𝟙, comp := category_theory.category_struct.comp category_theory.category.to_category_struct}, id_comp' := algebraic_geometry.Scheme.category_theory.category._proof_1, comp_id' := algebraic_geometry.Scheme.category_theory.category._proof_2, assoc' := algebraic_geometry.Scheme.category_theory.category._proof_3}

@[protected, reducible]

def algebraic_geometry.Scheme.sheaf (X : algebraic_geometry.Scheme) :

Top.sheaf CommRing ↑(X.to_LocallyRingedSpace.to_SheafedSpace)

The structure sheaf of a Scheme.

@[protected, instance]

def algebraic_geometry.Scheme.forget_to_LocallyRingedSpace.full :

category_theory.full algebraic_geometry.Scheme.forget_to_LocallyRingedSpace

@[simp]

theorem algebraic_geometry.Scheme.forget_to_LocallyRingedSpace_map (x y : category_theory.induced_category algebraic_geometry.LocallyRingedSpace algebraic_geometry.Scheme.to_LocallyRingedSpace) (f : x ⟶ y) :

algebraic_geometry.Scheme.forget_to_LocallyRingedSpace.map f = f

def algebraic_geometry.Scheme.forget_to_LocallyRingedSpace :

algebraic_geometry.Scheme ⥤ algebraic_geometry.LocallyRingedSpace

The forgetful functor from Scheme to LocallyRingedSpace.

Equations

algebraic_geometry.Scheme.forget_to_LocallyRingedSpace = category_theory.induced_functor algebraic_geometry.Scheme.to_LocallyRingedSpace

Instances for algebraic_geometry.Scheme.forget_to_LocallyRingedSpace

@[simp]

theorem algebraic_geometry.Scheme.forget_to_LocallyRingedSpace_obj (self : algebraic_geometry.Scheme) :

algebraic_geometry.Scheme.forget_to_LocallyRingedSpace.obj self = self.to_LocallyRingedSpace

@[protected, instance]

def algebraic_geometry.Scheme.forget_to_LocallyRingedSpace.faithful :

category_theory.faithful algebraic_geometry.Scheme.forget_to_LocallyRingedSpace

@[simp]

theorem algebraic_geometry.Scheme.forget_to_LocallyRingedSpace_preimage {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y) :

algebraic_geometry.Scheme.forget_to_LocallyRingedSpace.preimage f = f

def algebraic_geometry.Scheme.forget_to_Top :

algebraic_geometry.Scheme ⥤ Top

The forgetful functor from Scheme to Top.

Equations

algebraic_geometry.Scheme.forget_to_Top = algebraic_geometry.Scheme.forget_to_LocallyRingedSpace ⋙ algebraic_geometry.LocallyRingedSpace.forget_to_Top

Instances for algebraic_geometry.Scheme.forget_to_Top

@[simp]

theorem algebraic_geometry.Scheme.forget_to_Top_obj (X : algebraic_geometry.Scheme) :

algebraic_geometry.Scheme.forget_to_Top.obj X = (algebraic_geometry.SheafedSpace.forget CommRing).obj X.to_LocallyRingedSpace.to_SheafedSpace

@[simp]

theorem algebraic_geometry.Scheme.forget_to_Top_map (_x _x_1 : algebraic_geometry.Scheme) (f : _x ⟶ _x_1) :

algebraic_geometry.Scheme.forget_to_Top.map f = (algebraic_geometry.SheafedSpace.forget CommRing).map f.val

@[simp]

theorem algebraic_geometry.Scheme.id_val_base (X : algebraic_geometry.Scheme) :

(𝟙 X).val.base = 𝟙 ↑(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace)

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

theorem algebraic_geometry.Scheme.comp_val_assoc {X Y Z : algebraic_geometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) {X' : algebraic_geometry.SheafedSpace CommRing} (f' : Z.to_LocallyRingedSpace.to_SheafedSpace ⟶ X') :

(f ≫ g).val ≫ f' = f.val ≫ g.val ≫ f'

theorem algebraic_geometry.Scheme.comp_coe_base_assoc {X Y Z : algebraic_geometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) {X' : Top} (f' : ↑(Z.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace) ⟶ X') :

(f ≫ g).val.base ≫ f' = f.val.base ≫ g.val.base ≫ f'

@[simp]

theorem algebraic_geometry.Scheme.comp_coe_base {X Y Z : algebraic_geometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) :

(f ≫ g).val.base = f.val.base ≫ g.val.base

theorem algebraic_geometry.Scheme.comp_val_base_assoc {X Y Z : algebraic_geometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) {X' : Top} (f' : ↑(Z.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace) ⟶ X') :

(f ≫ g).val.base ≫ f' = f.val.base ≫ g.val.base ≫ f'

theorem algebraic_geometry.Scheme.comp_val_base_apply {X Y Z : algebraic_geometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (x : ↥↑(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace)) :

⇑((f ≫ g).val.base) x = ⇑(g.val.base) (⇑(f.val.base) x)

theorem algebraic_geometry.Scheme.comp_val_base {X Y Z : algebraic_geometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) :

(f ≫ g).val.base = f.val.base ≫ g.val.base

theorem algebraic_geometry.Scheme.comp_val_c_app_assoc {X Y Z : algebraic_geometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (U : (topological_space.opens ↥(Z.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier))ᵒᵖ) {X' : CommRing} (f' : ((f ≫ g).val.base _* X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf).obj U ⟶ X') :

(f ≫ g).val.c.app U ≫ f' = g.val.c.app U ≫ f.val.c.app ((topological_space.opens.map g.val.base).op.obj U) ≫ f'

@[simp]

theorem algebraic_geometry.Scheme.comp_val_c_app {X Y Z : algebraic_geometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (U : (topological_space.opens ↥(Z.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier))ᵒᵖ) :

(f ≫ g).val.c.app U = g.val.c.app U ≫ f.val.c.app ((topological_space.opens.map g.val.base).op.obj U)

theorem algebraic_geometry.Scheme.congr_app {X Y : algebraic_geometry.Scheme} {f g : X ⟶ Y} (e : f = g) (U : (topological_space.opens ↥(Y.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier))ᵒᵖ) :

f.val.c.app U = g.val.c.app U ≫ X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.map (category_theory.eq_to_hom _)

theorem algebraic_geometry.Scheme.app_eq {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y) {U V : topological_space.opens ↥(Y.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)} (e : U = V) :

@[protected, instance]

def algebraic_geometry.Scheme.is_LocallyRingedSpace_iso {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y) [category_theory.is_iso f] :

category_theory.is_iso f

@[simp]

theorem algebraic_geometry.Scheme.inv_val_c_app {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y) [category_theory.is_iso f] (U : topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)) :

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

def algebraic_geometry.Scheme.Spec_obj (R : CommRing) :

algebraic_geometry.Scheme

The spectrum of a commutative ring, as a scheme.

Equations

algebraic_geometry.Scheme.Spec_obj R = {to_LocallyRingedSpace := algebraic_geometry.Spec.LocallyRingedSpace_obj R, local_affine := _}

@[simp]

theorem algebraic_geometry.Scheme.Spec_obj_to_LocallyRingedSpace (R : CommRing) :

(algebraic_geometry.Scheme.Spec_obj R).to_LocallyRingedSpace = algebraic_geometry.Spec.LocallyRingedSpace_obj R

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

algebraic_geometry.Scheme.Spec_obj S ⟶ algebraic_geometry.Scheme.Spec_obj R

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

Equations

algebraic_geometry.Scheme.Spec_map f = algebraic_geometry.Spec.LocallyRingedSpace_map f

@[simp]

theorem algebraic_geometry.Scheme.Spec_map_id (R : CommRing) :

algebraic_geometry.Scheme.Spec_map (𝟙 R) = 𝟙 (algebraic_geometry.Scheme.Spec_obj R)

theorem algebraic_geometry.Scheme.Spec_map_comp {R S T : CommRing} (f : R ⟶ S) (g : S ⟶ T) :

algebraic_geometry.Scheme.Spec_map (f ≫ g) = algebraic_geometry.Scheme.Spec_map g ≫ algebraic_geometry.Scheme.Spec_map f

theorem algebraic_geometry.Scheme.Spec_map_2 (R S : CommRing ᵒᵖ) (f : R ⟶ S) :

algebraic_geometry.Scheme.Spec.map f = algebraic_geometry.Scheme.Spec_map f.unop

noncomputable def algebraic_geometry.Scheme.Spec :

CommRing ᵒᵖ ⥤ algebraic_geometry.Scheme

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

Equations

algebraic_geometry.Scheme.Spec = {obj := λ (R : CommRing ᵒᵖ), algebraic_geometry.Scheme.Spec_obj (opposite.unop R), map := λ (R S : CommRing ᵒᵖ) (f : R ⟶ S), algebraic_geometry.Scheme.Spec_map f.unop, map_id' := algebraic_geometry.Scheme.Spec._proof_1, map_comp' := algebraic_geometry.Scheme.Spec._proof_2}

Instances for algebraic_geometry.Scheme.Spec

theorem algebraic_geometry.Scheme.Spec_obj_2 (R : CommRing ᵒᵖ) :

algebraic_geometry.Scheme.Spec.obj R = algebraic_geometry.Scheme.Spec_obj (opposite.unop R)

@[simp]

theorem algebraic_geometry.Scheme.empty_to_LocallyRingedSpace_to_SheafedSpace_to_PresheafedSpace_presheaf :

algebraic_geometry.Scheme.empty.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf = (category_theory.functor.const (topological_space.opens ↥(Top.of pempty))ᵒᵖ).obj (CommRing.of punit)

def algebraic_geometry.Scheme.empty :

algebraic_geometry.Scheme

The empty scheme.

Equations

algebraic_geometry.Scheme.empty = {to_LocallyRingedSpace := {to_SheafedSpace := {to_PresheafedSpace := {carrier := Top.of pempty pempty.topological_space, presheaf := (category_theory.functor.const (topological_space.opens ↥(Top.of pempty))ᵒᵖ).obj (CommRing.of punit)}, is_sheaf := algebraic_geometry.Scheme.empty._proof_1}, local_ring := algebraic_geometry.Scheme.empty._proof_2}, local_affine := algebraic_geometry.Scheme.empty._proof_3}

@[simp]

theorem algebraic_geometry.Scheme.empty_to_LocallyRingedSpace_to_SheafedSpace_to_PresheafedSpace_carrier :

algebraic_geometry.Scheme.empty.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier = Top.of pempty

@[protected, instance]

def algebraic_geometry.Scheme.has_emptyc :

has_emptyc algebraic_geometry.Scheme

Equations

algebraic_geometry.Scheme.has_emptyc = {emptyc := algebraic_geometry.Scheme.empty}

@[protected, instance]

def algebraic_geometry.Scheme.inhabited :

inhabited algebraic_geometry.Scheme

Equations

algebraic_geometry.Scheme.inhabited = {default := ∅}

def algebraic_geometry.Scheme.Γ :

algebraic_geometry.Scheme ᵒᵖ ⥤ CommRing

The global sections, notated Gamma.

Equations

algebraic_geometry.Scheme.Γ = (category_theory.induced_functor algebraic_geometry.Scheme.to_LocallyRingedSpace).op ⋙ algebraic_geometry.LocallyRingedSpace.Γ

theorem algebraic_geometry.Scheme.Γ_def :

algebraic_geometry.Scheme.Γ = (category_theory.induced_functor algebraic_geometry.Scheme.to_LocallyRingedSpace).op ⋙ algebraic_geometry.LocallyRingedSpace.Γ

@[simp]

theorem algebraic_geometry.Scheme.Γ_obj (X : algebraic_geometry.Scheme ᵒᵖ) :

algebraic_geometry.Scheme.Γ.obj X = (opposite.unop X).to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op ⊤)

theorem algebraic_geometry.Scheme.Γ_obj_op (X : algebraic_geometry.Scheme) :

algebraic_geometry.Scheme.Γ.obj (opposite.op X) = X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op ⊤)

@[simp]

theorem algebraic_geometry.Scheme.Γ_map {X Y : algebraic_geometry.Scheme ᵒᵖ} (f : X ⟶ Y) :

algebraic_geometry.Scheme.Γ.map f = f.unop.val.c.app (opposite.op ⊤)

theorem algebraic_geometry.Scheme.Γ_map_op {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y) :

algebraic_geometry.Scheme.Γ.map f.op = f.val.c.app (opposite.op ⊤)

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

Equations

X.basic_open f = X.to_LocallyRingedSpace.to_RingedSpace.basic_open f

@[simp]

theorem algebraic_geometry.Scheme.mem_basic_open (X : algebraic_geometry.Scheme) {U : topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)} (f : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op U))) (x : ↥U) :

↑x ∈ X.basic_open f ↔ is_unit (⇑(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.germ x) f)

@[simp]

theorem algebraic_geometry.Scheme.mem_basic_open_top (X : algebraic_geometry.Scheme) (f : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op ⊤))) (x : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)) :

x ∈ X.basic_open f ↔ is_unit (⇑(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.germ ⟨x, trivial⟩) f)

@[simp]

theorem algebraic_geometry.Scheme.basic_open_res (X : algebraic_geometry.Scheme) {V U : topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)} (f : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op U))) (i : opposite.op U ⟶ opposite.op V) :

X.basic_open (⇑(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.map i) f) = V ⊓ X.basic_open f

@[simp]

theorem algebraic_geometry.Scheme.basic_open_res_eq (X : algebraic_geometry.Scheme) {V U : topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)} (f : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op U))) (i : opposite.op U ⟶ opposite.op V) [category_theory.is_iso i] :

X.basic_open (⇑(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.map i) f) = X.basic_open f

theorem algebraic_geometry.Scheme.basic_open_le (X : algebraic_geometry.Scheme) {U : topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)} (f : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op U))) :

X.basic_open f ≤ U

@[simp]

theorem algebraic_geometry.Scheme.preimage_basic_open {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y) {U : topological_space.opens ↥(Y.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)} (r : ↥(Y.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op U))) :

(topological_space.opens.map f.val.base).obj (Y.basic_open r) = X.basic_open (⇑(f.val.c.app (opposite.op U)) r)

@[simp]

theorem algebraic_geometry.Scheme.basic_open_zero (X : algebraic_geometry.Scheme) (U : topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)) :

X.basic_open 0 = ⊥

@[simp]

theorem algebraic_geometry.Scheme.basic_open_mul (X : algebraic_geometry.Scheme) {U : topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)} (f g : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op U))) :

X.basic_open (f * g) = X.basic_open f ⊓ X.basic_open g

theorem algebraic_geometry.Scheme.basic_open_of_is_unit (X : algebraic_geometry.Scheme) {U : topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)} {f : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op U))} (hf : is_unit f) :

X.basic_open f = U

theorem algebraic_geometry.basic_open_eq_of_affine {R : CommRing} (f : ↥R) :

(algebraic_geometry.Scheme.Spec.obj (opposite.op R)).basic_open (⇑((algebraic_geometry.Spec_Γ_identity.app R).inv) f) = prime_spectrum.basic_open f

@[simp]