$Spec$ as a functor to locally ringed spaces. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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.
Related results #
The adjunction Γ ⊣ Spec is constructed in algebraic_geometry/Gamma_Spec_adjunction.lean.
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_1, map_comp' := algebraic_geometry.Spec.to_SheafedSpace._proof_2}
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.
Equations
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}
Instances for algebraic_geometry.Spec.to_LocallyRingedSpace
- algebraic_geometry.Spec.to_LocallyRingedSpace.category_theory.limits.preserves_limits
- algebraic_geometry.Spec.to_LocallyRingedSpace.category_theory.full
- algebraic_geometry.Spec.to_LocallyRingedSpace.category_theory.faithful
- algebraic_geometry.Spec.to_LocallyRingedSpace.category_theory.is_right_adjoint
- algebraic_geometry.Spec.to_LocallyRingedSpace.category_theory.reflective
The counit morphism R ⟶ Γ(Spec R) given by algebraic_geometry.structure_sheaf.to_open.
Instances for algebraic_geometry.to_Spec_Γ
The counit (Spec_Γ_identity.inv.op) 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
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 is_localized_module_to_pushforward_stalk_alg_hom.
This is the alg_hom version of to_pushforward_stalk, which is the map S ⟶ (f∗ 𝒪ₛ)ₚ for some
algebra R ⟶ S and some p : Spec R.
Equations
- algebraic_geometry.structure_sheaf.to_pushforward_stalk_alg_hom R S p = {to_fun := (algebraic_geometry.structure_sheaf.to_pushforward_stalk (algebra_map ↥R ↥S) p).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}