Transfer commutes with the connecting map

Let S be a finite-index subgroup of a group G and X a short exact sequence of G-representations. Restricting X to S keeps it short exact, and the transfer Hₙ(G, M) ⟶ Hₙ(S, Res_S M) commutes with the connecting maps of the two long exact sequences:

Hᵢ(G, X₃) ⟶ Hⱼ(G, X₁) ↓ ↓ Hᵢ(S, X₃) ⟶ Hⱼ(S, X₁)

with j + 1 = i. This is what lets a statement about the transfer be moved up or down in degree by dimension shifting.

Main results

• TauCeti.groupHomology.δ_comp_indIso_inv: the inverse of Shapiro's isomorphism commutes with the connecting maps.
• TauCeti.groupHomology.δ_comp_transfer: the transfer commutes with the connecting maps.

theorem TauCeti.groupHomology.δ_comp_indIso_inv {R G : Type u} [CommRing R] [Group G] (S : Subgroup G) [DecidableEq G] {Y : CategoryTheory.ShortComplex (Rep.{u, u, u} R ↥S)} (hY : Y.ShortExact) (hIY : (Y.map (Rep.indFunctor R S.subtype)).ShortExact) (i j : ℕ) (hij : j + 1 = i) : CategoryTheory.CategoryStruct.comp (groupHomology.δ hY i j hij) (groupHomology.indIso S Y.X₁ j).inv = CategoryTheory.CategoryStruct.comp (groupHomology.indIso S Y.X₃ i).inv (groupHomology.δ hIY i j hij)

Shapiro's isomorphism commutes with the connecting maps. For a short exact sequence Y of S-representations, the inverse of Hₙ(G, Ind_S^G Y) ≅ Hₙ(S, Y) intertwines the connecting map of Y with the connecting map of the induced sequence Ind_S^G Y. Exactness of Ind_S^G Y is a hypothesis because Mathlib provides left exactness of induction only for finite-index S, where hIY is hY.map_of_exact _.

theorem TauCeti.groupHomology.δ_comp_indIso_inv_assoc {R G : Type u} [CommRing R] [Group G] (S : Subgroup G) [DecidableEq G] {Y : CategoryTheory.ShortComplex (Rep.{u, u, u} R ↥S)} (hY : Y.ShortExact) (hIY : (Y.map (Rep.indFunctor R S.subtype)).ShortExact) (i j : ℕ) (hij : j + 1 = i) {Z : ModuleCat R} (h : groupHomology (Rep.ind S.subtype Y.X₁) j ⟶ Z) : CategoryTheory.CategoryStruct.comp (groupHomology.δ hY i j hij) (CategoryTheory.CategoryStruct.comp (groupHomology.indIso S Y.X₁ j).inv h) = CategoryTheory.CategoryStruct.comp (groupHomology.indIso S Y.X₃ i).inv (CategoryTheory.CategoryStruct.comp (groupHomology.δ hIY i j hij) h)

Shapiro's isomorphism commutes with the connecting maps. For a short exact sequence Y of S-representations, the inverse of Hₙ(G, Ind_S^G Y) ≅ Hₙ(S, Y) intertwines the connecting map of Y with the connecting map of the induced sequence Ind_S^G Y. Exactness of Ind_S^G Y is a hypothesis because Mathlib provides left exactness of induction only for finite-index S, where hIY is hY.map_of_exact _.

theorem TauCeti.groupHomology.δ_comp_transfer {R G : Type u} [CommRing R] [Group G] (S : Subgroup G) [S.FiniteIndex] {X : CategoryTheory.ShortComplex (Rep.{u, u, u} R G)} (hX : X.ShortExact) (i j : ℕ) (hij : j + 1 = i) : CategoryTheory.CategoryStruct.comp (groupHomology.δ hX i j hij) (transfer X.X₁ S j) = CategoryTheory.CategoryStruct.comp (transfer X.X₃ S i) (groupHomology.δ ⋯ i j hij)

The transfer commutes with the connecting maps. For a finite-index subgroup S ≤ G and a short exact sequence X of G-representations, the transfer intertwines the connecting map of X with the connecting map of its restriction Res_S X to S.

theorem TauCeti.groupHomology.δ_comp_transfer_assoc {R G : Type u} [CommRing R] [Group G] (S : Subgroup G) [S.FiniteIndex] {X : CategoryTheory.ShortComplex (Rep.{u, u, u} R G)} (hX : X.ShortExact) (i j : ℕ) (hij : j + 1 = i) {Z : ModuleCat R} (h : groupHomology (Rep.res S.subtype X.X₁) j ⟶ Z) : CategoryTheory.CategoryStruct.comp (groupHomology.δ hX i j hij) (CategoryTheory.CategoryStruct.comp (transfer X.X₁ S j) h) = CategoryTheory.CategoryStruct.comp (transfer X.X₃ S i) (CategoryTheory.CategoryStruct.comp (groupHomology.δ ⋯ i j hij) h)

The transfer commutes with the connecting maps. For a finite-index subgroup S ≤ G and a short exact sequence X of G-representations, the transfer intertwines the connecting map of X with the connecting map of its restriction Res_S X to S.