The transfer along group isomorphisms

For a finite-index subgroup S of a group G and a group isomorphism e : G ≃* G' carrying S onto S', the transfer Hₙ(G, M) ⟶ Hₙ(S, Res_S M) is compatible with e.

This moves transfer computations between isomorphic groups and their corresponding subgroups. For example, the Galois group of a layer of a class formation is identified with its image in a larger Galois group. Tate restriction below degree -1 is the transfer read along that identification, so its functoriality along a tower of layers needs this compatibility.

Main results

• TauCeti.groupHomology.map_comp_transfer_congrOfMapEq: the transfer is compatible with a group isomorphism and a compatible map of coefficients.

theorem TauCeti.groupHomology.map_comp_transfer_congrOfMapEq {R G G' : Type u} [CommRing R] [Group G] [Group G'] (e : G ≃* G') {S : Subgroup G} {S' : Subgroup G'} (he : Subgroup.map (↑e) S = S') [S.FiniteIndex] {M : Rep.{u, u, u} R G} {N : Rep.{u, u, u} R G'} (φ : M ⟶ Rep.res (↑e) N) (n : ℕ) : CategoryTheory.CategoryStruct.comp (groupHomology.map (↑e) φ n) (transfer N S' n) = CategoryTheory.CategoryStruct.comp (transfer M S n) (groupHomology.map (↑(Subgroup.congrOfMapEq e he)) (CategoryTheory.CategoryStruct.comp ((Rep.resFunctor S.subtype).map φ) ⋯.toRes) n)

The transfer is compatible with a group isomorphism. Let e : G ≃* G' carry S onto S' and let φ : M ⟶ Res_e N. Then the transfers Hₙ(G, M) ⟶ Hₙ(S, Res_S M) and Hₙ(G', N) ⟶ Hₙ(S', Res_S' N) commute with the maps induced by (e, φ) over G and by its restriction (e|_S, Res_S φ) over S. This extends TauCeti.groupHomology.map_comp_transfer, the case where e is the identity, to a change of group.

theorem TauCeti.groupHomology.map_comp_transfer_congrOfMapEq_assoc {R G G' : Type u} [CommRing R] [Group G] [Group G'] (e : G ≃* G') {S : Subgroup G} {S' : Subgroup G'} (he : Subgroup.map (↑e) S = S') [S.FiniteIndex] {M : Rep.{u, u, u} R G} {N : Rep.{u, u, u} R G'} (φ : M ⟶ Rep.res (↑e) N) (n : ℕ) {Z : ModuleCat R} (h : groupHomology (Rep.res S'.subtype N) n ⟶ Z) : CategoryTheory.CategoryStruct.comp (groupHomology.map (↑e) φ n) (CategoryTheory.CategoryStruct.comp (transfer N S' n) h) = CategoryTheory.CategoryStruct.comp (transfer M S n) (CategoryTheory.CategoryStruct.comp (groupHomology.map (↑(Subgroup.congrOfMapEq e he)) (CategoryTheory.CategoryStruct.comp (Rep.resMap S.subtype φ) ⋯.toRes) n) h)

The transfer is compatible with a group isomorphism. Let e : G ≃* G' carry S onto S' and let φ : M ⟶ Res_e N. Then the transfers Hₙ(G, M) ⟶ Hₙ(S, Res_S M) and Hₙ(G', N) ⟶ Hₙ(S', Res_S' N) commute with the maps induced by (e, φ) over G and by its restriction (e|_S, Res_S φ) over S. This extends TauCeti.groupHomology.map_comp_transfer, the case where e is the identity, to a change of group.

theorem TauCeti.groupHomology.map_comp_transfer_congrOfMapEq_apply {R G G' : Type u} [CommRing R] [Group G] [Group G'] (e : G ≃* G') {S : Subgroup G} {S' : Subgroup G'} (he : Subgroup.map (↑e) S = S') [S.FiniteIndex] {M : Rep.{u, u, u} R G} {N : Rep.{u, u, u} R G'} (φ : M ⟶ Rep.res (↑e) N) (n : ℕ) (x : ↑(groupHomology M n)) : (CategoryTheory.ConcreteCategory.hom (transfer N S' n)) ((CategoryTheory.ConcreteCategory.hom (groupHomology.map (↑e) φ n)) x) = (CategoryTheory.ConcreteCategory.hom (groupHomology.map (↑(Subgroup.congrOfMapEq e he)) (CategoryTheory.CategoryStruct.comp (Rep.resMap S.subtype φ) ⋯.toRes) n)) ((CategoryTheory.ConcreteCategory.hom (transfer M S n)) x)

The transfer is compatible with a group isomorphism. Let e : G ≃* G' carry S onto S' and let φ : M ⟶ Res_e N. Then the transfers Hₙ(G, M) ⟶ Hₙ(S, Res_S M) and Hₙ(G', N) ⟶ Hₙ(S', Res_S' N) commute with the maps induced by (e, φ) over G and by its restriction (e|_S, Res_S φ) over S. This extends TauCeti.groupHomology.map_comp_transfer, the case where e is the identity, to a change of group.