The projection formula for Tate cup products

For a subgroup H of a finite group G, a class x of H and a class y of G,

cor (x ∪ res y) = cor x ∪ y

in all integer bidegrees. The coefficient modules are restrictions of representations of G. There is no normality assumption on H, and the coefficient modules need not be flat.

The degree-zero right factor is represented by an invariant vector, so the formula there is coefficient naturality of corestriction. Dimension shifting in the second factor extends it across all degrees, using compatibility of restriction and corestriction with connecting maps. This is the cup-product compatibility used to transport Tate isomorphisms and reciprocity along norm maps.

Main results

• TauCeti.TateCohomology.cup_projection: the projection formula with corestriction in the first factor.

References

• K. S. Brown, Cohomology of Groups, Chapter VI, §5.
• E. Artin and J. Tate, Class Field Theory, Chapter IV, §6 and Chapter XIV, §4.

@[simp]

theorem TauCeti.TateCohomology.cup_projection {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 (Rep.res H.subtype M) p)) (y : ↑(tateCohomology N q)) : (CategoryTheory.ConcreteCategory.hom (cor (CategoryTheory.MonoidalCategoryStruct.tensorObj M N) H r)) (((cup (Rep.res H.subtype M) (Rep.res H.subtype N) p q r h) x) ((CategoryTheory.ConcreteCategory.hom (res N H q)) y)) = ((cup M N p q r h) ((CategoryTheory.ConcreteCategory.hom (cor M H p)) x)) y

The projection formula for Tate cup products in all integer bidegrees. Corestricting x ∪ res y is cor x ∪ y, for arbitrary representations of a finite group and any subgroup. As in res and cor, subgroup cohomology uses Subgroup.fintypeOfFinite; callers with another Fintype H should select this instance.