The Herbrand quotient as a norm index

For a finite cyclic Galois extension L/K, Hilbert 90 and two-periodicity identify the Herbrand quotient of Lˣ with the index of N(Lˣ) in Kˣ. This is a numerical consequence of TauCeti.cyclicNormQuotientEquiv and TauCeti.natCard_H2_units_eq_herbrandQuotient; it does not use reciprocity or assume that the index equals the extension degree. For finite extensions of an algebraically closed field the quotient is one, since such an extension is isomorphic to the identity extension.

References

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

@[simp]

theorem TauCeti.herbrandQuotient_units_eq_index_normGroup {K L : Type} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] [IsCyclic Gal(L/K)] : TateCohomology.herbrandQuotient (Rep.ofMulDistribMulAction Gal(L/K) Lˣ) = ↑(normGroup K L).index

The Herbrand quotient of the multiplicative group of a finite cyclic Galois extension is the index of its norm group in the ground field's units.

@[simp]

theorem TauCeti.herbrandQuotient_units_eq_one_of_isAlgClosed (K L : Type) [Field K] [Field L] [Algebra K L] [IsAlgClosed K] [FiniteDimensional K L] : TateCohomology.herbrandQuotient (Rep.ofMulDistribMulAction Gal(L/K) Lˣ) = 1

A finite extension of an algebraically closed field has multiplicative-group Herbrand quotient one. In particular, a complex place contributes the factor one.