Finite-place permutation lattices

For a finite Galois extension of number fields L/K and a finite set S of finite places of K, the permutation lattice on the primes of L above S has Herbrand quotient ∏ v ∈ S, [L_w : K_v]. Each factor is independent of the choice of a prime w above v. Cyclicity is not needed. This supplies the finite-place factors in the permutation lattice used to compare the logarithmic S-unit lattice with the augmentation hyperplane. For cyclic L/K and nonempty S, the sum-zero lattice on these finite places has quotient ∏ v ∈ S, [L_w : K_v] / [L : K]. Archimedean factors and the logarithmic comparison with S-units are separate from this finite-place calculation.

The calculation combines TauCeti.TateCohomology.herbrandQuotient_ofMulAction_sigma_of_isPretransitive with IsDedekindDomain.HeightOneSpectrum.card_stabilizer_eq_finrank_adicCompletion.

Main results

• TauCeti.ClassFieldTheory.herbrandQuotient_ofMulAction_primesAbove: the local-degree product on the canonical HeightOneSpectrum.primesAbove carrier.
• TauCeti.ClassFieldTheory.herbrandQuotient_augmentationSubrepresentation_primesAbove: the sum-zero lattice's quotient, with denominator the global degree.

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_primesAbove {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) ↑(IsDedekindDomain.HeightOneSpectrum.primesAbove (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L) ↑S)) = ∏ v : ↥S, ↑(Module.finrank (IsDedekindDomain.HeightOneSpectrum.adicCompletion K ↑v) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L ↑(w v)))

The permutation lattice on the canonical carrier of primes above a finite set of finite places has Herbrand quotient the product of their local degrees. The prime above each place may be chosen arbitrarily.

theorem TauCeti.ClassFieldTheory.herbrandQuotient_augmentationSubrepresentation_primesAbove {K L : Type} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] [IsGalois K L] [IsCyclic Gal(L/K)] (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (hS : S.Nonempty) (w : (v : ↥S) → { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // w.asIdeal.LiesOver (↑v).asIdeal }) : TateCohomology.herbrandQuotient (Rep.of (augmentationSubrepresentation ℤ Gal(L/K) ↑(IsDedekindDomain.HeightOneSpectrum.primesAbove (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L) ↑S)).toRepresentation) = (∏ v : ↥S, ↑(Module.finrank (IsDedekindDomain.HeightOneSpectrum.adicCompletion K ↑v) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L ↑(w v)))) / ↑(Module.finrank K L)

For a cyclic extension and a nonempty finite set of finite places, the sum-zero lattice on the primes above those places has Herbrand quotient the product of local degrees divided by the global degree. This is the finite-place augmentation calculation, not yet the Herbrand quotient of the S-units.