Shapiro's lemma for group cohomology

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.

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 finite index subgroup S ≤ G and an S-representation A.

!

noncomputable def groupCohomology.linearYonedaObjResProjectiveResolutionIso {k G : Type u} [CommRing k] [Group G] {S : Subgroup G} [DecidableRel ⇑(QuotientGroup.rightRel S)] [S.FiniteIndex] (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 finite index 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} [DecidableRel ⇑(QuotientGroup.rightRel S)] [S.FiniteIndex] [DecidableEq G] (A : Rep k ↥S) (n : ℕ) : groupCohomology (Rep.coind S.subtype A) n ≅ groupCohomology A n

Shapiro's lemma: given a finite index 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.