Finiteness of low-degree Tate cohomology for integral representations

For a finite group acting on a finitely generated abelian group, Tate cohomology in degrees zero and minus one is finite. The low-degree descriptions give quotients of finitely generated subgroups; the group order kills both quotients. These finiteness results allow Herbrand quotients of arithmetic lattices, in particular the S-units, to be used without separate finiteness assumptions.

theorem TauCeti.TateCohomology.finite_tateCohomology_zero_of_moduleFinite {G : Type} [Group G] [Fintype G] (M : Rep.{0, 0, 0} ℤ G) [Module.Finite ℤ ↑M] : Finite ↑(tateCohomology M 0)

Degree-zero Tate cohomology of a finitely generated integral representation of a finite group is finite.

theorem TauCeti.TateCohomology.finite_tateCohomology_negOne_of_moduleFinite {G : Type} [Group G] [Fintype G] (M : Rep.{0, 0, 0} ℤ G) [Module.Finite ℤ ↑M] : Finite ↑(tateCohomology M (-1))

Degree-minus-one Tate cohomology of a finitely generated integral representation of a finite group is finite.