homologyπ_comp_leftHomologyIso_inv

English

The composition of the homology map with the inverse left homology is the same as the left homology map: hπ ≫ leftHomologyIso^{-1} = leftHomologyπ.

Русский

Сочетание отображения гомологии с обратной левой гомологией даёт то же самое отображение, что и левый гомологический компонент: hπ ∘ leftHomologyIso^{-1} = leftHomologyπ.

LaTeX

$$$S.homology\pi \circ S.leftHomologyIso^{-1} = S.leftHomology\pi$$$

Lean4

@[reassoc (attr := simp)]
theorem homologyπ_comp_leftHomologyIso_inv : S.homologyπ ≫ S.leftHomologyIso.inv = S.leftHomologyπ :=
  by
  dsimp only [homologyπ]
  simp only [assoc, Iso.hom_inv_id, comp_id]

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