Commit 2025-06-17 08:16 4466755c

feat(RepresentationTheory/Homological/GroupHomology/Functoriality): add functoriality (#25880) Given a commutative ring k, a group homomorphism f : G →* H, a k-linear G-representation A, a k-linear H-representation B, and a representation morphism A ⟶ Res(f)(B), we get a chain map inhomogeneousChains A ⟶ inhomogeneousChains B and hence maps on group homology Hⁿ(H, A) ⟶ Hⁿ(G, B). A subsequent PR will add specialised API for low degree, and a future PR will add support for switching resolution.