Fraction fields of discrete valuation rings #
This file relates the two natural descriptions of the fraction field of a discrete valuation ring. Besides being the localization at all non-zero elements, it is the localization away from any uniformizer. This identifies the induced map of spectra with a principal open immersion.
theorem
TauCeti.isLocalizationAway_fractionRing
{R : Type u_1}
{K : Type u_2}
[CommRing R]
[IsDomain R]
[IsDiscreteValuationRing R]
[CommSemiring K]
[Algebra R K]
[IsFractionRing R K]
{ϖ : R}
(hϖ : Irreducible ϖ)
:
The fraction field of a discrete valuation ring is the localization away from any
uniformizer. Here uniformizers are expressed using Mathlib's equivalent Irreducible predicate.