The normalized valuation of a nonarchimedean local field #
Mathlib equips a nonarchimedean local field K with a valuation ValuativeRel.valuation K
taking values in an abstract value group ValueGroupWithZero K, together with an order
isomorphism IsNonarchimedeanLocalField.valueGroupWithZeroIsoInt of that group with ℤᵐ⁰.
This file assembles them into the additively normalized valuation of a local field, the monoid
homomorphism
normalizedValuation K : Kˣ →* Multiplicative ℤ,
whose value at a uniformizer is Multiplicative.ofAdd 1, and its zero-preserving extension
normalizedValuationWithZero K : K →*₀ ℤᵐ⁰. An integer is recovered from a nonzero value by
decoding with Multiplicative.toAdd. The associated rational-valued absolute value is
normalizedAbsoluteValue K : AbsoluteValue K ℚ≥0.
Its value at a nonzero x is q ^ (-v_K(x)), where q is the cardinality of the residue field.
Main definitions #
TauCeti.normalizedValuation: the normalized valuationv_K^×of a nonarchimedean local field, as a homomorphism from the unit group toMultiplicative ℤ.TauCeti.normalizedValuationWithZero: its zero-preserving extension to all of the field.TauCeti.normalizedValuationMod: the normalized valuation reduced modulon, as an additive homomorphismAdditive Kˣ →+ ZMod n.TauCeti.normalizedAbsoluteValue: the normalizedℚ≥0-valued absolute value associated tonormalizedValuation.
Main results #
TauCeti.toAdd_normalizedValuation_eq_neg_log: the translation between the multiplicative convention ofValuativeRel.valuationand the additive normalization.TauCeti.normalizedValuation_surjective: the normalized value group is all ofℤ.TauCeti.normalizedValuationMod_surjective: every residue modulonis the normalized valuation of a unit.TauCeti.normalizedValuation_irreducible: an irreducible element of𝒪[K]has normalized valuation1; that is, uniformizers are exactly where the normalization is pinned.TauCeti.toAdd_normalizedValuation_eq_iff_valuation_eq_zpowand its two one-sided forms: the powers of a uniformizer translate the additive normalization intoValuativeRel.valuation.TauCeti.normalizedValuationWithZero_eq_ordFrac: the zero-preserving normalized valuation is Mathlib's order-of-vanishing mapRing.ordFrac 𝒪[K], which is where the discrete-valuation-ring API for it comes from.Valuation.normalizedValuationWithZero_eq_inv_of_surjective: the zero-preserving normalized valuation is the inverse of any surjectiveℤᵐ⁰-valued valuation compatible withK.TauCeti.normalizedValuation_eq_one_of_isOfFinOrder: the normalized valuation vanishes on the roots of unity ofK.TauCeti.normalizedValuation_neg: negation does not change the normalized valuation.TauCeti.even_toAdd_normalizedValuation_of_isSquare: a square has even normalized valuation.TauCeti.normalizedAbsoluteValue_apply_ne_zero: the formula|x|_K = q ^ (-v_K(x)).TauCeti.isNonarchimedean_normalizedAbsoluteValue: the normalized absolute value satisfies the strong triangle inequality.TauCeti.normalizedAbsoluteValue_le_normalizedAbsoluteValue_iffandTauCeti.normalizedAbsoluteValue_lt_normalizedAbsoluteValue_iff: the normalized absolute value orders the elements ofKasValuativeRel.valuationdoes.TauCeti.eq_normalizedValuation: the kernel condition together with the uniformizer equation characterizes the normalized valuation among homomorphismsKˣ →* Multiplicative ℤ.TauCeti.isUnit_iff_normalizedValuationWithZero_eq_one,TauCeti.mem_integer_iff_toAdd_normalizedValuation_nonnegandTauCeti.dvd_iff_toAdd_normalizedValuation_le: the normalized valuation reads off the units, the elements and the divisibility relation of the ring of integers.
Implementation notes #
Mathlib's convention is multiplicative and decreasing: valuation K π < 1 at a uniformizer π,
and the integers of K are the elements of valuation at most 1. The additive normalization
therefore carries a minus sign, and that sign is confined to the single translation lemma
toAdd_normalizedValuation_eq_neg_log; every statement mixing the two conventions is derived
from it.
The group-valued normalized valuation is defined on Kˣ because Multiplicative ℤ has no room
for the value at 0; normalizedValuationWithZero supplies the corresponding map on all of K.
References #
- J.-P. Serre, Corps Locaux, Chapter I, §§1–2.
- J. Neukirch, Algebraic Number Theory, Chapter II, §§3–4.
The normalized valuation v_K^× of a nonarchimedean local field K: the composite of
ValuativeRel.valuation K with the order isomorphism valueGroupWithZeroIsoInt of the value
group with ℤᵐ⁰, read additively and with the sign chosen so that a uniformizer has value
Multiplicative.ofAdd 1.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The normalized valuation extended across zero, as a zero-preserving monoid homomorphism
from K to ℤᵐ⁰.
Equations
Instances For
The zero-preserving normalized valuation vanishes exactly at zero.
The zero-preserving normalized valuation restricts to normalizedValuation on Kˣ.
The normalized valuation of a local field is the order of vanishing along 𝒪[K]: it agrees
with Mathlib's Ring.ordFrac, the canonical ℤᵐ⁰-valued order map of a discrete valuation ring
on its fraction field. The Ring.ordFrac API therefore applies to normalizedValuationWithZero.
The zero-preserving normalized valuation is the inverse of any surjective ℤᵐ⁰-valued
valuation compatible with the valuative relation of K. This is how a concrete discrete
valuation, such as the adic valuation of a completion, is read as the normalized one.
The translation between Mathlib's multiplicative valuation and the additive normalization:
the normalized valuation is minus the logarithm of ValuativeRel.valuation, transported to
ℤᵐ⁰. Every comparison of the two conventions goes through this lemma.
The translation of toAdd_normalizedValuation_eq_neg_log read in the other direction: Mathlib's
valuation of a unit is recovered from the normalized valuation by exponentiating its negative.
The normalized valuation vanishes exactly on the elements of valuation 1.
The normalized valuation vanishes on every root of unity: Multiplicative ℤ is torsion
free, so a unit of finite order has normalized valuation 1.
Negation does not change the normalized valuation: -1 is a root of unity.
A square has even normalized valuation.
The normalized valuation reverses the order of Mathlib's valuation.
A uniformizer has normalized valuation n in its n-th power.
The powers of a uniformizer measure the normalized valuation: n ≤ v_K(x) exactly when the
multiplicative valuation of x is at most that of ϖ ^ n.
The powers of a uniformizer measure the normalized valuation, in the other direction.
The normalized valuation of x is n exactly when x and ϖ ^ n have the same
multiplicative valuation.
A unit of K lies in the ring of integers exactly when its normalized valuation is
nonnegative.
The normalized value group of a nonarchimedean local field is all of ℤ.
The normalized valuation of K reduced modulo n, as an additive homomorphism
Additive Kˣ →+ ZMod n.
Equations
Instances For
The normalized valuation modulo n of a ∈ Kˣ is the residue of v_K(a).
The normalized valuation modulo n is surjective.
An element of the ring of integers is a unit there exactly when its zero-preserving normalized valuation is one.
Divisibility in the ring of integers is monotonicity of the normalized valuation.
Every unit of K is a unit of 𝒪[K] times an integer power of a fixed irreducible element
of 𝒪[K].
The normalized valuation of an irreducible element of 𝒪[K], that is of a uniformizer of
K, is Multiplicative.ofAdd 1.
The normalized valuation is the unique homomorphism Kˣ →* Multiplicative ℤ that vanishes
on the elements of valuation 1 and takes the value Multiplicative.ofAdd 1 at a uniformizer.
The valuation of an irreducible element of 𝒪[K] generates the value group: every nonzero
value is an integer power of it.
The normalized absolute value of a nonarchimedean local field, with values in ℚ≥0.
For a nonzero element x, its value is q ^ (-v_K(x)), where
q = Nat.card 𝓀[K] is the cardinality of the residue field.
Equations
Instances For
The normalized absolute value is the rational power q ^ (-v_K(x)) at every nonzero
element, where q is the cardinality of the residue field.
The normalized absolute value on Kˣ is the rational power q ^ (-v_K(x)).
The normalized absolute value of an irreducible element of 𝒪[K], that is of a uniformizer
of K, is the inverse of the residue-field cardinality.
The normalized absolute value satisfies the strong triangle inequality.
The normalized absolute value induces the order of Mathlib's valuation.
The normalized absolute value induces the strict order of Mathlib's valuation.
The normalized absolute value is less than one exactly on the elements of valuation less than one, that is, on the maximal ideal of the ring of integers.
The normalized absolute value takes the value one exactly on the elements of valuation one, that is, on the units of the ring of integers.
An element belongs to the ring of integers exactly when its normalized absolute value is at most one.
The normalized absolute value is one on every unit of the ring of integers.
The normalized absolute value is one on every root of unity.