Discrete valuation rings of an algebraic extension of a local field

Let K be a nonarchimedean local field and M an algebraic extension of K. A discrete valuation ring S with fraction field M which lies over 𝒪[K] through a local homomorphism defines a valuation on M whose restriction to K has valuation ring 𝒪[K] (TauCeti.isEquiv_comap_valuation_maximalIdeal_of_isLocalHom). Since the valuation of K extends uniquely to M (TauCeti.algebraicExtensionValuation_isEquiv), the valuation of S is the extended valuation, and in particular S lies inside 𝒪[M].

This is what lets a statement phrased with an abstract discrete valuation ring dominating 𝒪[K], such as potential good reduction, be read over the ring of integers of an algebraic extension.

Main results

• TauCeti.isEquiv_valuation_maximalIdeal_of_isLocalHom: the valuation of S is equivalent to the valuation of M.
• TauCeti.valuation_algebraMap_le_one_of_isLocalHom: the elements of S have valuation at most 1 in M.

References

• J. Neukirch, Algebraic Number Theory, Chapter II, §4 (Theorem 4.8).

theorem TauCeti.isEquiv_valuation_maximalIdeal_of_isLocalHom {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {M : Type u_2} [Field M] [Algebra K M] [Algebra.IsAlgebraic K M] {S : Type u_3} [CommRing S] [IsDomain S] [IsDiscreteValuationRing S] [Algebra S M] [IsFractionRing S M] [Algebra (↥(ValuativeRel.valuation K).integer) S] [IsLocalHom (algebraMap (↥(ValuativeRel.valuation K).integer) S)] [ValuativeRel M] [ValuativeExtension K M] (h : (algebraMap S M).comp (algebraMap (↥(ValuativeRel.valuation K).integer) S) = (algebraMap K M).comp (algebraMap (↥(ValuativeRel.valuation K).integer) K)) : (IsDedekindDomain.HeightOneSpectrum.valuation M (IsDiscreteValuationRing.maximalIdeal S)).IsEquiv (ValuativeRel.valuation M)

A discrete valuation ring dominating 𝒪[K] defines the extended valuation. Let S be a discrete valuation ring with fraction field an algebraic extension M of K, lying over 𝒪[K] through a local homomorphism. Its valuation is equivalent to the valuation of any valuative relation on M extending that of K.

theorem TauCeti.valuation_algebraMap_le_one_of_isLocalHom {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {M : Type u_2} [Field M] [Algebra K M] [Algebra.IsAlgebraic K M] {S : Type u_3} [CommRing S] [IsDomain S] [IsDiscreteValuationRing S] [Algebra S M] [IsFractionRing S M] [Algebra (↥(ValuativeRel.valuation K).integer) S] [IsLocalHom (algebraMap (↥(ValuativeRel.valuation K).integer) S)] [ValuativeRel M] [ValuativeExtension K M] (h : (algebraMap S M).comp (algebraMap (↥(ValuativeRel.valuation K).integer) S) = (algebraMap K M).comp (algebraMap (↥(ValuativeRel.valuation K).integer) K)) (s : S) : (ValuativeRel.valuation M) ((algebraMap S M) s) ≤ 1

A discrete valuation ring dominating 𝒪[K] lies in 𝒪[M]. Every element of a discrete valuation ring S with fraction field M, lying over 𝒪[K] through a local homomorphism, has valuation at most 1 for any valuative relation on M extending that of K.