H0Iso — Mathlib

English

The 0th group homology H0 A is isomorphic to the coinvariants of A.

Русский

0-я гомологическая группа H0(A) изоморфна конивариантам A.

LaTeX

$$$ H0 A \cong (\mathrm{coinvariantsFunctor}\ k\ G).obj A $$$

Lean4

/-- The 0th group homology of `A`, defined as the 0th homology of the complex of inhomogeneous
chains, is isomorphic to the invariants of the representation on `A`. -/
def H0Iso : H0 A ≅ (coinvariantsFunctor k G).obj A :=
  (ChainComplex.isoHomologyι₀ _) ≪≫ opcyclesIso₀ A

Похожие утверждения