Shapiro's lemma for group cohomology

Given a commutative ring k and a subgroup S ≤ G, the file RepresentationTheory/Coinduced.lean proves that the functor Coind_S^G : Rep k S ⥤ Rep k G preserves epimorphisms. Since Res(S) : Rep k G ⥤ Rep k S is left adjoint to Coind_S^G, this means Res(S) preserves projective objects. Since Res(S) is also exact, 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.

Main definitions

• groupCohomology.coindIso A n: Shapiro's lemma for group cohomology: an isomorphism Hⁿ(G, Coind_S^G(A)) ≅ Hⁿ(S, A), given a subgroup S ≤ G and an S-representation A.

!

noncomputable def groupCohomology.linearYonedaObjResProjectiveResolutionIso {k G : Type u} [CommRing k] [Group G] {S : Subgroup G} (P : CategoryTheory.ProjectiveResolution (Rep.trivial k G k)) (A : Rep k ↥S) : ((Action.res (ModuleCat k) S.subtype).mapProjectiveResolution P).complex.linearYonedaObj k A ≅ P.complex.linearYonedaObj k (Rep.coind S.subtype A)

Given a projective resolution P of k as a k-linear G-representation, a subgroup S ≤ G, and a k-linear S-representation A, this is an isomorphism of complexes Hom(Res(S)(P), A) ≅ Hom(P, Coind_S^G(A)).

Equations

• groupCohomology.linearYonedaObjResProjectiveResolutionIso P A = HomologicalComplex.Hom.isoOfComponents (fun (x : ℕ) => (Rep.resCoindHomEquiv S.subtype (P.complex.X x) A).toModuleIso) ⋯

noncomputable def groupCohomology.coindIso {k G : Type u} [CommRing k] [Group G] {S : Subgroup G} [DecidableEq G] (A : Rep k ↥S) (n : ℕ) : groupCohomology (Rep.coind S.subtype A) n ≅ groupCohomology A n

Shapiro's lemma: given a subgroup S ≤ G and an S-representation A, we have Hⁿ(G, Coind_S^G(A)) ≅ Hⁿ(S, A).

Equations

• One or more equations did not get rendered due to their size.