H0IsoOfIsTrivial — Mathlib

English

If A is a trivial G-representation, then H0(G,A) is isomorphic to A.V (the underlying vector space of A).

Русский

Если представление A тривиально по действию G, то H0(G,A) изоморфно A.V (гладкая структура пространства над A).

LaTeX

$$def H0IsoOfIsTrivial : H0 A ≅ A.V$$

Lean4

/-- When the representation on `A` is trivial, then `H₀(G, A)` is all of `A.` -/
def H0IsoOfIsTrivial : H0 A ≅ A.V :=
  ((inhomogeneousChains A).isoHomologyπ 1 0 (by simp) <| by ext;
        simp [inhomogeneousChains.d_def, inhomogeneousChains.d_single (G := G),
          Unique.eq_default (α := Fin 0 → G)]).symm ≪≫
    cyclesIso₀ A

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