Archimedean multiplicative-group Herbrand quotients

For every finite extension L of ℝ or ℂ, the Herbrand quotient of Lˣ with its Galois action equals the extension degree. Thus a real place which becomes complex contributes 2, whereas an unchanged real place or a complex place contributes 1. These are the archimedean factors in the Herbrand quotient calculation for S-ideles.

The real calculation uses Mathlib's Real.nonempty_algEquiv_or: an algebraic extension of ℝ is isomorphic to ℝ or ℂ. For ℂ/ℝ the norm group consists of the positive units, whose subgroup has index two (Units.index_posSubgroup). Hilbert 90 and cyclic two-periodicity identify each Herbrand quotient with this norm index.

References

• J. S. Milne, Class Field Theory, Chapter VII, Proposition 2.7, the local factors of the S-idele Herbrand quotient: https://www.jmilne.org/math/CourseNotes/CFT.pdf

@[simp]

theorem TauCeti.herbrandQuotient_units_eq_finrank_real (L : Type) [Field L] [Algebra ℝ L] [FiniteDimensional ℝ L] : TateCohomology.herbrandQuotient (Rep.ofMulDistribMulAction Gal(L/ℝ) Lˣ) = ↑(Module.finrank ℝ L)

The multiplicative group of any finite real extension has Herbrand quotient equal to its degree, including the contribution 2 when a real place becomes complex.