English
Shapiro's lemma: for a subgroup S ≤ G and an S-representation A, there is an isomorphism Hn(G,Ind_S^G(A)) ≅ Hn(S,A).
Русский
Лемма Шапиро: при подгруппе S ≤ G и представлении A на S существует изоморфизм гиперповерхностей Hn(G,Ind_S^G(A)) ≅ Hn(S,A).
LaTeX
$$$H_n(G,\\mathrm{Ind}_S^G(A)) \\cong H_n(S,A).$$$
Lean4
/-- Shapiro's lemma: given a subgroup `S ≤ G` and an `S`-representation `A`, we have
`Hₙ(G, Ind_S^G(A)) ≅ Hₙ(S, A).` -/
noncomputable def indIso [DecidableEq G] (A : Rep k S) (n : ℕ) :
groupHomology (ind S.subtype A) n ≅ groupHomology A n :=
(HomologicalComplex.homologyFunctor _ _ _).mapIso
(inhomogeneousChainsIso (ind S.subtype A) ≪≫
(coinvariantsTensorResProjectiveResolutionIso S A (barResolution k G)).symm) ≪≫
(groupHomologyIso A n ((Action.res _ _).mapProjectiveResolution <| barResolution k G)).symm
