isIso_homologyπ₀ — Mathlib

English

There is an isomorphism between the 0-th homology π₀ and the 0-th cycles π₀ for cochain complexes.

Русский

Существует изоморфизм между нулевой гомологией π₀ и нулевыми циклами π₀ для коцепочечных комплексов.

LaTeX

$$$ \operatorname{IsIso}(\operatorname{homology\,π}_0(K)) $$$

Lean4

instance isIso_homologyπ₀ : IsIso (K.homologyπ 0) :=
  K.isIso_homologyπ _ 0 rfl (by simp)

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