Transitivity of restriction in group cohomology

Restriction along a tower of subgroups K ≤ H ≤ G is transitive: restriction of Hⁿ⁺¹(G, M) to H and then to K.subgroupOf H is restriction to K, once K.subgroupOf H is identified with K by the change-of-group map along Subgroup.subgroupOfEquivOfLe hKH. This lets the cohomology of a small subgroup be computed in stages through an intermediate subgroup; it is what makes Tate restriction in positive degrees (TauCeti.TateCohomology.posRes) functorial along a tower of layers of a class formation.

The change-of-group map is unavoidable, because Rep.res does not compose: for K ≤ H ≤ G the composite Rep.res (K.subgroupOf H).subtype (Rep.res H.subtype M) and the single restriction Rep.res K.subtype M are representations of groups with different carrier types (↥(K.subgroupOf H) and ↥K), so the two cannot even be compared as representations. The comparison morphism between them is built from Subgroup.subtype_comp_subgroupOfEquivOfLe and Rep.isIntertwiningMap_res_res.

Main results

• TauCeti.groupCohomology.map_subgroupOf_trans: restriction along a tower of subgroups is transitive, in every degree n for n : ℕ.

References

• E. Artin and J. Tate, Class Field Theory, Chapter IV, §6 and Chapter XIV, §4.
• K. S. Brown, Cohomology of Groups, Graduate Texts in Mathematics 87, Springer (1982), Chapter I, §5 for the composition law of the maps induced on cohomology by homomorphisms, and Chapter III, §9 for the dual transitivity of the transfer in group homology (TauCeti.groupHomology.transfer_trans).
• Formally: Mathlib's groupCohomology.map and its composition law groupCohomology.map_comp, of Mathlib/RepresentationTheory/Homological/GroupCohomology/Functoriality.lean, of which this is the case of two inclusions composed with a change of group; and Tau Ceti's Rep.isIntertwiningMap_res_res, of TauCeti/RepresentationTheory/Rep/ChangeOfGroup.lean, which is what makes the two restrictions of M agree along Subgroup.subgroupOfEquivOfLe.

theorem TauCeti.groupCohomology.map_subgroupOf_trans {R G : Type u} [CommRing R] [Group G] (M : Rep R G) {K H : Subgroup G} (hKH : K ≤ H) (n : ℕ) : CategoryTheory.CategoryStruct.comp (groupCohomology.map H.subtype (CategoryTheory.CategoryStruct.id (Rep.res H.subtype M)) n) (CategoryTheory.CategoryStruct.comp (groupCohomology.map (K.subgroupOf H).subtype (CategoryTheory.CategoryStruct.id (Rep.res (K.subgroupOf H).subtype (Rep.res H.subtype M))) n) (groupCohomology.map ↑(Subgroup.subgroupOfEquivOfLe hKH).symm ⋯.ofRes n)) = groupCohomology.map K.subtype (CategoryTheory.CategoryStruct.id (Rep.res K.subtype M)) n

Restriction along a tower of subgroups is transitive: for K ≤ H ≤ G and n : ℕ, the map Hⁿ(G, M) ⟶ Hⁿ(H, Res_H M) along H.subtype followed by the map along (K.subgroupOf H).subtype and then the change-of-group map along Subgroup.subgroupOfEquivOfLe hKH is restriction Hⁿ(G, M) ⟶ Hⁿ(K, Res_K M) along K.subtype. Here K.subgroupOf H, which is K viewed as a subgroup of H, is identified with K by Subgroup.subgroupOfEquivOfLe hKH, under which the two restrictions of M agree (Rep.isIntertwiningMap_res_res).

theorem TauCeti.groupCohomology.map_subgroupOf_trans_assoc {R G : Type u} [CommRing R] [Group G] (M : Rep R G) {K H : Subgroup G} (hKH : K ≤ H) (n : ℕ) {Z : ModuleCat R} (h : groupCohomology (Rep.res K.subtype M) n ⟶ Z) : CategoryTheory.CategoryStruct.comp (groupCohomology.map H.subtype (CategoryTheory.CategoryStruct.id (Rep.res H.subtype M)) n) (CategoryTheory.CategoryStruct.comp (groupCohomology.map (K.subgroupOf H).subtype (CategoryTheory.CategoryStruct.id (Rep.res (K.subgroupOf H).subtype (Rep.res H.subtype M))) n) (CategoryTheory.CategoryStruct.comp (groupCohomology.map ↑(Subgroup.subgroupOfEquivOfLe hKH).symm ⋯.ofRes n) h)) = CategoryTheory.CategoryStruct.comp (groupCohomology.map K.subtype (CategoryTheory.CategoryStruct.id (Rep.res K.subtype M)) n) h

Restriction along a tower of subgroups is transitive: for K ≤ H ≤ G and n : ℕ, the map Hⁿ(G, M) ⟶ Hⁿ(H, Res_H M) along H.subtype followed by the map along (K.subgroupOf H).subtype and then the change-of-group map along Subgroup.subgroupOfEquivOfLe hKH is restriction Hⁿ(G, M) ⟶ Hⁿ(K, Res_K M) along K.subtype. Here K.subgroupOf H, which is K viewed as a subgroup of H, is identified with K by Subgroup.subgroupOfEquivOfLe hKH, under which the two restrictions of M agree (Rep.isIntertwiningMap_res_res).