Rat.LocalizationAt.exists_specMap_comp_eq_fromSpecResidueField
The residue-field map induced from the rational localization at a prime.
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open AlgebraicGeometry CategoryTheory
namespace Rat.LocalizationAtLean source · statement
theorem exists_specMap_comp_eq_fromSpecResidueField
(p : ℕ) [Fact p.Prime] (s : Spec (CommRingCat.of ℤ))
(hs : s.asIdeal = Ideal.span {(p : ℤ)}) :
∃ φ : ↥(Rat.LocalizationAt p) →+* (Spec (CommRingCat.of ℤ)).residueField s,
Function.Surjective φ ∧ φ (p : ↥(Rat.LocalizationAt p)) = 0 ∧
Spec.map (CommRingCat.ofHom φ) ≫
Spec.map (CommRingCat.ofHom (algebraMap ℤ ↥(Rat.LocalizationAt p))) =
(Spec (CommRingCat.of ℤ)).fromSpecResidueField s