Shapiro's lemma for group homology

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.

In RepresentationTheory/Homological/GroupHomology/Induced.lean, given a G-representation X, we define a natural isomorphism between the functors Rep k S ⥤ ModuleCat k sending A to (Ind_S^G A ⊗ X)_G and to (A ⊗ Res(S)(X))_S. Hence a projective resolution P of k as a trivial G-representation induces an isomorphism of complexes (Ind_S^G A ⊗ P)_G ≅ (A ⊗ Res(S)(P))_S, and since the homology of these complexes calculate group homology, we conclude Shapiro's lemma: Hₙ(G, Ind_S^G(A)) ≅ Hₙ(S, A) for all n.

Main definitions

• groupHomology.indIso A n: Shapiro's lemma for group homology: an isomorphism Hₙ(G, Ind_S^G(A)) ≅ Hₙ(S, A), given a subgroup S ≤ G and an S-representation A.

@[reducible, inline]

noncomputable abbrev groupHomology.coinvariantsTensorResProjectiveResolutionIso {k G : Type u} [CommRing k] [Group G] (S : Subgroup G) (A : Rep k ↥S) (P : CategoryTheory.ProjectiveResolution (Rep.trivial k G k)) : HomologicalComplex.coinvariantsTensorObj A ((Action.res (ModuleCat k) S.subtype).mapProjectiveResolution P).complex ≅ HomologicalComplex.coinvariantsTensorObj (Rep.ind S.subtype A) P.complex

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 (A ⊗ Res(S)(P))_S ≅ (Ind_S^G(A) ⊗ P)_G.

Equations

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

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

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

Equations

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