The Herbrand quotient of the units of a local field

Let L/K be a finite Galois extension of nonarchimedean local fields whose Galois group G = L ≃ₐ[K] L is cyclic. This file proves that the Herbrand quotient of the unit group 𝒪[L]ˣ = U(L, 0), with its Galois action and read as an integral representation of G, is 1 (TauCeti.TateCohomology.herbrandQuotient_unitFiltration_zero). Together with the Herbrand quotient |G| of the trivial module ℤ and the valuation sequence 0 → 𝒪[L]ˣ → Lˣ → ℤ → 0, this is the cyclic computation h(Lˣ) = [L : K] from which the order of H²(G, Lˣ) is bounded by the degree.

The unit group is replaced by a commensurable one on which the computation can be carried out. For a uniformizer ϖ of K, a scaled normal basis element spans a Galois-stable lattice A ⊆ 𝒪[L], free of rank one over 𝒪[K][G], whose unit filtration 1 + ϖ ^ n • A (TauCeti.IsUnitFiltrationLattice.filtration) consists of open subgroups of 𝒪[L]ˣ. Its step zero 1 + A has finite index in 𝒪[L]ˣ, so by invariance of the Herbrand quotient under maps with finite cokernel it suffices to show that the Herbrand quotient of 1 + A is 1. The filtration of 1 + A is separated and complete, and each graded piece is A ⧸ ϖ • A, free of rank one over (𝒪[K] ⧸ ϖ)[G], hence with vanishing Tate cohomology; successive approximation (TauCeti.TateCohomology.herbrandQuotient_eq_one_of_filtration) then gives the claim. The filtration is used instead of the unit filtration U(L, i) of L, whose graded pieces are the residue field of L and are in general not free over the group ring.

Main results

• TauCeti.TateCohomology.herbrandQuotient_unitFiltration_zero: the Herbrand quotient of 𝒪[L]ˣ is 1 for a cyclic extension L/K of nonarchimedean local fields.

References

• J.-P. Serre, Local Fields, Chapter IX, §3, Lemma 2 and Proposition 3.
• J.-P. Serre, Local class field theory, in J. W. S. Cassels and A. Fröhlich (eds.), Algebraic Number Theory, Chapter VI, §1.4.
• J. Neukirch, Algebraic Number Theory, Chapter V, Proposition 1.2.

Step zero of the filtration as an integral representation

The graded pieces

Comparison with the unit group

@[simp]

theorem TauCeti.TateCohomology.herbrandQuotient_unitFiltration_zero {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] [IsGalois K L] [IsCyclic Gal(L/K)] : herbrandQuotient (Rep.ofMulDistribMulAction Gal(L/K) ↥(unitFiltration L 0)) = 1

The Herbrand quotient of the local units. For a finite Galois extension L/K of nonarchimedean local fields with cyclic Galois group G, the Herbrand quotient of the unit group 𝒪[L]ˣ = U(L, 0), with its Galois action and read as an integral representation of G, is 1: its Tate cohomology groups in degrees 0 and -1 are finite of the same order.