Herbrand quotient of the sum-zero permutation lattice

For a finite cyclic group G acting on a nonempty finite set X, the integral sum-zero permutation lattice has Herbrand quotient ∏ ω, |G_ω| / |G|. The denominator comes from the trivial quotient in the augmentation sequence 0 → ker(sum) → ℤ[X] → ℤ → 0.

This computes the lattice used in the logarithmic description of S-units: the permutation basis indexes the places above S, the stabilizers are decomposition groups, and the sum-zero hyperplane encodes the product formula. Comparing an S-unit lattice with this lattice still requires an equivariant logarithmic comparison.

The calculation uses herbrandQuotient_ofMulAction, herbrandQuotient_eq_mul_of_shortExact and herbrandQuotient_trivial_int_eq_card. Finiteness in degree -1 follows from the augmentation long exact sequence and the identification HNegTwoAddEquivAbelianization of degree -2 for the trivial integral module.

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.

instance TauCeti.TateCohomology.finite_tateCohomology_negOne_augmentationSubrepresentation {G X : Type} [Group G] [Fintype G] [MulAction G X] : Finite ↑(tateCohomology (Rep.of (augmentationSubrepresentation ℤ G X).toRepresentation) (-1))

Degree-minus-one Tate cohomology of the integral sum-zero permutation module is finite. No nonemptiness or finiteness of the permutation set or cyclicity of the group is required.

theorem TauCeti.TateCohomology.herbrandQuotient_augmentationSubrepresentation_eq_div {G X : Type} [Group G] [Fintype G] [MulAction G X] [Nonempty X] [IsCyclic G] : herbrandQuotient (Rep.of (augmentationSubrepresentation ℤ G X).toRepresentation) = herbrandQuotient (Rep.ofMulAction ℤ G X) / ↑(Nat.card G)

For a finite cyclic group acting on a nonempty set, the integral sum-zero permutation module's Herbrand quotient is that of the integral permutation module divided by the order of the group.

theorem TauCeti.TateCohomology.herbrandQuotient_augmentationSubrepresentation {G X : Type} [Group G] [Fintype G] [MulAction G X] [Nonempty X] [IsCyclic G] [Fintype (MulAction.orbitRel.Quotient G X)] : herbrandQuotient (Rep.of (augmentationSubrepresentation ℤ G X).toRepresentation) = (∏ ω : MulAction.orbitRel.Quotient G X, ↑(Nat.card ↥(MulAction.stabilizer G (Quotient.out ω)))) / ↑(Nat.card G)

The sum-zero permutation lattice has Herbrand quotient the product of orbit stabilizer orders divided by the group order. The set must be nonempty for augmentation onto ℤ.