The class of Lˣ ⧸ (Lˣ)^ℓ in G₀(k[Gal(L/K)])

Let L/K be a finite extension of nonarchimedean local fields with automorphism group G = L ≃ₐ[K] L, let ℓ be a prime which is nonzero in L, and let k be a field of characteristic ℓ. The multiplicative group Lˣ, written additively, is a G-module. This file computes the class of its reduction Lˣ ⧸ (Lˣ)^ℓ in the Grothendieck group G₀(k[G]) of finitely generated k[G]-modules, in terms of the lattice defect TauCeti.latticeDefect of the unit filtration:

[Lˣ ⧸ (Lˣ)^ℓ] = [k] + [μ_ℓ(L)] + latticeDefect (U(L,i))

for every i, where μ_ℓ(L) is the ℓ-torsion of Lˣ (TauCeti.reductionK0_quotSMulTop_units). Since [Lˣ ⧸ (Lˣ)^ℓ] - [μ_ℓ(L)] is by definition the defect of Lˣ, this is the statement latticeDefect Lˣ = 1 + latticeDefect (U(L,i)) (TauCeti.latticeDefect_units_eq_one_add). It follows from the additivity of the defect along the valuation sequence 0 → 𝒪[L]ˣ → Lˣ → ℤ → 0, whose quotient ℤ has the trivial action and defect 1 (TauCeti.latticeDefect_int_eq_one), and from the invariance of the defect under the inclusions U(L,i) ⊆ 𝒪[L]ˣ, which have finite index (TauCeti.latticeDefect_unitFiltration_eq). When ℓ is a unit of 𝒪[L], raising to the ℓ-th power is bijective on the principal units, whose defect therefore vanishes, and [Lˣ ⧸ (Lˣ)^ℓ] = [k] + [μ_ℓ(L)] (TauCeti.reductionK0_quotSMulTop_units_of_isUnit).

At the residue characteristic ℓ = p, when K is a finite extension of ℚ_[p] and L/K is Galois, the defect of the principal units is [K : ℚ_p] · [k[G]], so that [Lˣ ⧸ (Lˣ)^p] = [k] + [μ_p(L)] + [K : ℚ_p] · [k[G]] (TauCeti.reductionK0_quotSMulTop_units_eq_add_finrank_smul). For (p - 1) n > e, with e the absolute ramification index of L, the logarithm identifies the deep units U(L,n) Galois-equivariantly with 𝓂[L]^n (TauCeti.deepUnitExpLogEquiv), which has finite index in 𝒪[L]; so U(L,n) has the defect of 𝒪[L] (TauCeti.latticeDefect_unitFiltration_eq_integerRing), computed in TauCeti.latticeDefect_integerRing_eq_finrank_smul.

This is the computation of the units of L that enters the proof of the local Euler characteristic formula, where Kummer theory identifies H¹(L, μ_ℓ) with Lˣ ⧸ (Lˣ)^ℓ.

The finiteness of the reductions and torsion subgroups, which the definition of the defect asks for, is recorded by instances: Lˣ ⧸ (Lˣ)^ℓ is finite since (Lˣ)^ℓ has finite index (TauCeti.finiteIndex_range_powMonoidHom), and the reductions of the U(L,i) are then finite by the snake lemma (TauCeti.finite_quotSMulTop_of_exact).

Main results

• TauCeti.latticeDefect_unitFiltration_eq: all steps of the unit filtration have the same defect.
• TauCeti.latticeDefect_units_eq_one_add: the defect of Lˣ is 1 plus that of U(L,i).
• TauCeti.latticeDefect_unitFiltration_succ_eq_zero_of_isUnit: away from the residue characteristic, the positive-depth steps have zero defect.
• TauCeti.latticeDefect_unitFiltration_eq_integerRing: deep units have the defect of 𝒪[L].
• TauCeti.latticeDefect_unitFiltration_eq_finrank_smul: at ℓ = p, every step of the unit filtration has defect [K : ℚ_p] · [k[G]].
• TauCeti.reductionK0_quotSMulTop_units, TauCeti.reductionK0_quotSMulTop_units_of_isUnit and TauCeti.reductionK0_quotSMulTop_units_eq_add_finrank_smul: the class of Lˣ ⧸ (Lˣ)^ℓ.

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., Springer (2008), §VII.3, (7.3.3) and the proof of (7.3.1).
• J. S. Milne, Arithmetic Duality Theorems, 2nd ed., Chapter I, proof of Theorem 2.8.

Finiteness of the torsion and of the reductions modulo ℓ

instance TauCeti.finite_torsionBy_additive_unitFiltration {L : Type u_1} [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] (n : ℕ) [NeZero n] (i : ℕ) : Finite ↥(Submodule.torsionBy ℤ (Additive ↥(unitFiltration L i)) ↑n)

The n-torsion of every step of the unit filtration, written additively, is finite.

instance TauCeti.finite_quotSMulTop_additive_units {L : Type u_1} [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] (n : ℕ) [NeZero ↑n] : Finite (QuotSMulTop (↑n) (Additive Lˣ))

When n is nonzero in L, the reduction Lˣ ⧸ (Lˣ)^n of the multiplicative group, written additively, is finite.

instance TauCeti.finite_quotSMulTop_additive_unitFiltration {L : Type u_1} [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] (n : ℕ) [NeZero ↑n] (i : ℕ) : Finite (QuotSMulTop (↑n) (Additive ↥(unitFiltration L i)))

When n is nonzero in L, the reduction U(L,i) ⧸ U(L,i)^n of every step of the unit filtration, written additively, is finite.

The Galois module Lˣ

theorem TauCeti.latticeDefect_unitFiltration_eq (K L : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] (k : Type) (ℓ : ℕ) [CommRing k] [Fact (Nat.Prime ℓ)] [NeZero ↑ℓ] (i j : ℕ) : latticeDefect k Gal(L/K) ℓ (Additive ↥(unitFiltration L i)) = latticeDefect k Gal(L/K) ℓ (Additive ↥(unitFiltration L j))

The defect does not depend on the step of the unit filtration: all the U(L,i) have finite index in U(L,0) = 𝒪[L]ˣ, so they have the same lattice defect.

theorem TauCeti.latticeDefect_units_eq_one_add (K L : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] (k : Type) (ℓ : ℕ) [Field k] [Fact (Nat.Prime ℓ)] [CharP k ℓ] [NeZero ↑ℓ] (i : ℕ) : latticeDefect k Gal(L/K) ℓ (Additive Lˣ) = 1 + latticeDefect k Gal(L/K) ℓ (Additive ↥(unitFiltration L i))

The lattice defect of Lˣ: along the valuation sequence 0 → 𝒪[L]ˣ → Lˣ → ℤ → 0, whose quotient ℤ carries the trivial action, and the inclusions of finite index U(L,i) ⊆ 𝒪[L]ˣ, the defect of Lˣ is that of any step U(L,i) of the unit filtration plus the class 1 = [k] of the trivial line.

theorem TauCeti.latticeDefect_unitFiltration_succ_eq_zero_of_isUnit (K L : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] (k : Type) (ℓ : ℕ) [CommRing k] (hℓ : IsUnit ↑ℓ) (i : ℕ) : latticeDefect k Gal(L/K) ℓ (Additive ↥(unitFiltration L (i + 1))) = 0

Away from the residue characteristic the principal units have zero defect: if ℓ is a unit of 𝒪[L], raising to the ℓ-th power is bijective on every positive-depth step U(L,i+1), so its reduction modulo ℓ and its ℓ-torsion both vanish.

theorem TauCeti.reductionK0_quotSMulTop_units (K L : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] (k : Type) (ℓ : ℕ) [Field k] [Fact (Nat.Prime ℓ)] [CharP k ℓ] [NeZero ↑ℓ] (i : ℕ) : reductionK0 k ((Representation.ofDistribMulAction ℤ Gal(L/K) (Additive Lˣ)).quotSMulTop ↑ℓ) = 1 + reductionK0 k ((Representation.ofDistribMulAction ℤ Gal(L/K) (Additive Lˣ)).torsionBy ↑ℓ) + latticeDefect k Gal(L/K) ℓ (Additive ↥(unitFiltration L i))

The class of Lˣ ⧸ (Lˣ)^ℓ in G₀(k[Gal(L/K)]), for k of characteristic ℓ: it is [k] + [μ_ℓ(L)] + latticeDefect (U(L,i)) for every step U(L,i) of the unit filtration, where μ_ℓ(L) is the ℓ-torsion of Lˣ.

theorem TauCeti.reductionK0_quotSMulTop_units_of_isUnit (K L : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] (k : Type) (ℓ : ℕ) [Field k] [Fact (Nat.Prime ℓ)] [CharP k ℓ] (hℓ : IsUnit ↑ℓ) : reductionK0 k ((Representation.ofDistribMulAction ℤ Gal(L/K) (Additive Lˣ)).quotSMulTop ↑ℓ) = 1 + reductionK0 k ((Representation.ofDistribMulAction ℤ Gal(L/K) (Additive Lˣ)).torsionBy ↑ℓ)

The class of Lˣ ⧸ (Lˣ)^ℓ away from the residue characteristic: if ℓ is a unit of 𝒪[L], then [Lˣ ⧸ (Lˣ)^ℓ] = [k] + [μ_ℓ(L)] in G₀(k[Gal(L/K)]).

The residue characteristic

theorem TauCeti.latticeDefect_unitFiltration_eq_integerRing (K L : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] (k : Type) (p : ℕ) [Fact (Nat.Prime p)] [FinitePadicExtension L p] [CommRing k] {n : ℕ} (hn : absoluteRamificationIndex L p < (p - 1) * n) : latticeDefect k Gal(L/K) p (Additive ↥(unitFiltration L n)) = latticeDefect k Gal(L/K) p ↥(ValuativeRel.valuation L).integer

The deep units have the defect of the integers: for (p - 1) n > e, the logarithm identifies U(L,n) Galois-equivariantly with 𝓂[L]^n, which has finite index in 𝒪[L], so U(L,n) and the lattice 𝒪[L] have the same p-defect.

theorem TauCeti.latticeDefect_unitFiltration_eq_finrank_smul (K L : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] (k : Type) (p : ℕ) [Fact (Nat.Prime p)] [FinitePadicExtension L p] [FinitePadicExtension K p] [IsGalois K L] [CommRing k] [CharP k p] (i : ℕ) : latticeDefect k Gal(L/K) p (Additive ↥(unitFiltration L i)) = Module.finrank ℚ_[p] K • permK0 k Gal(L/K) Gal(L/K)

The p-defect of the unit filtration of a finite Galois extension L/K of finite extensions of ℚ_p: every step U(L,i) has defect [K:ℚ_p] · [k[G]] in G₀(k[G]), G = Gal(L/K), for k of characteristic p.

theorem TauCeti.reductionK0_quotSMulTop_units_eq_add_finrank_smul (K L : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] (k : Type) (p : ℕ) [Fact (Nat.Prime p)] [FinitePadicExtension L p] [FinitePadicExtension K p] [IsGalois K L] [Field k] [CharP k p] : reductionK0 k ((Representation.ofDistribMulAction ℤ Gal(L/K) (Additive Lˣ)).quotSMulTop ↑p) = 1 + reductionK0 k ((Representation.ofDistribMulAction ℤ Gal(L/K) (Additive Lˣ)).torsionBy ↑p) + Module.finrank ℚ_[p] K • permK0 k Gal(L/K) Gal(L/K)

The class of Lˣ ⧸ (Lˣ)^p in G₀(k[Gal(L/K)]), for L/K a finite Galois extension of finite extensions of ℚ_p and k of characteristic p: [Lˣ ⧸ (Lˣ)^p] = [k] + [μ_p(L)] + [K:ℚ_p] · [k[G]].