isIso_leftRightHomologyComparison'_of_homologyData

English

The left-right morphism factors through the left and right homology isomorphisms, providing a neat factorization of the comparison morphism.

Русский

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

LaTeX

$$$\\text{leftRightHomologyComparison}'(h_1,h_2) = h_1.\\mathrm{left}\\; \\mathrm{homologyIso}^{-1} \\circ h_2.\\mathrm{homologyIso}.\\mathrm{hom}$$$

Lean4

instance isIso_leftRightHomologyComparison'_of_homologyData (h : S.HomologyData) :
    IsIso (leftRightHomologyComparison' h.left h.right) :=
  by
  rw [h.leftRightHomologyComparison'_eq]
  infer_instance

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