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

Related results

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

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

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

@[simp]

theorem AlgebraicGeometry.Spec.topObj_forget {R : CommRingCat} : CategoryTheory.ToType (topObj R) = PrimeSpectrum ↑R

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.

@[simp]

theorem AlgebraicGeometry.Spec.topMap_id (R : CommRingCat) : topMap (CategoryTheory.CategoryStruct.id R) = CategoryTheory.CategoryStruct.id (topObj R)

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

def AlgebraicGeometry.Spec.toTop : CategoryTheory.Functor CommRingCatᵒᵖ TopCat

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

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

@[simp]

theorem AlgebraicGeometry.Spec.toTop_obj_carrier (R : CommRingCatᵒᵖ) : ↑(toTop.obj R) = PrimeSpectrum ↑(Opposite.unop R)

def AlgebraicGeometry.Spec.sheafedSpaceObj (R : CommRingCat) : SheafedSpace CommRingCat

The spectrum of a commutative ring, as a SheafedSpace.

@[simp]

theorem AlgebraicGeometry.Spec.sheafedSpaceObj_carrier (R : CommRingCat) : ↑(sheafedSpaceObj R).toPresheafedSpace = topObj R

@[simp]

theorem AlgebraicGeometry.Spec.sheafedSpaceObj_presheaf (R : CommRingCat) : (sheafedSpaceObj R).presheaf = (structureSheaf ↑R).val

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.

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

@[simp]

theorem AlgebraicGeometry.Spec.sheafedSpaceMap_base {R S : CommRingCat} (f : R ⟶ S) : (sheafedSpaceMap f).base = topMap f

@[simp]

theorem AlgebraicGeometry.Spec.sheafedSpaceMap_id {R : CommRingCat} : sheafedSpaceMap (CategoryTheory.CategoryStruct.id R) = CategoryTheory.CategoryStruct.id (sheafedSpaceObj R)

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)

def AlgebraicGeometry.Spec.toSheafedSpace : CategoryTheory.Functor CommRingCatᵒᵖ (SheafedSpace CommRingCat)

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

@[simp]

theorem AlgebraicGeometry.Spec.toSheafedSpace_obj (R : CommRingCatᵒᵖ) : toSheafedSpace.obj R = sheafedSpaceObj (Opposite.unop R)

@[simp]

theorem AlgebraicGeometry.Spec.toSheafedSpace_map {X✝ Y✝ : CommRingCatᵒᵖ} (f : X✝ ⟶ Y✝) : toSheafedSpace.map f = sheafedSpaceMap f.unop

def AlgebraicGeometry.Spec.toPresheafedSpace : CategoryTheory.Functor CommRingCatᵒᵖ (PresheafedSpace CommRingCat)

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

@[simp]

theorem AlgebraicGeometry.Spec.toPresheafedSpace_obj (R : CommRingCatᵒᵖ) : toPresheafedSpace.obj R = (sheafedSpaceObj (Opposite.unop R)).toPresheafedSpace

theorem AlgebraicGeometry.Spec.toPresheafedSpace_obj_op (R : CommRingCat) : toPresheafedSpace.obj (Opposite.op R) = (sheafedSpaceObj R).toPresheafedSpace

@[simp]

theorem AlgebraicGeometry.Spec.toPresheafedSpace_map (R S : CommRingCatᵒᵖ) (f : R ⟶ S) : toPresheafedSpace.map f = sheafedSpaceMap f.unop

theorem AlgebraicGeometry.Spec.toPresheafedSpace_map_op (R S : CommRingCat) (f : R ⟶ S) : toPresheafedSpace.map f.op = sheafedSpaceMap f

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))) : α = β

def AlgebraicGeometry.Spec.locallyRingedSpaceObj (R : CommRingCat) : LocallyRingedSpace

The spectrum of a commutative ring, as a LocallyRingedSpace.

@[simp]

theorem AlgebraicGeometry.Spec.locallyRingedSpaceObj_presheaf (R : CommRingCat) : (locallyRingedSpaceObj R).presheaf = (structureSheaf ↑R).val

@[simp]

theorem AlgebraicGeometry.Spec.locallyRingedSpaceObj_toSheafedSpace (R : CommRingCat) : (locallyRingedSpaceObj R).toSheafedSpace = sheafedSpaceObj R

theorem AlgebraicGeometry.Spec.locallyRingedSpaceObj_sheaf (R : CommRingCat) : (locallyRingedSpaceObj R).sheaf = structureSheaf ↑R

theorem AlgebraicGeometry.Spec.locallyRingedSpaceObj_sheaf' (R : Type u) [CommRing R] : (locallyRingedSpaceObj (CommRingCat.of R)).sheaf = structureSheaf R

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

theorem AlgebraicGeometry.Spec.locallyRingedSpaceObj_presheaf' (R : Type u) [CommRing R] : (locallyRingedSpaceObj (CommRingCat.of R)).presheaf = (structureSheaf R).val

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

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)

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

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.

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

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

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.

@[simp]

theorem AlgebraicGeometry.Spec.locallyRingedSpaceMap_toShHom {R S : CommRingCat} (f : R ⟶ S) : LocallyRingedSpace.Hom.toShHom (locallyRingedSpaceMap f) = sheafedSpaceMap f

@[simp]

theorem AlgebraicGeometry.Spec.locallyRingedSpaceMap_id (R : CommRingCat) : locallyRingedSpaceMap (CategoryTheory.CategoryStruct.id R) = CategoryTheory.CategoryStruct.id (locallyRingedSpaceObj R)

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)

def AlgebraicGeometry.Spec.toLocallyRingedSpace : CategoryTheory.Functor CommRingCatᵒᵖ LocallyRingedSpace

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

@[simp]

theorem AlgebraicGeometry.Spec.toLocallyRingedSpace_map {X✝ Y✝ : CommRingCatᵒᵖ} (f : X✝ ⟶ Y✝) : toLocallyRingedSpace.map f = locallyRingedSpaceMap f.unop

@[simp]

theorem AlgebraicGeometry.Spec.toLocallyRingedSpace_obj (R : CommRingCatᵒᵖ) : toLocallyRingedSpace.obj R = locallyRingedSpaceObj (Opposite.unop R)

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.

instance AlgebraicGeometry.isIso_toSpecΓ (R : CommRingCat) : CategoryTheory.IsIso (toSpecΓ R)

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)

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)

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.

@[simp]

theorem AlgebraicGeometry.LocallyRingedSpace.SpecΓIdentity_inv_app (X : CommRingCat) : SpecΓIdentity.inv.app X = toSpecΓ X

@[simp]

theorem AlgebraicGeometry.LocallyRingedSpace.SpecΓIdentity_hom_app (X : CommRingCat) : SpecΓIdentity.hom.app X = CategoryTheory.inv (toSpecΓ X)

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.

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.

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)

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)

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)

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

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.

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

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

instance AlgebraicGeometry.StructureSheaf.isLocalizedModule_toPushforwardStalkAlgHom (R S : CommRingCat) (p : PrimeSpectrum ↑R) [Algebra ↑R ↑S] : IsLocalizedModule p.asIdeal.primeCompl (toPushforwardStalkAlgHom R S p).toLinearMap