Restriction of the Tate cup product

Restriction preserves the Tate cup product with a degree-zero right factor in every integer degree (cup_res_zero_right). An invariant vector represents the right factor, so coefficient naturality gives this base case of the all-degree restriction law used in Tate's theorem. In bidegree (0, 0), restriction carries an invariant pure tensor to the tensor of its restrictions.

The product and restriction are those of the existing Tate cohomology API. See Artin and Tate, Class Field Theory, Preliminaries, §2, and Brown, Cohomology of Groups, Chapter VI, §5.

@[simp]

theorem TauCeti.TateCohomology.cupH0_H0Res {k G : Type u} [CommRing k] [Group G] [Fintype G] (M N : Rep.{u, u, u} k G) (H : Subgroup G) (x : ↑(tateCohomology M 0)) (y : ↑(tateCohomology N 0)) : (CategoryTheory.ConcreteCategory.hom (H0Res (CategoryTheory.MonoidalCategoryStruct.tensorObj M N) H)) (((cupH0 M N 0) x) y) = ((cupH0 (Rep.res H.subtype M) (Rep.res H.subtype N) 0) ((CategoryTheory.ConcreteCategory.hom (H0Res M H)) x)) ((CategoryTheory.ConcreteCategory.hom (H0Res N H)) y)

Restriction commutes with the degree-zero cup product in its cupH0 normal form. This is the form used by simp after reducing cup and res in degree zero.

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

Restriction preserves the Tate cup product with a degree-zero right factor, in every integer degree.