The Herbrand quotient of the infinite ideles

Let L/K be a cyclic extension of number fields. This file computes the Herbrand quotient of the infinite ideles L_∞ˣ = ∏_w L_wˣ of L, as a representation of Gal(L/K):

h(L_∞ˣ) = ∏_v [L_w : K_v],

the product running over the infinite places v of K, with w any place of L above v (herbrandQuotient_infiniteIdelesRep). A factor is 2 when v is real and the places above it are complex, and 1 otherwise, so this is the Herbrand quotient of the permutation lattice ℤ[places of L at ∞] (herbrandQuotient_infiniteIdelesRep_eq_herbrandQuotient_ofMulAction).

This is the archimedean factor of the Herbrand quotient of the S-ideles I_{L,S} = L_∞ˣ × ∏_{w ∈ S} L_wˣ × ∏_{w ∉ S} 𝒪_wˣ, which enters the computation h(C_L) = h(I_{L,S}) / h(U_{L,S}) = [L : K] behind the first fundamental inequality. The comparison with the permutation lattice matches the logarithmic computation of the S-units, which embeds them in the real representation spanned by the same lattice.

The proof decomposes the infinite ideles as the product over v of the semi-local units (K_v ⊗[K] L)ˣ (TauCeti.GlobalNumberFields.infiniteIdelesPiIso), takes the Herbrand quotient factor by factor (TauCeti.TateCohomology.herbrandQuotient_pi), and uses the archimedean local computation TauCeti.ClassFieldTheory.herbrandQuotient_infiniteSemilocalUnitsRep.

Main results

• TauCeti.ClassFieldTheory.herbrandQuotient_infiniteIdelesRep: h(L_∞ˣ) = ∏_v [L_w : K_v].
• TauCeti.ClassFieldTheory.herbrandQuotient_infiniteIdelesRep_eq_herbrandQuotient_ofMulAction: h(L_∞ˣ) is the Herbrand quotient of the permutation lattice on the infinite places of L.
• TauCeti.ClassFieldTheory.finite_tateCohomology_infiniteIdelesRep: the Tate cohomology of the infinite ideles is finite in degrees 0 and -1.

References

• J. S. Milne, Class Field Theory, Chapter VII, §2 and the proof of Theorem 4.3.
• J. Neukirch, Algebraic Number Theory, Chapter VI, §2.

theorem TauCeti.ClassFieldTheory.herbrandQuotient_infiniteIdelesRep {K L : Type} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [IsCyclic Gal(L/K)] (w : (v : NumberField.InfinitePlace K) → { w : NumberField.InfinitePlace L // w.LiesOver v }) : TateCohomology.herbrandQuotient (GlobalNumberFields.infiniteIdelesRep K L) = ∏ v : NumberField.InfinitePlace K, ↑(Module.finrank v.Completion (↑(w v)).Completion)

The Herbrand quotient of the infinite ideles. For a cyclic extension L/K of number fields, the infinite ideles L_∞ˣ have Herbrand quotient ∏_v [L_w : K_v] as a representation of Gal(L/K), the product running over the infinite places v of K. The places w above each v may be chosen arbitrarily.

theorem TauCeti.ClassFieldTheory.herbrandQuotient_infiniteIdelesRep_eq_herbrandQuotient_ofMulAction {K L : Type} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [IsCyclic Gal(L/K)] : TateCohomology.herbrandQuotient (GlobalNumberFields.infiniteIdelesRep K L) = TateCohomology.herbrandQuotient (Rep.ofMulAction ℤ Gal(L/K) (NumberField.InfinitePlace L))

The infinite ideles and the archimedean place lattice have the same Herbrand quotient: for a cyclic extension L/K of number fields, h(L_∞ˣ) is the Herbrand quotient of the permutation lattice on the infinite places of L, namely 2^r with r the number of infinite places of K ramified in L (herbrandQuotient_ofMulAction_infinitePlace).

theorem TauCeti.ClassFieldTheory.herbrandQuotient_infiniteIdelesRep_ne_zero {K L : Type} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [IsCyclic Gal(L/K)] : TateCohomology.herbrandQuotient (GlobalNumberFields.infiniteIdelesRep K L) ≠ 0

For a cyclic extension L/K of number fields, the Herbrand quotient of the infinite ideles L_∞ˣ is nonzero: it is the power of 2 given by herbrandQuotient_infiniteIdelesRep_eq_herbrandQuotient_ofMulAction.

theorem TauCeti.ClassFieldTheory.finite_tateCohomology_infiniteIdelesRep {K L : Type} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [IsCyclic Gal(L/K)] : Finite ↑(tateCohomology (GlobalNumberFields.infiniteIdelesRep K L) 0) ∧ Finite ↑(tateCohomology (GlobalNumberFields.infiniteIdelesRep K L) (-1))

The Tate cohomology of the infinite ideles is finite in degrees 0 and -1, for a cyclic extension L/K of number fields.