Documentation

Mathlib.AlgebraicGeometry.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.toTop, valued in the category of topological spaces,
  2. Spec.toSheafedSpace, valued in the category of sheafed spaces and
  3. Spec.toLocallyRingedSpace, valued in the category of locally ringed spaces.

Additionally, we provide Spec.toPresheafedSpace as a composition of Spec.toSheafedSpace with a forgetful functor.

The adjunction Γ ⊣ Spec is constructed in Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean.

source
def AlgebraicGeometry.Spec.topObj (R : CommRingCat) :
TopCat

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

Equations
source
@[simp]
theorem AlgebraicGeometry.Spec.topObj_forget {R : CommRingCat} :
CategoryTheory.ToType (topObj R) = PrimeSpectrum ↑R
source
def AlgebraicGeometry.Spec.topMap {R S : CommRingCat} (f : R ⟶ S) :
topObj S ⟶ topObj R

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

Equations
source
@[simp]
theorem AlgebraicGeometry.Spec.topMap_id (R : CommRingCat) :
topMap (CategoryTheory.CategoryStruct.id R) = CategoryTheory.CategoryStruct.id (topObj R)
source
@[simp]
theorem AlgebraicGeometry.Spec.topMap_comp {R S T : CommRingCat} (f : R ⟶ S) (g : S ⟶ T) :
topMap (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (topMap g) (topMap f)
source
def AlgebraicGeometry.Spec.toTop :
CategoryTheory.Functor CommRingCatᵒᵖ TopCat

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

Equations
  • One or more equations did not get rendered due to their size.
source
@[simp]
theorem AlgebraicGeometry.Spec.toTop_obj_carrier (R : CommRingCatᵒᵖ) :
↑(toTop.obj R) = PrimeSpectrum ↑(Opposite.unop R)
source
@[simp]
theorem AlgebraicGeometry.Spec.coe_toTop_map_hom_apply_asIdeal {x✝ x✝¹ : CommRingCatᵒᵖ} (f : x✝ ⟶ x✝¹) (a✝ : PrimeSpectrum ↑(Opposite.unop x✝)) :
↑((TopCat.Hom.hom (toTop.map f)) a✝).asIdeal = ⇑(CommRingCat.Hom.hom f.unop) ⁻¹' ↑a✝.asIdeal
source
def AlgebraicGeometry.Spec.sheafedSpaceObj (R : CommRingCat) :
SheafedSpace CommRingCat

The spectrum of a commutative ring, as a SheafedSpace.

Equations
source
@[simp]
theorem AlgebraicGeometry.Spec.sheafedSpaceObj_carrier (R : CommRingCat) :
↑(sheafedSpaceObj R).toPresheafedSpace = topObj R
source
@[simp]
theorem AlgebraicGeometry.Spec.sheafedSpaceObj_presheaf (R : CommRingCat) :
(sheafedSpaceObj R).presheaf = (structureSheaf ↑R).val
source
def AlgebraicGeometry.Spec.sheafedSpaceMap {R S : CommRingCat} (f : R ⟶ S) :
sheafedSpaceObj S ⟶ sheafedSpaceObj R

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

Equations
  • One or more equations did not get rendered due to their size.
source
@[simp]
theorem AlgebraicGeometry.Spec.sheafedSpaceMap_c_app {R S : CommRingCat} (f : R ⟶ S) (U : (TopologicalSpace.Opens ↑↑(sheafedSpaceObj R).toPresheafedSpace)ᵒᵖ) :
(sheafedSpaceMap f).c.app U = CommRingCat.ofHom (StructureSheaf.comap (CommRingCat.Hom.hom f) (Opposite.unop U) ((TopologicalSpace.Opens.map (topMap f)).obj (Opposite.unop U)) ⋯)
source
@[simp]
theorem AlgebraicGeometry.Spec.sheafedSpaceMap_base {R S : CommRingCat} (f : R ⟶ S) :
(sheafedSpaceMap f).base = topMap f
source
@[simp]
theorem AlgebraicGeometry.Spec.sheafedSpaceMap_id {R : CommRingCat} :
sheafedSpaceMap (CategoryTheory.CategoryStruct.id R) = CategoryTheory.CategoryStruct.id (sheafedSpaceObj R)
source
theorem AlgebraicGeometry.Spec.sheafedSpaceMap_comp {R S T : CommRingCat} (f : R ⟶ S) (g : S ⟶ T) :
sheafedSpaceMap (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (sheafedSpaceMap g) (sheafedSpaceMap f)
source
def AlgebraicGeometry.Spec.toSheafedSpace :
CategoryTheory.Functor CommRingCatᵒᵖ (SheafedSpace CommRingCat)

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

Equations
  • One or more equations did not get rendered due to their size.
source
@[simp]
theorem AlgebraicGeometry.Spec.toSheafedSpace_obj (R : CommRingCatᵒᵖ) :
toSheafedSpace.obj R = sheafedSpaceObj (Opposite.unop R)
source
@[simp]
theorem AlgebraicGeometry.Spec.toSheafedSpace_map {X✝ Y✝ : CommRingCatᵒᵖ} (f : X✝ ⟶ Y✝) :
toSheafedSpace.map f = sheafedSpaceMap f.unop
source
def AlgebraicGeometry.Spec.toPresheafedSpace :
CategoryTheory.Functor CommRingCatᵒᵖ (PresheafedSpace CommRingCat)

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

Equations
source
@[simp]
theorem AlgebraicGeometry.Spec.toPresheafedSpace_obj (R : CommRingCatᵒᵖ) :
toPresheafedSpace.obj R = (sheafedSpaceObj (Opposite.unop R)).toPresheafedSpace
source
theorem AlgebraicGeometry.Spec.toPresheafedSpace_obj_op (R : CommRingCat) :
toPresheafedSpace.obj (Opposite.op R) = (sheafedSpaceObj R).toPresheafedSpace
source
@[simp]
theorem AlgebraicGeometry.Spec.toPresheafedSpace_map (R S : CommRingCatᵒᵖ) (f : R ⟶ S) :
toPresheafedSpace.map f = sheafedSpaceMap f.unop
source
theorem AlgebraicGeometry.Spec.toPresheafedSpace_map_op (R S : CommRingCat) (f : R ⟶ S) :
toPresheafedSpace.map f.op = sheafedSpaceMap f
source
theorem AlgebraicGeometry.Spec.basicOpen_hom_ext {X : RingedSpace} {R : CommRingCat} {α β : X ⟶ sheafedSpaceObj R} (w : α.base = β.base) (h : ∀ (r : ↑R), let U := PrimeSpectrum.basicOpen r; CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (StructureSheaf.toOpen (↑R) U) (α.c.app (Opposite.op U))) (X.presheaf.map (CategoryTheory.eqToHom ⋯)) = CategoryTheory.CategoryStruct.comp (StructureSheaf.toOpen (↑R) U) (β.c.app (Opposite.op U))) :
α = β
source
def AlgebraicGeometry.Spec.locallyRingedSpaceObj (R : CommRingCat) :
LocallyRingedSpace

The spectrum of a commutative ring, as a LocallyRingedSpace.

Equations
source
@[simp]
theorem AlgebraicGeometry.Spec.locallyRingedSpaceObj_toSheafedSpace (R : CommRingCat) :
(locallyRingedSpaceObj R).toSheafedSpace = sheafedSpaceObj R
source
@[simp]
theorem AlgebraicGeometry.Spec.locallyRingedSpaceObj_presheaf (R : CommRingCat) :
(locallyRingedSpaceObj R).presheaf = (structureSheaf ↑R).val
source
theorem AlgebraicGeometry.Spec.locallyRingedSpaceObj_sheaf (R : CommRingCat) :
(locallyRingedSpaceObj R).sheaf = structureSheaf ↑R
source
theorem AlgebraicGeometry.Spec.locallyRingedSpaceObj_sheaf' (R : Type u) [CommRing R] :
(locallyRingedSpaceObj (CommRingCat.of R)).sheaf = structureSheaf R
source
theorem AlgebraicGeometry.Spec.locallyRingedSpaceObj_presheaf_map (R : CommRingCat) {U V : (TopologicalSpace.Opens ↑↑(locallyRingedSpaceObj R).toPresheafedSpace)ᵒᵖ} (i : U ⟶ V) :
(locallyRingedSpaceObj R).presheaf.map i = (structureSheaf ↑R).val.map i
source
theorem AlgebraicGeometry.Spec.locallyRingedSpaceObj_presheaf' (R : Type u) [CommRing R] :
(locallyRingedSpaceObj (CommRingCat.of R)).presheaf = (structureSheaf R).val
source
theorem AlgebraicGeometry.Spec.locallyRingedSpaceObj_presheaf_map' (R : Type u) [CommRing R] {U V : (TopologicalSpace.Opens ↑↑(locallyRingedSpaceObj (CommRingCat.of R)).toPresheafedSpace)ᵒᵖ} (i : U ⟶ V) :
(locallyRingedSpaceObj (CommRingCat.of R)).presheaf.map i = (structureSheaf R).val.map i
source
theorem AlgebraicGeometry.stalkMap_toStalk {R S : CommRingCat} (f : R ⟶ S) (p : PrimeSpectrum ↑S) :
CategoryTheory.CategoryStruct.comp (StructureSheaf.toStalk (↑R) ((PrimeSpectrum.comap (CommRingCat.Hom.hom f)) p)) (PresheafedSpace.Hom.stalkMap (Spec.sheafedSpaceMap f) p) = CategoryTheory.CategoryStruct.comp f (StructureSheaf.toStalk (↑S) p)
source
theorem AlgebraicGeometry.stalkMap_toStalk_apply {R S : CommRingCat} (f : R ⟶ S) (p : PrimeSpectrum ↑S) (x : CategoryTheory.ToType (CommRingCat.of ↑R)) :
(CategoryTheory.ConcreteCategory.hom (PresheafedSpace.Hom.stalkMap (Spec.sheafedSpaceMap f) p)) ((CategoryTheory.ConcreteCategory.hom (StructureSheaf.toStalk (↑R) ((PrimeSpectrum.comap (CommRingCat.Hom.hom f)) p))) x) = (CategoryTheory.CategoryStruct.comp f (StructureSheaf.toStalk (↑S) p)) x
source
theorem AlgebraicGeometry.localRingHom_comp_stalkIso {R S : CommRingCat} (f : R ⟶ S) (p : PrimeSpectrum ↑S) :
CategoryTheory.CategoryStruct.comp (StructureSheaf.stalkIso (↑R) ((PrimeSpectrum.comap (CommRingCat.Hom.hom f)) p)).hom (CategoryTheory.CategoryStruct.comp (CommRingCat.ofHom (Localization.localRingHom ((PrimeSpectrum.comap (CommRingCat.Hom.hom f)) p).asIdeal p.asIdeal (CommRingCat.Hom.hom f) ⋯)) (StructureSheaf.stalkIso (↑S) p).inv) = PresheafedSpace.Hom.stalkMap (Spec.sheafedSpaceMap f) p

Under the isomorphisms stalkIso, the map stalkMap (Spec.sheafedSpaceMap f) p corresponds to the induced local ring homomorphism Localization.localRingHom.

source
theorem AlgebraicGeometry.localRingHom_comp_stalkIso_apply {R S : CommRingCat} (f : R ⟶ S) (p : PrimeSpectrum ↑S) (x : CategoryTheory.ToType ((Spec.structureSheaf ↑R).presheaf.stalk ((PrimeSpectrum.comap (CommRingCat.Hom.hom f)) p))) :
(CategoryTheory.ConcreteCategory.hom (StructureSheaf.localizationToStalk (↑S) p)) ((Localization.localRingHom (Ideal.comap (CommRingCat.Hom.hom f) p.asIdeal) p.asIdeal (CommRingCat.Hom.hom f) ⋯) ((CategoryTheory.ConcreteCategory.hom (StructureSheaf.stalkToFiberRingHom (↑R) ((PrimeSpectrum.comap (CommRingCat.Hom.hom f)) p))) x)) = (PresheafedSpace.Hom.stalkMap (Spec.sheafedSpaceMap f) p) x
source
theorem AlgebraicGeometry.localRingHom_comp_stalkIso_apply' {R S : CommRingCat} (f : R ⟶ S) (p : PrimeSpectrum ↑S) (x : ↑((Spec.structureSheaf ↑R).presheaf.stalk ((PrimeSpectrum.comap (CommRingCat.Hom.hom f)) p))) :
(CategoryTheory.ConcreteCategory.hom (StructureSheaf.stalkIso (↑S) p).inv) ((Localization.localRingHom ((PrimeSpectrum.comap (CommRingCat.Hom.hom f)) p).asIdeal p.asIdeal (CommRingCat.Hom.hom f) ⋯) ((CategoryTheory.ConcreteCategory.hom (StructureSheaf.stalkIso (↑R) ((PrimeSpectrum.comap (CommRingCat.Hom.hom f)) p)).hom) x)) = (CategoryTheory.ConcreteCategory.hom (PresheafedSpace.Hom.stalkMap (Spec.sheafedSpaceMap f) p)) x

Version of localRingHom_comp_stalkIso_apply using CommRingCat.Hom.hom

source
def AlgebraicGeometry.Spec.locallyRingedSpaceMap {R S : CommRingCat} (f : R ⟶ S) :
locallyRingedSpaceObj S ⟶ locallyRingedSpaceObj R

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

Equations
source
@[simp]
theorem AlgebraicGeometry.Spec.locallyRingedSpaceMap_toShHom {R S : CommRingCat} (f : R ⟶ S) :
LocallyRingedSpace.Hom.toShHom (locallyRingedSpaceMap f) = sheafedSpaceMap f
source
@[simp]
theorem AlgebraicGeometry.Spec.locallyRingedSpaceMap_id (R : CommRingCat) :
locallyRingedSpaceMap (CategoryTheory.CategoryStruct.id R) = CategoryTheory.CategoryStruct.id (locallyRingedSpaceObj R)
source
theorem AlgebraicGeometry.Spec.locallyRingedSpaceMap_comp {R S T : CommRingCat} (f : R ⟶ S) (g : S ⟶ T) :
locallyRingedSpaceMap (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (locallyRingedSpaceMap g) (locallyRingedSpaceMap f)
source
def AlgebraicGeometry.Spec.toLocallyRingedSpace :
CategoryTheory.Functor CommRingCatᵒᵖ LocallyRingedSpace

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

Equations
  • One or more equations did not get rendered due to their size.
source
@[simp]
theorem AlgebraicGeometry.Spec.toLocallyRingedSpace_map {X✝ Y✝ : CommRingCatᵒᵖ} (f : X✝ ⟶ Y✝) :
toLocallyRingedSpace.map f = locallyRingedSpaceMap f.unop
source
@[simp]
theorem AlgebraicGeometry.Spec.toLocallyRingedSpace_obj (R : CommRingCatᵒᵖ) :
toLocallyRingedSpace.obj R = locallyRingedSpaceObj (Opposite.unop R)
source
def AlgebraicGeometry.toSpecΓ (R : CommRingCat) :
R ⟶ LocallyRingedSpace.Γ.obj (Opposite.op (Spec.toLocallyRingedSpace.obj (Opposite.op R)))

The counit morphism R ⟶ Γ(Spec R) given by AlgebraicGeometry.StructureSheaf.toOpen.

Equations
source
instance AlgebraicGeometry.isIso_toSpecΓ (R : CommRingCat) :
CategoryTheory.IsIso (toSpecΓ R)
source
theorem AlgebraicGeometry.Spec_Γ_naturality {R S : CommRingCat} (f : R ⟶ S) :
CategoryTheory.CategoryStruct.comp f (toSpecΓ S) = CategoryTheory.CategoryStruct.comp (toSpecΓ R) (LocallyRingedSpace.Γ.map (Spec.toLocallyRingedSpace.map f.op).op)
source
theorem AlgebraicGeometry.Spec_Γ_naturality_assoc {R S : CommRingCat} (f : R ⟶ S) {Z : CommRingCat} (h : LocallyRingedSpace.Γ.obj (Opposite.op (Spec.toLocallyRingedSpace.obj (Opposite.op S))) ⟶ Z) :
CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (toSpecΓ S) h) = CategoryTheory.CategoryStruct.comp (toSpecΓ R) (CategoryTheory.CategoryStruct.comp (LocallyRingedSpace.Γ.map (Spec.toLocallyRingedSpace.map f.op).op) h)
source
def AlgebraicGeometry.LocallyRingedSpace.SpecΓIdentity :
Spec.toLocallyRingedSpace.rightOp.comp Γ ≅ CategoryTheory.Functor.id CommRingCat

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

Equations
  • One or more equations did not get rendered due to their size.
source
@[simp]
theorem AlgebraicGeometry.LocallyRingedSpace.SpecΓIdentity_inv_app (X : CommRingCat) :
SpecΓIdentity.inv.app X = toSpecΓ X
source
@[simp]
theorem AlgebraicGeometry.LocallyRingedSpace.SpecΓIdentity_hom_app (X : CommRingCat) :
SpecΓIdentity.hom.app X = CategoryTheory.inv (toSpecΓ X)
source
theorem AlgebraicGeometry.Spec_map_localization_isIso (R : CommRingCat) (M : Submonoid ↑R) (x : PrimeSpectrum (Localization M)) :
CategoryTheory.IsIso (PresheafedSpace.Hom.stalkMap (Spec.toPresheafedSpace.map (CommRingCat.ofHom (algebraMap (↑R) (Localization M))).op) x)

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

source
def AlgebraicGeometry.StructureSheaf.toPushforwardStalk {R S : CommRingCat} (f : R ⟶ S) (p : PrimeSpectrum ↑R) :
S ⟶ ((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap f)).obj (Spec.structureSheaf ↑S).val).stalk p

For an algebra f : R →+* S, this is the ring homomorphism S →+* (f∗ 𝒪ₛ)ₚ for a p : Spec R. This is shown to be the localization at p in isLocalizedModule_toPushforwardStalkAlgHom.

Equations
  • One or more equations did not get rendered due to their size.
source
theorem AlgebraicGeometry.StructureSheaf.toPushforwardStalk_comp {R S : CommRingCat} (f : R ⟶ S) (p : PrimeSpectrum ↑R) :
CategoryTheory.CategoryStruct.comp f (toPushforwardStalk f p) = CategoryTheory.CategoryStruct.comp (toStalk (↑R) p) ((TopCat.Presheaf.stalkFunctor CommRingCat p).map (Spec.sheafedSpaceMap f).c)
source
theorem AlgebraicGeometry.StructureSheaf.toPushforwardStalk_comp_assoc {R S : CommRingCat} (f : R ⟶ S) (p : PrimeSpectrum ↑R) {Z : CommRingCat} (h : ((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap f)).obj (Spec.structureSheaf ↑S).val).stalk p ⟶ Z) :
CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (toPushforwardStalk f p) h) = CategoryTheory.CategoryStruct.comp (toStalk (↑R) p) (CategoryTheory.CategoryStruct.comp ((TopCat.Presheaf.stalkFunctor CommRingCat p).map (Spec.sheafedSpaceMap f).c) h)
source
instance AlgebraicGeometry.StructureSheaf.instAlgebraCarrierStalkCommRingCatObjPresheafTopObjPushforwardTopMapValOpensCarrierTopStructureSheaf {R S : CommRingCat} (f : R ⟶ S) (p : PrimeSpectrum ↑R) :
Algebra ↑R ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap f)).obj (Spec.structureSheaf ↑S).val).stalk p)
Equations
  • One or more equations did not get rendered due to their size.
source
theorem AlgebraicGeometry.StructureSheaf.algebraMap_pushforward_stalk {R S : CommRingCat} (f : R ⟶ S) (p : PrimeSpectrum ↑R) :
algebraMap ↑R ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap f)).obj (Spec.structureSheaf ↑S).val).stalk p) = CommRingCat.Hom.hom (CategoryTheory.CategoryStruct.comp f (toPushforwardStalk f p))
source
def AlgebraicGeometry.StructureSheaf.toPushforwardStalkAlgHom (R S : CommRingCat) (p : PrimeSpectrum ↑R) [Algebra ↑R ↑S] :
↑S →ₐ[↑R] ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj (Spec.structureSheaf ↑S).val).stalk p)

This is the AlgHom version of toPushforwardStalk, which is the map S ⟶ (f∗ 𝒪ₛ)ₚ for some algebra R ⟶ S and some p : Spec R.

Equations
  • One or more equations did not get rendered due to their size.
source
@[simp]
theorem AlgebraicGeometry.StructureSheaf.toPushforwardStalkAlgHom_apply (R S : CommRingCat) (p : PrimeSpectrum ↑R) [Algebra ↑R ↑S] (a✝ : ↑(CommRingCat.of ↑S)) :
(toPushforwardStalkAlgHom R S p) a✝ = (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj (Spec.structureSheaf ↑S).val).germ ⊤ p trivial).hom' ((toOpen ↑S ⊤).hom' a✝)
source
theorem AlgebraicGeometry.StructureSheaf.isLocalizedModule_toPushforwardStalkAlgHom_aux (R S : CommRingCat) (p : PrimeSpectrum ↑R) [Algebra ↑R ↑S] (y : ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj (Spec.structureSheaf ↑S).val).stalk p)) :
∃ (x : ↑S × ↥p.asIdeal.primeCompl), x.2 • y = (toPushforwardStalkAlgHom R S p) x.1
source
instance AlgebraicGeometry.StructureSheaf.isLocalizedModule_toPushforwardStalkAlgHom (R S : CommRingCat) (p : PrimeSpectrum ↑R) [Algebra ↑R ↑S] :
IsLocalizedModule p.asIdeal.primeCompl (toPushforwardStalkAlgHom R S p).toLinearMap