$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:
Spec.toTop, valued in the category of topological spaces,
Spec.toSheafedSpace, valued in the category of sheafed spaces and
Spec.toLocallyRingedSpace, valued in the category of locally ringed spaces.
Related results #
Γ ⊣ Spec is constructed in
The induced map of a ring homomorphism on the prime spectra, as a morphism of locally ringed spaces.
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