EtaleFundamentalGroups.geometricallyIntegral_localizationAtPrimeMapResidueField
Geometric integrality of a prime residue field persists after extending the prime to a localization at a containing prime.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry
namespace EtaleFundamentalGroups
universe uLean source · full declaration
theorem geometricallyIntegral_localizationAtPrimeMapResidueField
{k A : Type u} [Field k] [CommRing A]
(P q : Ideal A) [P.IsPrime] [q.IsPrime] (hqP : q ≤ P)
[Algebra k q.ResidueField]
(hgeo : GeometricallyIntegral
(Spec.map (CommRingCat.ofHom
(algebraMap k q.ResidueField)))) :
let qV := q.map (algebraMap A (Localization.AtPrime P))
letI : qV.IsPrime :=
Ideal.isPrime_map_of_isLocalizationAtPrime P hqP
let e := localizationAtPrimeMapResidueFieldRingEquiv A P q hqP
letI : Algebra k qV.ResidueField :=
(e.toRingHom.comp (algebraMap k q.ResidueField)).toAlgebra
GeometricallyIntegral
(Spec.map (CommRingCat.ofHom
(algebraMap k qV.ResidueField))) := by
exact geometricallyIntegral_specMap_transport_ringEquiv'
(localizationAtPrimeMapResidueFieldRingEquiv A P q hqP) hgeo