Restriction commutes with the connecting maps of Tate cohomology

Let H be a subgroup of a finite group G and S a short exact sequence of G-representations. Restricting S to H keeps it short exact, and in every degree Tate restriction commutes with the connecting maps of the two long exact sequences:

H_Tateʳ(G, X₃) ⟶ H_Tateʳ⁺¹(G, X₁) ↓ ↓ H_Tateʳ(H, X₃) ⟶ H_Tateʳ⁺¹(H, X₁)

for every r : ℤ (TauCeti.TateCohomology.δ_comp_res). This is what lets a statement about restriction be moved across degrees by dimension shifting, as in the proof that restriction is compatible with the Tate cup product. The boundary case r = -1 is supplied by TauCeti.TateCohomology.δ_comp_res_neg_one.

In nonnegative degrees the Tate complex is the complex of inhomogeneous cochains. Restriction of cochains, extended by zero to negative degrees, is not a map of Tate complexes: the norm map from the negative half of the Tate complex over G lands in G-invariant cochains of degree zero, which restriction does not annihilate. It is, however, a map to the Tate complex over H from the complex of inhomogeneous cochains over G extended by zero to negative degrees, and that complex also maps to the Tate complex over G by the identity in nonnegative degrees. Both maps are natural, so the connecting maps commute with them. In positive degrees the second map induces an isomorphism on cohomology, and the first one induces its composite with Tate restriction. In degree zero the second map induces the epimorphism from the invariants onto H_Tate⁰, and the first one again induces its composite with Tate restriction, which is induced by the inclusion Mᴳ ⊆ Mᴴ.

Below degree -1 the comparison is made in group homology instead. The injective comparison TauCeti.TateCohomology.toGroupHomology of H_Tate^{-(n+1)} with Hₙ commutes with the connecting maps, and through it Tate restriction is the transfer of group homology (TauCeti.TateCohomology.res_comp_toGroupHomology), which commutes with the connecting maps by TauCeti.groupHomology.δ_comp_transfer.

Main results

• TauCeti.TateCohomology.res_comp_toGroupHomology: in negative degrees, Tate restriction is the transfer of group homology through toGroupHomology.
• TauCeti.TateCohomology.δ_comp_res: Tate restriction commutes with the connecting maps in every degree.

References

• K. S. Brown, Cohomology of Groups, Chapter III, §9 and Chapter VI, §5.
• J. S. Milne, Class Field Theory, v4.03, Chapter II, §1.

theorem TauCeti.TateCohomology.res_comp_toGroupHomology {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep.{u, u, u} R G) (H : Subgroup G) (n : ℕ) : CategoryTheory.CategoryStruct.comp (res M H (Int.negSucc n)) (toGroupHomology (Rep.res H.subtype M) n) = CategoryTheory.CategoryStruct.comp (toGroupHomology M n) (groupHomology.transfer M H n)

In negative degrees Tate restriction is the transfer of group homology: through the comparison toGroupHomology of H_Tate^{-(n+1)} with Hₙ, restriction to H is the transfer.

theorem TauCeti.TateCohomology.res_comp_toGroupHomology_assoc {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep.{u, u, u} R G) (H : Subgroup G) (n : ℕ) {Z : ModuleCat R} (h : groupHomology (Rep.res H.subtype M) n ⟶ Z) : CategoryTheory.CategoryStruct.comp (res M H (Int.negSucc n)) (CategoryTheory.CategoryStruct.comp (toGroupHomology (Rep.res H.subtype M) n) h) = CategoryTheory.CategoryStruct.comp (toGroupHomology M n) (CategoryTheory.CategoryStruct.comp (groupHomology.transfer M H n) h)

In negative degrees Tate restriction is the transfer of group homology: through the comparison toGroupHomology of H_Tate^{-(n+1)} with Hₙ, restriction to H is the transfer.

@[simp]

theorem TauCeti.TateCohomology.δ_comp_res {R G : Type u} [CommRing R] [Group G] [Fintype G] {S : CategoryTheory.ShortComplex (Rep.{u, u, u} R G)} (hS : S.ShortExact) (H : Subgroup G) (r : ℤ) : CategoryTheory.CategoryStruct.comp (TateCohomology.δ hS r) (res S.X₁ H (r + 1)) = CategoryTheory.CategoryStruct.comp (res S.X₃ H r) (TateCohomology.δ ⋯ r)

Tate restriction commutes with the connecting maps. For a short exact sequence S of G-representations and a subgroup H, restriction to H intertwines the connecting map H_Tateʳ(G, X₃) ⟶ H_Tateʳ⁺¹(G, X₁) of S with the connecting map of its restriction to H, in every degree r.

@[simp]

theorem TauCeti.TateCohomology.δ_comp_res_assoc {R G : Type u} [CommRing R] [Group G] [Fintype G] {S : CategoryTheory.ShortComplex (Rep.{u, u, u} R G)} (hS : S.ShortExact) (H : Subgroup G) (r : ℤ) {Z : ModuleCat R} (h : tateCohomology (Rep.res H.subtype S.X₁) (r + 1) ⟶ Z) : CategoryTheory.CategoryStruct.comp (TateCohomology.δ hS r) (CategoryTheory.CategoryStruct.comp (res S.X₁ H (r + 1)) h) = CategoryTheory.CategoryStruct.comp (res S.X₃ H r) (CategoryTheory.CategoryStruct.comp (TateCohomology.δ ⋯ r) h)

Tate restriction commutes with the connecting maps. For a short exact sequence S of G-representations and a subgroup H, restriction to H intertwines the connecting map H_Tateʳ(G, X₃) ⟶ H_Tateʳ⁺¹(G, X₁) of S with the connecting map of its restriction to H, in every degree r.