Commit 2025-07-03 08:36 ec4672ac

feat(RepresentationTheory/GroupCohomology): add Shapiro's lemma (#25937) Given a commutative ring k and a finite index subgroup S ≤ G, the file RepresentationTheory/FiniteIndex.lean defines a natural isomorphism between the functors Ind_S^G, Coind_S^G : Rep k S ⥤ Rep k G. Using this isomorphism, we conclude that the (Co)ind_S^G and Res(S) : Rep k G ⥤ Rep k S are both left and right adjoint to each other, and thus that Res(S) is an exact functor which preserves projective objects. In particular, given a projective resolution P of k as a trivial k-linear G-representation, Res(S)(P) is a projective resolution of k as a trivial k-linear S-representation. Since Hom(Res(S)(P), A) ≅ Hom(P, Coind_S^G(A)) for any S-representation A, we conclude Shapiro's lemma for group cohomology: Hⁿ(G, Coind_S^G(A)) ≅ Hⁿ(S, A) for all n.