$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.
In progress #
Adjunction between Γ and Spec: Currently, the counit of the adjunction is proven to be a
natural transformation in Spec_Γ_naturality, and realized as a natural isomorphism in
Spec_Γ_identity.
TODO: provide the unit, and prove the triangle identities.
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.
Equations
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.
Equations
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}
The morphism R ⟶ Γ(Spec R) given by algebraic_geometry.structure_sheaf.to_open.
The counit of the adjunction Γ ⊣ Spec is an isomorphism.
Equations
- algebraic_geometry.Spec_Γ_identity = (category_theory.nat_iso.of_components (λ (R : CommRing), category_theory.as_iso (algebraic_geometry.to_Spec_Γ R)) algebraic_geometry.Spec_Γ_identity._proof_1).symm