English
For any ProjectiveResolution P of the trivial G-representation, the nth group cohomology of A is isomorphic to the nth homology of the complex Hom(P.complex, A).
Русский
Для любого проектного разрешения P тривиального представления G, n-я когомология группы A изоморфна n-й гомологии комплекса Hom(P.complex, A).
LaTeX
$$$$ groupCohomology A n \\cong \\mathrm{H}^n( \\mathrm{Hom}(P, A) ). $$$$
Lean4
/-- The `n`th group cohomology of a `k`-linear `G`-representation `A` is isomorphic to
`Hⁿ(Hom(P, A))`, where `P` is any projective resolution of `k` as a trivial `k`-linear
`G`-representation. -/
def groupCohomologyIso [Group G] [DecidableEq G] (A : Rep k G) (n : ℕ) (P : ProjectiveResolution (Rep.trivial k G k)) :
groupCohomology A n ≅ (P.complex.linearYonedaObj k A).homology n :=
groupCohomologyIsoExt A n ≪≫ P.isoExt _ _
