English
For a subgroup S ≤ G and an S-representation A, cohomology with trivial G-action on coind_S^G(A) is isomorphic to cohomology of A over S.
Русский
Для подгруппы S ≤ G и представления A над S когомология группы G действует на Coind_S^G(A) так же, как когомология S над A.
LaTeX
$$groupCohomology.coindIso A n : groupCohomology (coind S.subtype A) n ≅ groupCohomology A n$$
Lean4
/-- 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)).` -/
noncomputable def linearYonedaObjResProjectiveResolutionIso (P : ProjectiveResolution (trivial k G k)) (A : Rep k S) :
((Action.res _ S.subtype).mapProjectiveResolution P).complex.linearYonedaObj k A ≅
P.complex.linearYonedaObj k (coind S.subtype A) :=
HomologicalComplex.Hom.isoOfComponents (fun _ => (resCoindHomEquiv _ _ _).toModuleIso) fun _ _ _ =>
ModuleCat.hom_ext (LinearMap.ext fun f => Action.Hom.ext <| by ext; simp [hom_comm_apply])
