English
A refined expression shows leftRightHomologyComparison' equals the left-homology map composed with the iso and then with the right-homology map.
Русский
Уточнённое выражение показывает, что leftRightHomologyComparison' равняется композиции отображения левой гомологии с изоморфизмом и далее правого отображения гомологии.
LaTeX
$$$\\text{leftRightHomologyComparison}'(h_1,h_2) = h_1.\\text{leftHomologyMap}'(\\mathrm{Id}_S) \\circ h.\\mathrm{iso}.hom \\circ \\text{rightHomologyMap}'(\\mathrm{Id}_S)$$$
Lean4
theorem leftRightHomologyComparison'_eq_leftHomologpMap'_comp_iso_hom_comp_rightHomologyMap' (h : S.HomologyData)
(h₁ : S.LeftHomologyData) (h₂ : S.RightHomologyData) :
leftRightHomologyComparison' h₁ h₂ =
leftHomologyMap' (𝟙 S) h₁ h.left ≫ h.iso.hom ≫ rightHomologyMap' (𝟙 S) h.right h₂ :=
by
simpa only [h.leftRightHomologyComparison'_eq] using leftRightHomologyComparison'_compatibility h₁ h.left h₂ h.right
