English
There is an isomorphism between H_n(G,A) and the homology of the coinvariants tensor A with a projective resolution P of the trivial G-module, i.e. H_n(G,A) ≅ H_n( (P.complex.coinvariantsTensorObj A) ).
Русский
Существуют канонические изоморфизмы H_n(G,A) и гомология коэффициентов превращения, получаемые из 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
`Torₙ(A, k)` (taken in `Rep k G`), where `k` is a trivial `k`-linear `G`-representation. -/
def groupHomologyIsoTor [DecidableEq G] (n : ℕ) : groupHomology A n ≅ ((Tor k G n).obj A).obj (Rep.trivial k G k) :=
isoOfQuasiIsoAt (HomotopyEquiv.ofIso (inhomogeneousChainsIso A)).hom n ≪≫ (torIso A (barResolution k G) n).symm
