right_homologyIso_eq_left_homologyIso_trans_iso

English

The right-hand side homology iso relates to the left-hand side via a transitive relation with the middle morphism.

Русский

Правое гомологическое изоморфирование связано с левым через транзитивное отношение с промежуточным отображением.

LaTeX

$$$h.\\text{right}.\\mathrm{homologyIso} = h.\\text{left}.\\mathrm{homologyIso} \\circ h.\\mathrm{iso}$$$

Lean4

theorem right_homologyIso_eq_left_homologyIso_trans_iso (h : S.HomologyData) [S.HasHomology] :
    h.right.homologyIso = h.left.homologyIso ≪≫ h.iso :=
  by
  suffices h.iso = h.left.homologyIso.symm ≪≫ h.right.homologyIso by rw [this, Iso.self_symm_id_assoc]
  ext
  dsimp
  rw [← leftRightHomologyComparison'_fac, leftRightHomologyComparison'_eq]

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