English
There is an isomorphism H_n(G,A) ≅ H_n((P.complex.coinvariantsTensorObj A)) for any projective resolution P of the trivial G-representation.
Русский
Для любого проектного разрешения P тривиального представления группы G выполняется изоморфизм H_n(G,A) ≅ H_n((P.complex.coinvariantsTensorObj A)).
LaTeX
$$groupHomologyIso(A,n,P) : groupHomology A n ≅ H_n(P.complex.coinvariantsTensorObj A)$$
Lean4
/-- The `n`th group homology of a `k`-linear `G`-representation `A` is isomorphic to
`Hₙ((A ⊗ P)_G)`, where `P` is any projective resolution of `k` as a trivial `k`-linear
`G`-representation. -/
def groupHomologyIso [DecidableEq G] (A : Rep k G) (n : ℕ) (P : ProjectiveResolution (Rep.trivial k G k)) :
groupHomology A n ≅ (P.complex.coinvariantsTensorObj A).homology n :=
groupHomologyIsoTor A n ≪≫ torIso A P n
