Complements on left homology map data

Two facts about ShortComplex.LeftHomologyMapData: the compatibility commf' follows from the compatibility commi (LeftHomologyMapData.commf'_of_commi), and a variant of LeftHomologyMapData.homologyMap_comm where the left homology objects are replaced by isomorphic objects (LeftHomologyMapData.homologyMap_comp_homologyIso_trans_hom).

theorem CategoryTheory.ShortComplex.LeftHomologyMapData.commf'_of_commi {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} {φ : S₁ ⟶ S₂} (h₁ : S₁.LeftHomologyData) (h₂ : S₂.LeftHomologyData) {φK : h₁.K ⟶ h₂.K} (commi : CategoryStruct.comp φK h₂.i = CategoryStruct.comp h₁.i φ.τ₂) : CategoryStruct.comp h₁.f' φK = CategoryStruct.comp φ.τ₁ h₂.f'

The compatibility commf' of a left homology map data follows from the compatibility commi.

theorem CategoryTheory.ShortComplex.LeftHomologyMapData.homologyMap_comp_homologyIso_trans_hom {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} [S₁.HasHomology] [S₂.HasHomology] {φ : S₁ ⟶ S₂} {h₁ : S₁.LeftHomologyData} {h₂ : S₂.LeftHomologyData} (γ : LeftHomologyMapData φ h₁ h₂) {A₁ A₂ : C} (e₁ : A₁ ≅ h₁.H) (e₂ : A₂ ≅ h₂.H) (g : A₁ ⟶ A₂) (hg : CategoryStruct.comp e₁.hom γ.φH = CategoryStruct.comp g e₂.hom) : CategoryStruct.comp (homologyMap φ) (h₂.homologyIso ≪≫ e₂.symm).hom = CategoryStruct.comp (h₁.homologyIso ≪≫ e₁.symm).hom g

A variant of LeftHomologyMapData.homologyMap_comm where the left homology objects are replaced by isomorphic objects.