Coefficient naturality of Tate corestriction

Corestriction from a subgroup of a finite group is natural in the coefficient representation in every integer degree. This allows a coefficient pairing, such as tensoring with an invariant vector, to pass through corestriction.

In nonnegative degrees this is the naturality of the relative norm and ordinary corestriction; in negative degrees it follows from the canonical injection into group homology.

References

• K. S. Brown, Cohomology of Groups, Chapter III, §9 and Chapter VI, §5.

theorem TauCeti.TateCohomology.cor_natural {k G : Type u} [CommRing k] [Group G] [Fintype G] {M N : Rep.{u, u, u} k G} (f : M ⟶ N) (H : Subgroup G) (r : ℤ) : CategoryTheory.CategoryStruct.comp ((tateCohomologyFunctor r).map (Rep.resMap H.subtype f)) (cor N H r) = CategoryTheory.CategoryStruct.comp (cor M H r) ((tateCohomologyFunctor r).map f)

Tate corestriction is natural in the coefficient representation, in every integer degree. The subgroup carrier uses the canonical Subgroup.fintypeOfFinite instance, as in cor.

theorem TauCeti.TateCohomology.cor_natural_assoc {k G : Type u} [CommRing k] [Group G] [Fintype G] {M N : Rep.{u, u, u} k G} (f : M ⟶ N) (H : Subgroup G) (r : ℤ) {Z : ModuleCat k} (h : tateCohomology N r ⟶ Z) : CategoryTheory.CategoryStruct.comp ((tateCohomologyFunctor r).map (Rep.resMap H.subtype f)) (CategoryTheory.CategoryStruct.comp (cor N H r) h) = CategoryTheory.CategoryStruct.comp (cor M H r) (CategoryTheory.CategoryStruct.comp ((tateCohomologyFunctor r).map f) h)

Tate corestriction is natural in the coefficient representation, in every integer degree. The subgroup carrier uses the canonical Subgroup.fintypeOfFinite instance, as in cor.