isoHomologyι₀ — Mathlib

English

The inverse canonical isomorphism for 0-th homology is natural with respect to morphisms of chain complexes.

Русский

Обратный канонический изоморфизм нулевой гомологии естественно ведет себя при отображениях между комплексами.

LaTeX

$$$ K.isoHomologyι_0^{-1} \circ \operatorname{HomologyMap}(\varphi,0) = \operatorname{opcyclesMap}(\varphi,0) \circ L.isoHomologyι_0^{-1} $$$

Lean4

/-- The canonical isomorphism `K.homology 0 ≅ K.opcycles 0` for a chain complex `K`
indexed by `ℕ`. -/
noncomputable abbrev isoHomologyι₀ : K.homology 0 ≅ K.opcycles 0 :=
  K.isoHomologyι 0 _ rfl (by simp)

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