$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.to_Top, valued in the category of topological spaces,Spec.to_SheafedSpace, valued in the category of sheafed spaces andSpec.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.
Future work #
Adjunction between Γ and Spec
The spectrum of a commutative ring, as a topological space.
Equations
The induced map of a ring homomorphism on the ring spectra, as a morphism of topological spaces.
Equations
The spectrum, as a contravariant functor from commutative rings to topological spaces.
Equations
- algebraic_geometry.Spec.to_Top = {obj := λ (R : CommRingᵒᵖ), algebraic_geometry.Spec.Top_obj (opposite.unop R), map := λ (R S : CommRingᵒᵖ) (f : R ⟶ S), algebraic_geometry.Spec.Top_map f.unop, map_id' := algebraic_geometry.Spec.to_Top._proof_1, map_comp' := algebraic_geometry.Spec.to_Top._proof_2}
The spectrum of a commutative ring, as a SheafedSpace.
The induced map of a ring homomorphism on the ring spectra, as a morphism of sheafed spaces.
Equations
- algebraic_geometry.Spec.SheafedSpace_map f = {base := algebraic_geometry.Spec.Top_map f, c := {app := λ (U : (topological_space.opens ↥((algebraic_geometry.Spec.SheafedSpace_obj R).to_PresheafedSpace.carrier))ᵒᵖ), algebraic_geometry.structure_sheaf.comap f (opposite.unop U) ((topological_space.opens.map (algebraic_geometry.Spec.Top_map f)).obj (opposite.unop U)) _, naturality' := _}}
Spec, as a contravariant functor from commutative rings to sheafed spaces.
Equations
- algebraic_geometry.Spec.to_SheafedSpace = {obj := λ (R : CommRingᵒᵖ), algebraic_geometry.Spec.SheafedSpace_obj (opposite.unop R), map := λ (R S : CommRingᵒᵖ) (f : R ⟶ S), algebraic_geometry.Spec.SheafedSpace_map f.unop, map_id' := algebraic_geometry.Spec.to_SheafedSpace._proof_5, map_comp' := algebraic_geometry.Spec.to_SheafedSpace._proof_6}
Spec, as a contravariant functor from commutative rings to presheafed spaces.
The spectrum of a commutative ring, as a LocallyRingedSpace.
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.
The induced map of a ring homomorphism on the prime spectra, as a morphism of locally ringed spaces.
Spec, as a contravariant functor from commutative rings to locally ringed spaces.
Equations
- algebraic_geometry.Spec.to_LocallyRingedSpace = {obj := λ (R : CommRingᵒᵖ), algebraic_geometry.Spec.LocallyRingedSpace_obj (opposite.unop R), map := λ (R S : CommRingᵒᵖ) (f : R ⟶ S), algebraic_geometry.Spec.LocallyRingedSpace_map f.unop, map_id' := algebraic_geometry.Spec.to_LocallyRingedSpace._proof_1, map_comp' := algebraic_geometry.Spec.to_LocallyRingedSpace._proof_2}