hasHomology_of_isIsoLeftRightHomologyComparison

English

If the left-right comparison is an isomorphism, the ShortComplex has Homology data given by the isomorphic left/right data.

Русский

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

LaTeX

$$$[S.HasLeftHomology] \\; [S.HasRightHomology] \\; [IsIso(\\text{leftRightHomologyComparison}'(h_1,h_2))] \Rightarrow S.HasHomology$$$

Lean4

theorem hasHomology_of_isIsoLeftRightHomologyComparison [S.HasLeftHomology] [S.HasRightHomology]
    [h : IsIso S.leftRightHomologyComparison] : S.HasHomology :=
  by
  haveI : IsIso (leftRightHomologyComparison' S.leftHomologyData S.rightHomologyData) := h
  exact hasHomology_of_isIso_leftRightHomologyComparison' S.leftHomologyData S.rightHomologyData

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