Archimedean factors in place permutation lattices

For a finite Galois extension of number fields L/K, the Herbrand quotient of the permutation lattice on the infinite places of L is 2^r, where r is the number of infinite places of K ramified in L. Such a place is real and becomes complex; its decomposition group has order two. Every other infinite place contributes one.

Combining this with the finite-place calculation gives the quotient of the permutation lattice on all infinite places and the primes above a finite set S. This is the place lattice used in the logarithmic comparison for the Herbrand quotient of the S-units.

References

• J. S. Milne, Class Field Theory, Chapter VII, §3.
• J. Tate, Global class field theory, in Cassels and Fröhlich, Algebraic Number Theory, Chapter VII.

theorem TauCeti.ClassFieldTheory.herbrandQuotient_ofMulAction_infinitePlace_eq_prod {K L : Type} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] [IsGalois K L] : TateCohomology.herbrandQuotient (Rep.ofMulAction ℤ Gal(L/K) (NumberField.InfinitePlace L)) = ∏ v : NumberField.InfinitePlace K, if NumberField.InfinitePlace.IsUnramifiedIn L v then 1 else 2

The infinite-place permutation lattice has one factor of two for each ramified infinite place of the base field, and a factor of one for each unramified place.

theorem TauCeti.ClassFieldTheory.herbrandQuotient_ofMulAction_infinitePlace {K L : Type} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] [IsGalois K L] : TateCohomology.herbrandQuotient (Rep.ofMulAction ℤ Gal(L/K) (NumberField.InfinitePlace L)) = 2 ^ {v : NumberField.InfinitePlace K | ¬NumberField.InfinitePlace.IsUnramifiedIn L v}.card

The Herbrand quotient of the infinite-place permutation lattice is 2^r, where r is exactly the number of infinite places of K ramified in L.

theorem TauCeti.ClassFieldTheory.herbrandQuotient_ofMulAction_places {K L : Type} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] [IsGalois K L] (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (w : (v : ↥S) → { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // w.asIdeal.LiesOver (↑v).asIdeal }) : TateCohomology.herbrandQuotient (Rep.ofMulAction ℤ Gal(L/K) (NumberField.InfinitePlace L ⊕ ↑(IsDedekindDomain.HeightOneSpectrum.primesAbove (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L) ↑S))) = 2 ^ {v : NumberField.InfinitePlace K | ¬NumberField.InfinitePlace.IsUnramifiedIn L v}.card * ∏ v : ↥S, ↑(Module.finrank (IsDedekindDomain.HeightOneSpectrum.adicCompletion K ↑v) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L ↑(w v)))

The place permutation lattice for a finite set of finite places, together with every infinite place, has quotient 2^r times the product of the finite local degrees. The primes above the finite places may be chosen arbitrarily.