The Herbrand quotient of the idele classes

For a cyclic extension L/K of number fields, the idele class group C_L with its Galois action has Herbrand quotient

h(C_L) = [L : K]

(herbrandQuotient_ideleClassRep_eq_finrank). This is the cohomological content of the first fundamental inequality of global class field theory.

The proof chooses a finite set S of finite places of K outside which L/K is unramified and whose primes upstairs generate the ideal class group of L, so that 0 → U_{L,S} → I_{L,S} → C_L → 0 is short exact and h(C_L) = h(I_{L,S}) / h(U_{L,S}). Both quotients split into an archimedean and a finite-place factor:

h(I_{L,S}) = h(L_∞ˣ) · ∏_{v ∈ S} [L_w : K_v],
h(U_{L,S}) = h((𝓞 L)ˣ) · ∏_{v ∈ S} [L_w : K_v],

and the Herbrand quotient of the units is that of the infinite ideles divided by the degree, h((𝓞 L)ˣ) = h(ℤ[S_∞(L)]) / [L : K] = h(L_∞ˣ) / [L : K]. The local degrees at S and the archimedean factor cancel, leaving [L : K].

Main results

• TauCeti.ClassFieldTheory.herbrandQuotient_ideleClassRep_eq_finrank: h(C_L) = [L : K] for a cyclic extension L/K of number fields.

References

• J. S. Milne, Class Field Theory, v4.03, Chapter VII, §4, Theorem 4.3.

theorem TauCeti.ClassFieldTheory.herbrandQuotient_ideleClassRep_eq_finrank {K : Type} [Field K] [NumberField K] (L : Type) [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [IsCyclic Gal(L/K)] : TateCohomology.herbrandQuotient (ideleClassRep K L) = ↑(Module.finrank K L)

The Herbrand quotient of the idele classes of a cyclic extension L/K of number fields is the degree: h(C_L) = [L : K].