mathlib documentation

algebraic_geometry.Spec

$Spec$ as a functor to locally ringed spaces. #

We define the functor $Spec$ from commutative rings to locally ringed spaces.

Implementation notes #

We define $Spec$ in three consecutive steps, each with more structure than the last:

  1. Spec.to_Top, valued in the category of topological spaces,
  2. Spec.to_SheafedSpace, valued in the category of sheafed spaces and
  3. Spec.to_LocallyRingedSpace, valued in the category of locally ringed spaces.

Additionally, we provide Spec.to_PresheafedSpace as a composition of Spec.to_SheafedSpace with a forgetful functor.

The adjunction Γ ⊣ Spec is constructed in algebraic_geometry/Gamma_Spec_adjunction.lean.

source
def algebraic_geometry.Spec.Top_obj (R : CommRing) :
Top

The spectrum of a commutative ring, as a topological space.

Equations
source
def algebraic_geometry.Spec.Top_map {R S : CommRing} (f : R ⟶ S) :
algebraic_geometry.Spec.Top_obj S ⟶ algebraic_geometry.Spec.Top_obj R

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

Equations
source
@[simp]
theorem algebraic_geometry.Spec.Top_map_id (R : CommRing) :
algebraic_geometry.Spec.Top_map (𝟙 R) = 𝟙 (algebraic_geometry.Spec.Top_obj R)
source
theorem algebraic_geometry.Spec.Top_map_comp {R S T : CommRing} (f : R ⟶ S) (g : S ⟶ T) :
algebraic_geometry.Spec.Top_map (f ≫ g) = algebraic_geometry.Spec.Top_map g ≫ algebraic_geometry.Spec.Top_map f
source
@[simp]
theorem algebraic_geometry.Spec.to_Top_obj (R : CommRingᵒᵖ) :
algebraic_geometry.Spec.to_Top.obj R = algebraic_geometry.Spec.Top_obj (opposite.unop R)
source
def algebraic_geometry.Spec.to_Top  :
CommRingᵒᵖ ⥤ Top

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

Equations
source
@[simp]
theorem algebraic_geometry.Spec.to_Top_map (R S : CommRingᵒᵖ) (f : R ⟶ S) :
algebraic_geometry.Spec.to_Top.map f = algebraic_geometry.Spec.Top_map f.unop
source
@[simp]
theorem algebraic_geometry.Spec.SheafedSpace_obj_to_PresheafedSpace_presheaf (R : CommRing) :
(algebraic_geometry.Spec.SheafedSpace_obj R).to_PresheafedSpace.presheaf = (algebraic_geometry.structure_sheaf ↥R).val
source
def algebraic_geometry.Spec.SheafedSpace_obj (R : CommRing) :
algebraic_geometry.SheafedSpace CommRing

The spectrum of a commutative ring, as a SheafedSpace.

Equations
source
@[simp]
theorem algebraic_geometry.Spec.SheafedSpace_obj_to_PresheafedSpace_carrier (R : CommRing) :
(algebraic_geometry.Spec.SheafedSpace_obj R).to_PresheafedSpace.carrier = algebraic_geometry.Spec.Top_obj R
source
noncomputable def algebraic_geometry.Spec.SheafedSpace_map {R S : CommRing} (f : R ⟶ S) :
algebraic_geometry.Spec.SheafedSpace_obj S ⟶ algebraic_geometry.Spec.SheafedSpace_obj R

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

Equations
source
@[simp]
theorem algebraic_geometry.Spec.SheafedSpace_map_c_app {R S : CommRing} (f : R ⟶ S) (U : (topological_space.opens ↥((algebraic_geometry.Spec.SheafedSpace_obj R).to_PresheafedSpace.carrier))ᵒᵖ) :
(algebraic_geometry.Spec.SheafedSpace_map f).c.app U = algebraic_geometry.structure_sheaf.comap f (opposite.unop U) ((topological_space.opens.map (algebraic_geometry.Spec.Top_map f)).obj (opposite.unop U)) _
source
@[simp]
theorem algebraic_geometry.Spec.SheafedSpace_map_base {R S : CommRing} (f : R ⟶ S) :
(algebraic_geometry.Spec.SheafedSpace_map f).base = algebraic_geometry.Spec.Top_map f
source
@[simp]
theorem algebraic_geometry.Spec.SheafedSpace_map_id {R : CommRing} :
algebraic_geometry.Spec.SheafedSpace_map (𝟙 R) = 𝟙 (algebraic_geometry.Spec.SheafedSpace_obj R)
source
theorem algebraic_geometry.Spec.SheafedSpace_map_comp {R S T : CommRing} (f : R ⟶ S) (g : S ⟶ T) :
algebraic_geometry.Spec.SheafedSpace_map (f ≫ g) = algebraic_geometry.Spec.SheafedSpace_map g ≫ algebraic_geometry.Spec.SheafedSpace_map f
source
@[simp]
theorem algebraic_geometry.Spec.to_SheafedSpace_obj (R : CommRingᵒᵖ) :
algebraic_geometry.Spec.to_SheafedSpace.obj R = algebraic_geometry.Spec.SheafedSpace_obj (opposite.unop R)
source
@[simp]
theorem algebraic_geometry.Spec.to_SheafedSpace_map (R S : CommRingᵒᵖ) (f : R ⟶ S) :
algebraic_geometry.Spec.to_SheafedSpace.map f = algebraic_geometry.Spec.SheafedSpace_map f.unop
source
noncomputable def algebraic_geometry.Spec.to_SheafedSpace  :
CommRingᵒᵖ ⥤ algebraic_geometry.SheafedSpace CommRing

Spec, as a contravariant functor from commutative rings to sheafed spaces.

Equations
source
noncomputable def algebraic_geometry.Spec.to_PresheafedSpace  :
CommRingᵒᵖ ⥤ algebraic_geometry.PresheafedSpace CommRing

Spec, as a contravariant functor from commutative rings to presheafed spaces.

Equations
source
@[simp]
theorem algebraic_geometry.Spec.to_PresheafedSpace_obj (R : CommRingᵒᵖ) :
algebraic_geometry.Spec.to_PresheafedSpace.obj R = (algebraic_geometry.Spec.SheafedSpace_obj (opposite.unop R)).to_PresheafedSpace
source
theorem algebraic_geometry.Spec.to_PresheafedSpace_obj_op (R : CommRing) :
algebraic_geometry.Spec.to_PresheafedSpace.obj (opposite.op R) = (algebraic_geometry.Spec.SheafedSpace_obj R).to_PresheafedSpace
source
@[simp]
theorem algebraic_geometry.Spec.to_PresheafedSpace_map (R S : CommRingᵒᵖ) (f : R ⟶ S) :
algebraic_geometry.Spec.to_PresheafedSpace.map f = algebraic_geometry.Spec.SheafedSpace_map f.unop
source
theorem algebraic_geometry.Spec.to_PresheafedSpace_map_op (R S : CommRing) (f : R ⟶ S) :
algebraic_geometry.Spec.to_PresheafedSpace.map f.op = algebraic_geometry.Spec.SheafedSpace_map f
source
theorem algebraic_geometry.Spec.basic_open_hom_ext {X : algebraic_geometry.RingedSpace} {R : CommRing} {α β : X ⟶ algebraic_geometry.Spec.SheafedSpace_obj R} (w : α.base = β.base) (h : ∀ (r : ↥R), let U : topological_space.opens (prime_spectrum ↥R) := prime_spectrum.basic_open r in (algebraic_geometry.structure_sheaf.to_open ↥R U ≫ α.c.app (opposite.op U)) ≫ X.to_PresheafedSpace.presheaf.map (category_theory.eq_to_hom _) = algebraic_geometry.structure_sheaf.to_open ↥R U ≫ β.c.app (opposite.op U)) :
α = β
source
def algebraic_geometry.Spec.LocallyRingedSpace_obj (R : CommRing) :
algebraic_geometry.LocallyRingedSpace

The spectrum of a commutative ring, as a LocallyRingedSpace.

Equations
source
@[simp]
theorem algebraic_geometry.Spec.LocallyRingedSpace_obj_to_SheafedSpace (R : CommRing) :
(algebraic_geometry.Spec.LocallyRingedSpace_obj R).to_SheafedSpace = algebraic_geometry.Spec.SheafedSpace_obj R
source
theorem algebraic_geometry.stalk_map_to_stalk {R S : CommRing} (f : R ⟶ S) (p : prime_spectrum ↥S) :
algebraic_geometry.structure_sheaf.to_stalk ↥R (⇑(prime_spectrum.comap f) p) ≫ algebraic_geometry.PresheafedSpace.stalk_map (algebraic_geometry.Spec.SheafedSpace_map f) p = f ≫ algebraic_geometry.structure_sheaf.to_stalk ↥S p
source
theorem algebraic_geometry.stalk_map_to_stalk_apply {R S : CommRing} (f : R ⟶ S) (p : prime_spectrum ↥S) (x : ↥(CommRing.of ↥R)) :
⇑(algebraic_geometry.PresheafedSpace.stalk_map (algebraic_geometry.Spec.SheafedSpace_map f) p) (⇑(algebraic_geometry.structure_sheaf.to_stalk ↥R (⇑(prime_spectrum.comap f) p)) x) = ⇑(algebraic_geometry.structure_sheaf.to_stalk ↥S p) (⇑f x)
source
theorem algebraic_geometry.local_ring_hom_comp_stalk_iso {R S : CommRing} (f : R ⟶ S) (p : prime_spectrum ↥S) :
(algebraic_geometry.structure_sheaf.stalk_iso ↥R (⇑(prime_spectrum.comap f) p)).hom ≫ localization.local_ring_hom (⇑(prime_spectrum.comap f) p).as_ideal p.as_ideal f rfl ≫ (algebraic_geometry.structure_sheaf.stalk_iso ↥S p).inv = algebraic_geometry.PresheafedSpace.stalk_map (algebraic_geometry.Spec.SheafedSpace_map f) p

Under the isomorphisms stalk_iso, the map stalk_map (Spec.SheafedSpace_map f) p corresponds to the induced local ring homomorphism localization.local_ring_hom.

source
theorem algebraic_geometry.local_ring_hom_comp_stalk_iso_apply {R S : CommRing} (f : R ⟶ S) (p : prime_spectrum ↥S) (x : ↥((algebraic_geometry.structure_sheaf ↥R).val.stalk (⇑(prime_spectrum.comap f) p))) :
⇑((algebraic_geometry.structure_sheaf.stalk_iso ↥S p).inv) (⇑(localization.local_ring_hom (⇑(prime_spectrum.comap f) p).as_ideal p.as_ideal f rfl) (⇑((algebraic_geometry.structure_sheaf.stalk_iso ↥R (⇑(prime_spectrum.comap f) p)).hom) x)) = ⇑(algebraic_geometry.PresheafedSpace.stalk_map (algebraic_geometry.Spec.SheafedSpace_map f) p) x
source
@[simp]
theorem algebraic_geometry.Spec.LocallyRingedSpace_map_coe {R S : CommRing} (f : R ⟶ S) :
↑(algebraic_geometry.Spec.LocallyRingedSpace_map f) = algebraic_geometry.Spec.SheafedSpace_map f
source
noncomputable def algebraic_geometry.Spec.LocallyRingedSpace_map {R S : CommRing} (f : R ⟶ S) :
algebraic_geometry.Spec.LocallyRingedSpace_obj S ⟶ algebraic_geometry.Spec.LocallyRingedSpace_obj R

The induced map of a ring homomorphism on the prime spectra, as a morphism of locally ringed spaces.

Equations
source
@[simp]
theorem algebraic_geometry.Spec.LocallyRingedSpace_map_id (R : CommRing) :
algebraic_geometry.Spec.LocallyRingedSpace_map (𝟙 R) = 𝟙 (algebraic_geometry.Spec.LocallyRingedSpace_obj R)
source
theorem algebraic_geometry.Spec.LocallyRingedSpace_map_comp {R S T : CommRing} (f : R ⟶ S) (g : S ⟶ T) :
algebraic_geometry.Spec.LocallyRingedSpace_map (f ≫ g) = algebraic_geometry.Spec.LocallyRingedSpace_map g ≫ algebraic_geometry.Spec.LocallyRingedSpace_map f
source
@[simp]
theorem algebraic_geometry.Spec.to_LocallyRingedSpace_obj (R : CommRingᵒᵖ) :
algebraic_geometry.Spec.to_LocallyRingedSpace.obj R = algebraic_geometry.Spec.LocallyRingedSpace_obj (opposite.unop R)
source
noncomputable def algebraic_geometry.Spec.to_LocallyRingedSpace  :
CommRingᵒᵖ ⥤ algebraic_geometry.LocallyRingedSpace

Spec, as a contravariant functor from commutative rings to locally ringed spaces.

Equations
source
@[simp]
theorem algebraic_geometry.Spec.to_LocallyRingedSpace_map (R S : CommRingᵒᵖ) (f : R ⟶ S) :
algebraic_geometry.Spec.to_LocallyRingedSpace.map f = algebraic_geometry.Spec.LocallyRingedSpace_map f.unop
source
@[simp]
theorem algebraic_geometry.to_Spec_Γ_apply_coe (R : CommRing) (f : ↥(CommRing.of ↥R)) (x : ↥(opposite.unop (opposite.op ⊤))) :
↑(⇑(algebraic_geometry.to_Spec_Γ R) f) x = ⇑(algebra_map ↥R (algebraic_geometry.structure_sheaf.localizations ↥R ↑x)) f
source
def algebraic_geometry.to_Spec_Γ (R : CommRing) :
R ⟶ algebraic_geometry.LocallyRingedSpace.Γ.obj (opposite.op (algebraic_geometry.Spec.to_LocallyRingedSpace.obj (opposite.op R)))

The counit morphism R ⟶ Γ(Spec R) given by algebraic_geometry.structure_sheaf.to_open.

Equations
source
@[protected, instance]
def algebraic_geometry.is_iso_to_Spec_Γ (R : CommRing) :
category_theory.is_iso (algebraic_geometry.to_Spec_Γ R)
source
theorem algebraic_geometry.Spec_Γ_naturality_assoc {R S : CommRing} (f : R ⟶ S) {X' : CommRing} (f' : algebraic_geometry.LocallyRingedSpace.Γ.obj (opposite.op (algebraic_geometry.Spec.to_LocallyRingedSpace.obj (opposite.op S))) ⟶ X') :
f ≫ algebraic_geometry.to_Spec_Γ S ≫ f' = algebraic_geometry.to_Spec_Γ R ≫ algebraic_geometry.LocallyRingedSpace.Γ.map (algebraic_geometry.Spec.to_LocallyRingedSpace.map f.op).op ≫ f'
source
theorem algebraic_geometry.Spec_Γ_naturality {R S : CommRing} (f : R ⟶ S) :
f ≫ algebraic_geometry.to_Spec_Γ S = algebraic_geometry.to_Spec_Γ R ≫ algebraic_geometry.LocallyRingedSpace.Γ.map (algebraic_geometry.Spec.to_LocallyRingedSpace.map f.op).op
source
@[simp]
theorem algebraic_geometry.Spec_Γ_identity_hom_app (X : CommRing) :
algebraic_geometry.Spec_Γ_identity.hom.app X = category_theory.inv (algebraic_geometry.to_Spec_Γ X)
source
@[simp]
theorem algebraic_geometry.Spec_Γ_identity_inv_app (X : CommRing) :
algebraic_geometry.Spec_Γ_identity.inv.app X = algebraic_geometry.to_Spec_Γ X
source
noncomputable def algebraic_geometry.Spec_Γ_identity  :
algebraic_geometry.Spec.to_LocallyRingedSpace.right_op ⋙ algebraic_geometry.LocallyRingedSpace.Γ ≅ 𝟭 CommRing

The counit (Spec_Γ_identity.inv.op) of the adjunction Γ ⊣ Spec is an isomorphism.

Equations
source
theorem algebraic_geometry.Spec_map_localization_is_iso (R : CommRing) (M : submonoid ↥R) (x : prime_spectrum (localization M)) :
category_theory.is_iso (algebraic_geometry.PresheafedSpace.stalk_map (algebraic_geometry.Spec.to_PresheafedSpace.map (CommRing.of_hom (algebra_map ↥R (localization M))).op) x)

The stalk map of Spec M⁻¹R ⟶ Spec R is an iso for each p : Spec M⁻¹R.