Restriction of the Tate cup product in all integer bidegrees

For a subgroup H of a finite group G, restriction preserves the Tate cup product of classes of arbitrary integer degrees (TauCeti.TateCohomology.cup_res). Thus products can be formed before or after restriction, including products with negative-degree classes in either factor.

The upward and downward dimension-shifting sequences move the second degree away from zero. Restriction commutes with connecting maps, and the restricted induced middle term remains Tate-acyclic even after tensoring with the first factor. The downward argument follows Cup.Associativity.

References

• E. Artin and J. Tate, Class Field Theory, Preliminaries, §2.
• K. S. Brown, Cohomology of Groups, Chapter VI, §5.

@[simp]

theorem TauCeti.TateCohomology.cup_res {k G : Type u} [CommRing k] [Group G] [Fintype G] (M N : Rep.{u, u, u} k G) (H : Subgroup G) {p q r : ℤ} (h : p + q = r) (x : ↑(tateCohomology M p)) (y : ↑(tateCohomology N q)) : (CategoryTheory.ConcreteCategory.hom (res (CategoryTheory.MonoidalCategoryStruct.tensorObj M N) H r)) (((cup M N p q r h) x) y) = ((cup (Rep.res H.subtype M) (Rep.res H.subtype N) p q r h) ((CategoryTheory.ConcreteCategory.hom (res M H p)) x)) ((CategoryTheory.ConcreteCategory.hom (res N H q)) y)

Restriction preserves the Tate cup product in all integer bidegrees. For a subgroup H of a finite group G, restricting x ∪ y gives the cup product of the restrictions of x and y, without any sign or degree restriction. As for res, subgroup cohomology uses Subgroup.fintypeOfFinite; a caller with another Fintype H must select this instance when forming the cup product on the restricted classes.