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

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

Instances For

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

Instances For
theorem AlgebraicGeometry.Spec.topMap_comp {R : CommRingCat} {S : CommRingCat} {T : CommRingCat} (f : R S) (g : S T) :
@[simp]
theorem AlgebraicGeometry.Spec.toTop_map {R : } {S : } (f : R S) :

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

Instances For
@[simp]
theorem AlgebraicGeometry.Spec.sheafedSpaceObj_carrier (R : CommRingCat) :
().toPresheafedSpace =
@[simp]
theorem AlgebraicGeometry.Spec.sheafedSpaceObj_presheaf (R : CommRingCat) :
().toPresheafedSpace.presheaf =

The spectrum of a commutative ring, as a SheafedSpace.

Instances For
@[simp]
theorem AlgebraicGeometry.Spec.sheafedSpaceMap_c_app {R : CommRingCat} {S : CommRingCat} (f : R S) (U : (TopologicalSpace.Opens ().toPresheafedSpace)ᵒᵖ) :
.app U = AlgebraicGeometry.StructureSheaf.comap f U.unop (().obj U.unop) (_ : ∀ (x : ), x (().obj U.unop).carrierx (().obj U.unop).carrier)

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

Instances For
@[simp]
@[simp]
theorem AlgebraicGeometry.Spec.toSheafedSpace_map :
∀ {X Y : } (f : X Y),

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

Instances For

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

Instances For
@[simp]
theorem AlgebraicGeometry.Spec.toPresheafedSpace_obj (R : ) :
= ().toPresheafedSpace
@[simp]
theorem AlgebraicGeometry.Spec.toPresheafedSpace_map (R : ) (S : ) (f : R S) :
theorem AlgebraicGeometry.Spec.basicOpen_hom_ext {R : CommRingCat} {α : } {β : } (w : α.base = β.base) (h : ∀ (r : R), let U := ; CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp () (α.c.app ())) (X.presheaf.map (CategoryTheory.eqToHom (_ : ().op.obj () = ().op.obj ()))) = CategoryTheory.CategoryStruct.comp () (β.c.app ())) :
α = β
@[simp]

The spectrum of a commutative ring, as a LocallyRingedSpace.

Instances For
theorem AlgebraicGeometry.stalkMap_toStalk_apply {R : CommRingCat} {S : CommRingCat} (f : R S) (p : ) (x : ().obj ()) :
↑() (↑() x) =
theorem AlgebraicGeometry.localRingHom_comp_stalkIso_apply {R : CommRingCat} {S : CommRingCat} (f : R S) (p : ) (x : ().obj ()) :
↑() (↑(Localization.localRingHom (↑() p).asIdeal p.asIdeal f (_ : (↑() p).asIdeal = (↑() p).asIdeal)) (↑() x)) =
theorem AlgebraicGeometry.localRingHom_comp_stalkIso {R : CommRingCat} {S : CommRingCat} (f : R S) (p : ) :
CategoryTheory.CategoryStruct.comp ().hom (CategoryTheory.CategoryStruct.comp (Localization.localRingHom (↑() p).asIdeal p.asIdeal f (_ : (↑() p).asIdeal = (↑() p).asIdeal)) ().inv) =

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

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

Instances For
@[simp]
@[simp]
theorem AlgebraicGeometry.Spec.toLocallyRingedSpace_map :
∀ {X Y : } (f : X Y),

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

Instances For
@[simp]
theorem AlgebraicGeometry.toSpecΓ_apply_coe (R : CommRingCat) (f : ↑()) (x : { x // x ().unop }) :
↑() x = ↑() f

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

Instances For
@[simp]

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

Instances For

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

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.

Instances For
@[simp]
theorem AlgebraicGeometry.StructureSheaf.toPushforwardStalkAlgHom_apply (R : CommRingCat) (S : CommRingCat) (p : ) [Algebra R S] :
∀ (a : S), = ↑(TopCat.Presheaf.germ () { val := p, property := trivial }) ()

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

Instances For