The Herbrand quotient of the global units

Let L/K be a cyclic extension of number fields with Galois group G. The unit group (𝓞 L)ˣ, with its Galois action, is an integral representation of G, and its Herbrand quotient is

h((𝓞 L)ˣ) = h(ℤ[S_∞(L)]) / [L : K] = 2^r / [L : K],

where ℤ[S_∞(L)] is the permutation lattice on the infinite places of L and r is the number of infinite places of K ramified in L (TauCeti.ClassFieldTheory.herbrandQuotient_units_eq_div, TauCeti.ClassFieldTheory.herbrandQuotient_units).

The proof is Dirichlet's unit theorem read equivariantly. The logarithmic embedding has finite kernel, the roots of unity, and its image, the unit lattice, is a full lattice in the real space logSpace L; the Galois group acts on that space by permuting the coordinates of the sum-zero hyperplane of ℝ^{S_∞(L)} (TauCeti.NumberField.Units.logSpaceRep). The sum-zero sublattice of ℤ[S_∞(L)] is a second Galois-stable lattice in the same representation: reading off the coordinates away from the distinguished place w₀ identifies it with ℤ^{S_∞(L) ∖ {w₀}}. By Tate's lattice lemma (TauCeti.TateCohomology.herbrandQuotient_eq_of_isBaseChange) the two lattices have the same Herbrand quotient, and that of the sum-zero lattice is h(ℤ[S_∞(L)]) / |G| (TauCeti.TateCohomology.herbrandQuotient_augmentationSubrepresentation_eq_div).

Together with the finite-place permutation lattices this is the unit part of the Herbrand quotient of the S-units, through which the Herbrand quotient of the idele classes of a cyclic extension, and so the first fundamental inequality, is computed.

Main results

• TauCeti.ClassFieldTheory.herbrandQuotient_units_eq_div_card: h((𝓞 L)ˣ) = h(ℤ[S_∞(L)]) / |Aut(L/K)|, for Aut(L/K) cyclic.
• TauCeti.ClassFieldTheory.herbrandQuotient_units_eq_div: h((𝓞 L)ˣ) = h(ℤ[S_∞(L)]) / [L : K].
• TauCeti.ClassFieldTheory.herbrandQuotient_units: h((𝓞 L)ˣ) = 2^r / [L : K], with r the number of infinite places of K ramified in L.

References

• J. S. Milne, Class Field Theory, Chapter VII, §3 (the Herbrand quotient of the unit group).
• J. Tate, Global class field theory, in Cassels and Fröhlich, Algebraic Number Theory, Chapter VII, §6.

The sum-zero lattice on the infinite places in logSpace L

The unit lattice

The Herbrand quotient

theorem TauCeti.ClassFieldTheory.herbrandQuotient_units_eq_div_card {K L : Type} [Field K] [Field L] [NumberField L] [Algebra K L] [NumberField K] [IsCyclic Gal(L/K)] : TateCohomology.herbrandQuotient (Rep.ofMulDistribMulAction Gal(L/K) (NumberField.RingOfIntegers L)ˣ) = TateCohomology.herbrandQuotient (Rep.ofMulAction ℤ Gal(L/K) (NumberField.InfinitePlace L)) / ↑(Nat.card Gal(L/K))

The Herbrand quotient of the units of an extension of number fields L/K with cyclic automorphism group is the Herbrand quotient of the permutation lattice on the infinite places of L divided by the order of the automorphism group: h((𝓞 L)ˣ) = h(ℤ[S_∞(L)]) / |Aut(L/K)|.

theorem TauCeti.ClassFieldTheory.herbrandQuotient_units_eq_div {K L : Type} [Field K] [Field L] [NumberField L] [Algebra K L] [NumberField K] [IsCyclic Gal(L/K)] [IsGalois K L] : TateCohomology.herbrandQuotient (Rep.ofMulDistribMulAction Gal(L/K) (NumberField.RingOfIntegers L)ˣ) = TateCohomology.herbrandQuotient (Rep.ofMulAction ℤ Gal(L/K) (NumberField.InfinitePlace L)) / ↑(Module.finrank K L)

The Herbrand quotient of the units of a cyclic extension of number fields L/K is the Herbrand quotient of the permutation lattice on the infinite places of L divided by the degree: h((𝓞 L)ˣ) = h(ℤ[S_∞(L)]) / [L : K].

theorem TauCeti.ClassFieldTheory.herbrandQuotient_units {K L : Type} [Field K] [Field L] [NumberField L] [Algebra K L] [NumberField K] [IsCyclic Gal(L/K)] [IsGalois K L] : TateCohomology.herbrandQuotient (Rep.ofMulDistribMulAction Gal(L/K) (NumberField.RingOfIntegers L)ˣ) = 2 ^ {v : NumberField.InfinitePlace K | ¬NumberField.InfinitePlace.IsUnramifiedIn L v}.card / ↑(Module.finrank K L)

The Herbrand quotient of the units of a cyclic extension of number fields L/K is 2^r / [L : K], where r is the number of infinite places of K ramified in L, that is, the real places of K that become complex in L.