Tate restriction below degree -1 along towers and isomorphisms

Below degree -1, restriction in Tate cohomology is the transfer in group homology, read through Mathlib's comparison TateCohomology.isoGroupHomology (TauCeti.TateCohomology.negSuccRes). This file transports the transitivity of the transfer and its compatibility with group isomorphisms (TauCeti.groupHomology.transfer_trans, TauCeti.groupHomology.map_comp_transfer_congrOfMapEq) to Tate cohomology.

Main results

• TauCeti.TateCohomology.negSuccRes_trans: restriction is transitive along a tower of subgroups.
• TauCeti.TateCohomology.map_comp_negSuccRes: restriction commutes with the Tate map of a compatible pair along a group isomorphism.
• TauCeti.TateCohomology.negSuccRes_natural: in particular, restriction is natural in the coefficient representation.

theorem TauCeti.TateCohomology.negSuccRes_trans {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep.{u, u, u} R G) {K H : Subgroup G} (hKH : K ≤ H) (n : ℕ) [NeZero n] : CategoryTheory.CategoryStruct.comp (negSuccRes M H n) (CategoryTheory.CategoryStruct.comp (negSuccRes (Rep.res H.subtype M) (K.subgroupOf H) n) (map ⋯ (Int.negSucc n))) = negSuccRes M K n

Tate restriction below degree -1 is transitive along a tower of subgroups K ≤ H ≤ G: restricting from G to H and then from H to K is restriction from G to K, once K.subgroupOf H is identified with K by the Tate map along Subgroup.subgroupOfEquivOfLe hKH.

theorem TauCeti.TateCohomology.negSuccRes_trans_assoc {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep.{u, u, u} R G) {K H : Subgroup G} (hKH : K ≤ H) (n : ℕ) [NeZero n] {Z : ModuleCat R} (h : tateCohomology (Rep.res K.subtype M) (Int.negSucc n) ⟶ Z) : CategoryTheory.CategoryStruct.comp (negSuccRes M H n) (CategoryTheory.CategoryStruct.comp (negSuccRes (Rep.res H.subtype M) (K.subgroupOf H) n) (CategoryTheory.CategoryStruct.comp (map ⋯ (Int.negSucc n)) h)) = CategoryTheory.CategoryStruct.comp (negSuccRes M K n) h

Tate restriction below degree -1 is transitive along a tower of subgroups K ≤ H ≤ G: restricting from G to H and then from H to K is restriction from G to K, once K.subgroupOf H is identified with K by the Tate map along Subgroup.subgroupOfEquivOfLe hKH.

theorem TauCeti.TateCohomology.map_comp_negSuccRes {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep.{u, u, u} R G) {G' : Type u} [Group G'] [Fintype G'] (e : G ≃* G') {N : Rep.{u, u, u} R G'} {φ : ↑M →ₗ[R] ↑N} (hφ : M.ρ.IsIntertwiningMap (MonoidHom.comp N.ρ ↑e) φ) {S : Subgroup G} {S' : Subgroup G'} (he : Subgroup.map (↑e) S = S') (n : ℕ) [NeZero n] : CategoryTheory.CategoryStruct.comp (map hφ (Int.negSucc n)) (negSuccRes N S' n) = CategoryTheory.CategoryStruct.comp (negSuccRes M S n) (map ⋯ (Int.negSucc n))

Tate restriction below degree -1 is compatible with a group isomorphism e : G ≃* G' carrying S onto S': for a compatible pair (e, φ), restricting to S' after transporting along (e, φ) is transporting along the restricted pair after restricting to S. This is TauCeti.groupHomology.map_comp_transfer_congrOfMapEq in Tate cohomology.

theorem TauCeti.TateCohomology.map_comp_negSuccRes_assoc {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep.{u, u, u} R G) {G' : Type u} [Group G'] [Fintype G'] (e : G ≃* G') {N : Rep.{u, u, u} R G'} {φ : ↑M →ₗ[R] ↑N} (hφ : M.ρ.IsIntertwiningMap (MonoidHom.comp N.ρ ↑e) φ) {S : Subgroup G} {S' : Subgroup G'} (he : Subgroup.map (↑e) S = S') (n : ℕ) [NeZero n] {Z : ModuleCat R} (h : tateCohomology (Rep.res S'.subtype N) (Int.negSucc n) ⟶ Z) : CategoryTheory.CategoryStruct.comp (map hφ (Int.negSucc n)) (CategoryTheory.CategoryStruct.comp (negSuccRes N S' n) h) = CategoryTheory.CategoryStruct.comp (negSuccRes M S n) (CategoryTheory.CategoryStruct.comp (map ⋯ (Int.negSucc n)) h)

Tate restriction below degree -1 is compatible with a group isomorphism e : G ≃* G' carrying S onto S': for a compatible pair (e, φ), restricting to S' after transporting along (e, φ) is transporting along the restricted pair after restricting to S. This is TauCeti.groupHomology.map_comp_transfer_congrOfMapEq in Tate cohomology.

theorem TauCeti.TateCohomology.negSuccRes_natural {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep.{u, u, u} R G) (H : Subgroup G) {N : Rep.{u, u, u} R G} (f : M ⟶ N) (n : ℕ) [NeZero n] : CategoryTheory.CategoryStruct.comp ((tateCohomologyFunctor (Int.negSucc n)).map f) (negSuccRes N H n) = CategoryTheory.CategoryStruct.comp (negSuccRes M H n) ((tateCohomologyFunctor (Int.negSucc n)).map ((Rep.resFunctor H.subtype).map f))

Tate restriction below degree -1 is natural in the coefficient representation. This is map_comp_negSuccRes along the identity of G.

theorem TauCeti.TateCohomology.negSuccRes_natural_assoc {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep.{u, u, u} R G) (H : Subgroup G) {N : Rep.{u, u, u} R G} (f : M ⟶ N) (n : ℕ) [NeZero n] {Z : ModuleCat R} (h : tateCohomology (Rep.res H.subtype N) (Int.negSucc n) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((tateCohomologyFunctor (Int.negSucc n)).map f) (CategoryTheory.CategoryStruct.comp (negSuccRes N H n) h) = CategoryTheory.CategoryStruct.comp (negSuccRes M H n) (CategoryTheory.CategoryStruct.comp ((tateCohomologyFunctor (Int.negSucc n)).map (Rep.resMap H.subtype f)) h)

Tate restriction below degree -1 is natural in the coefficient representation. This is map_comp_negSuccRes along the identity of G.