English
If the left-right comparison is an isomorphism, then the ShortComplex has a Homology structure.
Русский
Если сопоставление лево-правой гомологии является изоморфизмом, то короткий комплекс имеет структуру гомологии.
LaTeX
$$$[\\text{S HasHomology}] \\Rightarrow [IsIso(\\text{leftRightHomologyComparison}'(h_1,h_2))] \\Rightarrow S.HasHomology$$$
Lean4
@[reassoc]
theorem leftRightHomologyComparison'_fac (h₁ : S.LeftHomologyData) (h₂ : S.RightHomologyData) [S.HasHomology] :
leftRightHomologyComparison' h₁ h₂ = h₁.homologyIso.inv ≫ h₂.homologyIso.hom :=
by
rw [leftRightHomologyComparison'_eq_leftHomologpMap'_comp_iso_hom_comp_rightHomologyMap' S.homologyData h₁ h₂]
dsimp only [LeftHomologyData.homologyIso, LeftHomologyData.leftHomologyIso, Iso.symm, Iso.trans, Iso.refl,
leftHomologyMapIso', leftHomologyIso, RightHomologyData.homologyIso, RightHomologyData.rightHomologyIso,
rightHomologyMapIso', rightHomologyIso]
simp only [assoc, ← leftHomologyMap'_comp_assoc, id_comp, ← rightHomologyMap'_comp]
