The Herbrand quotient of the units of a local field

For a cyclic extension L/K of nonarchimedean local fields, the equivariant valuation sequence expresses the Herbrand quotient of Lˣ as the product of [L : K] and the Herbrand quotient of the valuation-zero units. The latter is one, so h(Lˣ) = [L : K].

Main results

• TauCeti.herbrandQuotient_units_eq_finrank: h(Lˣ) = [L : K] for cyclic L/K.

References

• J.-P. Serre, Local Fields, Chapter VIII, §4 and Chapter IX, §3.

theorem TauCeti.herbrandQuotient_units_eq_finrank (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)] : TateCohomology.herbrandQuotient (Rep.ofMulDistribMulAction Gal(L/K) Lˣ) = ↑(Module.finrank K L)

The Herbrand quotient of a cyclic local extension. For a cyclic extension L/K of nonarchimedean local fields, the Herbrand quotient of Lˣ is [L : K].