Natural-number valuations in adic completions

Let v be a height-one prime of a Dedekind domain R, with finite residue field and fraction field K. For a natural number whose image in the completion K_v is nonzero, its normalized additive valuation there is the exponent of v in the principal ideal that the number generates in R.

This identifies the local-field normalization, in which a uniformizer has valuation one, with the global ideal-theoretic normalization by prime multiplicity. It is the bridge needed when a local ramification bound contains the valuation of a natural number and is transported back to a global prime.

Main result

• IsDedekindDomain.HeightOneSpectrum.natCastValuation_completion_eq_multiplicity_span: for v with finite residue field, if the image of n in K_v is nonzero, its normalized valuation there is the multiplicity of v in (n).

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.natCastValuation_completion_eq_multiplicity_span {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) [Finite (R ⧸ v.asIdeal)] (n : ℕ) (hn : ↑n ≠ 0) : TauCeti.natCastValuation (adicCompletion K v) n hn = multiplicity v.asIdeal (Ideal.span {↑n})

If a height-one prime has finite residue field and a natural number has nonzero image in its adic completion, the normalized valuation there is its multiplicity in the corresponding global principal ideal.