The Tate cup product under change of group in positive degrees

Let φ : G →* Q be a homomorphism of finite groups. For classes x and y of positive degrees in the Tate cohomology of Q-representations M and N, and morphisms f : Res_φ M ⟶ M' and g : Res_φ N ⟶ N', change of group (TauCeti.TateCohomology.posMap) carries the cup product x ∪ y along f ⊗ g to the cup product of the changed classes (TauCeti.TateCohomology.cup_posMap). Restriction to a subgroup and inflation from a quotient are both instances. For inflation this is the compatibility that, together with the scaling of the fundamental class, gives the inflation formula for the Tate isomorphism of a class formation. Both degrees must be positive, since change of group does not exist in Tate degree zero.

Main statements

• TauCeti.TateCohomology.cup_posMap: change of group preserves the cup product of two classes of positive degree.

References

• K. S. Brown, Cohomology of Groups, Chapter V, §3 and Chapter VI, §5.
• J. W. S. Cassels and A. Fröhlich (eds.), Algebraic Number Theory, Chapter IV (Atiyah–Wall), §7.

theorem TauCeti.TateCohomology.cup_posMap {k G Q : Type u} [CommRing k] [Group G] [Group Q] [Fintype G] [Fintype Q] (φ : G →* Q) (M N : Rep.{u, u, u} k Q) {M' N' : Rep.{u, u, u} k G} (f : Rep.res φ M ⟶ M') (g : Rep.res φ N ⟶ N') (p q r : ℕ) [NeZero p] [NeZero q] [NeZero r] (h : ↑p + ↑q = ↑r) (x : ↑(tateCohomology M ↑p)) (y : ↑(tateCohomology N ↑q)) : (CategoryTheory.ConcreteCategory.hom (posMap φ (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) r)) (((cup M N (↑p) (↑q) (↑r) h) x) y) = ((cup M' N' (↑p) (↑q) (↑r) h) ((CategoryTheory.ConcreteCategory.hom (posMap φ f p)) x)) ((CategoryTheory.ConcreteCategory.hom (posMap φ g q)) y)

Change of group preserves the Tate cup product in positive degrees. For φ : G →* Q and morphisms f : Res_φ M ⟶ M', g : Res_φ N ⟶ N', changing the group of x ∪ y along f ⊗ g gives the cup product of the changed classes, for x and y of positive degrees.