isoHomologyι₀_inv_naturality — Mathlib

English

A similar naturality statement holds for the inverse isomorphism in the 0-th homology context.

Русский

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

LaTeX

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

Lean4

@[reassoc (attr := simp)]
theorem isoHomologyι₀_inv_naturality [L.HasHomology 0] :
    K.isoHomologyι₀.inv ≫ HomologicalComplex.homologyMap φ 0 =
      HomologicalComplex.opcyclesMap φ 0 ≫ L.isoHomologyι₀.inv :=
  by
  simp only [assoc, ← cancel_mono (L.homologyι 0), HomologicalComplex.homologyι_naturality,
    HomologicalComplex.isoHomologyι_inv_hom_id_assoc, HomologicalComplex.isoHomologyι_inv_hom_id, comp_id]

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