isIso_homologyι₀ — Mathlib

English

There is a canonical isomorphism between the zero-th homology and the zero-th cycles of a chain complex K.

Русский

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

LaTeX

$$$ K.homology 0 \cong K.opcycles 0 $$$

Lean4

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

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