The multiplicative group of a nonarchimedean local field #
Let K be a nonarchimedean local field, with normalized valuation v_K, integer ring 𝒪[K],
residue field 𝓀[K] of cardinality q, and unit filtration U(K,i). This file resolves Kˣ
into its three standard pieces:
TauCeti.unitsEquivProd, attached to a choice of uniformizer π, is the isomorphism
Kˣ ≃* Multiplicative ℤ × 𝒪[K]ˣ,
whose first component is v_K and whose inverse sends (n, u) to π ^ n * u, and
TauCeti.integerUnitsEquivProd, which needs no choice, is the isomorphism
𝒪[K]ˣ ≃* 𝓀[K]ˣ × U(K,1),
whose first component is reduction and whose inverse sends (α, y) to ω(α) * y, where ω is
the Teichmüller lift. Since ω identifies 𝓀[K]ˣ with the group μ_{q-1} of (q-1)-st roots
of unity of 𝒪[K] (TauCeti.range_teichmuller), the second isomorphism is the
splitting of the units of 𝒪[K] into their prime-to-p torsion and the principal units.
Both splittings come from the same mechanism: an exact sequence of abelian groups with a
distinguished section. For the first, the surjection is v_K, whose kernel is U(K,0)
(TauCeti.ker_normalizedValuation), and the section is n ↦ π ^ n; the dependence on π is
confined to that section, and the first component of the splitting is v_K no matter which
uniformizer is chosen. For the second, the surjection is reduction 𝒪[K]ˣ → 𝓀[K]ˣ, whose
kernel is U(K,1) (TauCeti.mem_unitFiltration_one_iff_residue_eq_one), and the section is the
Teichmüller lift.
Together the two reduce every multiplicative question about K to one about ℤ, about the
finite group 𝓀[K]ˣ, and about the principal units U(K,1), whose own structure is read off
the graded pieces of the unit filtration. This is the shape used to count power classes
Kˣ / (Kˣ)ⁿ and to compute norm groups.
Main definitions #
TauCeti.unitsProdHomandTauCeti.unitsEquivProd: the splittingKˣ ≃* Multiplicative ℤ × 𝒪[K]ˣattached to a uniformizer.TauCeti.integerUnitsProdHomandTauCeti.integerUnitsEquivProd: the Teichmüller splitting𝒪[K]ˣ ≃* 𝓀[K]ˣ × U(K,1).
Main results #
TauCeti.ker_normalizedValuation: the kernel of the normalized valuation isU(K,0).TauCeti.fst_unitsEquivProd: theℤ-component of the first splitting is the normalized valuation; in particular it does not depend on the uniformizer.TauCeti.fst_integerUnitsEquivProd: the𝓀[K]ˣ-component of the second splitting is reduction.TauCeti.unitsMap_subtype_snd_unitsEquivProdandTauCeti.unitFiltrationToIntegerUnits_snd_integerUnitsEquivProd: the remaining components, which are what is left after dividing by the image of the section.TauCeti.exists_forall_pow_eq_mem_unitFiltration_mul_zpow: for anyϖof nonzero valuation and any depthi, the quotientKˣ / (U(K,i) · ϖ ^ ℤ)has finite exponent.
References #
- J.-P. Serre, Corps Locaux, Chapter II, §§4–5.
- J. Neukirch, Algebraic Number Theory, Chapter II, §5.
The kernel of the normalized valuation #
The normalized valuation is trivial on the units of 𝒪[K].
The valuation splitting Kˣ ≃ ℤ × 𝒪[K]ˣ #
The homomorphism (n, u) ↦ π ^ n * u out of Multiplicative ℤ × 𝒪[K]ˣ, built from a
uniformizer π of K. It is the section-and-inclusion map of the exact sequence
1 → 𝒪[K]ˣ → Kˣ → ℤ → 1, and unitsProdHom_bijective shows that it splits it.
Equations
- TauCeti.unitsProdHom hπ = ((zpowersHom Kˣ) (Units.mk0 ↑π ⋯)).coprod (Units.map ↑(ValuativeRel.valuation K).integer.subtype)
Instances For
The defining formula of unitsProdHom.
A uniformizer splits Kˣ. Every unit of K is uniquely π ^ n * u with n : ℤ and
u a unit of 𝒪[K].
The multiplicative group of a local field, split by a uniformizer: Kˣ is the product
of ℤ, through the normalized valuation, and the units of 𝒪[K]. The isomorphism depends on
the uniformizer π only through its inverse unitsEquivProd_symm_apply; its first component is
normalizedValuation K, by fst_unitsEquivProd.
Equations
Instances For
The inverse of the splitting attached to π is (n, u) ↦ π ^ n * u.
The ℤ-component of the splitting attached to a uniformizer is the normalized valuation.
In particular it is the same for every uniformizer.
The 𝒪[K]ˣ-component of the splitting attached to π is x divided by π ^ v_K(x).
The Teichmüller splitting 𝒪[K]ˣ ≃ 𝓀[K]ˣ × U(K,1) #
The homomorphism (α, y) ↦ ω(α) * y out of 𝓀[K]ˣ × U(K,1), where ω is the Teichmüller
lift. It is the section-and-inclusion map of the reduction sequence
1 → U(K,1) → 𝒪[K]ˣ → 𝓀[K]ˣ → 1, and integerUnitsProdHom_bijective shows that it splits
it.
Equations
Instances For
The defining formula of integerUnitsProdHom.
The Teichmüller lift splits the units of 𝒪[K]. Every unit of 𝒪[K] is uniquely the
product of a (q-1)-st root of unity and a principal unit.
The units of the integer ring of a local field, split by the Teichmüller lift: 𝒪[K]ˣ
is the product of the multiplicative group of the residue field, through reduction, and the
principal units U(K,1). The residue-field factor is carried by the (q-1)-st roots of unity
of 𝒪[K], which TauCeti.range_teichmuller identifies with the image of the lift.
Instances For
The inverse of the Teichmüller splitting is (α, y) ↦ ω(α) * y.
The residue-field component of the Teichmüller splitting is reduction.
The principal-unit component of the Teichmüller splitting is u divided by the Teichmüller
representative of its residue.
Units up to a deep unit and a power of a fixed element #
For every depth i and every ϖ : Kˣ of nonzero valuation, a single exponent M ≠ 0
carries every unit of K into U(K,i) · ϖ ^ ℤ: Kˣ / (U(K,i) · ϖ ^ ℤ) has finite exponent.
Taking ϖ = p in a p-adic field, this is how Kˣ is compared with its deep units, on which
the logarithm is an isomorphism.