Transitivity of the transfer

For finite-index subgroups K ≤ H ≤ G, the transfer in group homology is transitive: transferring from G to H and then from H to K is the transfer from G to K, once K.subgroupOf H is identified with K. This lets a transfer to a small subgroup be computed in stages through an intermediate subgroup; it is what makes Tate restriction below degree -1 functorial along a tower of layers of a class formation.

Main results

• TauCeti.groupHomology.transfer_trans: the transfer is transitive along a tower of subgroups.

References

• K. S. Brown, Cohomology of Groups, Graduate Texts in Mathematics 87, Springer (1982), Chapter III, §9.

theorem TauCeti.groupHomology.transfer_trans {R G : Type u} [CommRing R] [Group G] {K H : Subgroup G} (hKH : K ≤ H) [K.FiniteIndex] (M : Rep.{u, u, u} R G) (n : ℕ) : CategoryTheory.CategoryStruct.comp (transfer M H n) (CategoryTheory.CategoryStruct.comp (transfer (Rep.res H.subtype M) (K.subgroupOf H) n) (groupHomology.map ↑(Subgroup.subgroupOfEquivOfLe hKH) ⋯.toRes n)) = transfer M K n

The transfer is transitive along a tower of finite-index subgroups K ≤ H ≤ G: the transfer Hₙ(G, M) ⟶ Hₙ(H, Res_H M) followed by the transfer to K.subgroupOf H is the transfer Hₙ(G, M) ⟶ Hₙ(K, Res_K M). Here K.subgroupOf H, which is K viewed as a subgroup of H, is identified with K by the change-of-group map along Subgroup.subgroupOfEquivOfLe hKH, under which the two restrictions of M agree (Rep.isIntertwiningMap_res_res). This is the transitivity of the transfer described in Brown, Chapter III, §9.

theorem TauCeti.groupHomology.transfer_trans_assoc {R G : Type u} [CommRing R] [Group G] {K H : Subgroup G} (hKH : K ≤ H) [K.FiniteIndex] (M : Rep.{u, u, u} R G) (n : ℕ) {Z : ModuleCat R} (h : groupHomology (Rep.res K.subtype M) n ⟶ Z) : CategoryTheory.CategoryStruct.comp (transfer M H n) (CategoryTheory.CategoryStruct.comp (transfer (Rep.res H.subtype M) (K.subgroupOf H) n) (CategoryTheory.CategoryStruct.comp (groupHomology.map ↑(Subgroup.subgroupOfEquivOfLe hKH) ⋯.toRes n) h)) = CategoryTheory.CategoryStruct.comp (transfer M K n) h

The transfer is transitive along a tower of finite-index subgroups K ≤ H ≤ G: the transfer Hₙ(G, M) ⟶ Hₙ(H, Res_H M) followed by the transfer to K.subgroupOf H is the transfer Hₙ(G, M) ⟶ Hₙ(K, Res_K M). Here K.subgroupOf H, which is K viewed as a subgroup of H, is identified with K by the change-of-group map along Subgroup.subgroupOfEquivOfLe hKH, under which the two restrictions of M agree (Rep.isIntertwiningMap_res_res). This is the transitivity of the transfer described in Brown, Chapter III, §9.