leftRightHomologyComparison_fac — Mathlib

English

Left-Right equality can be expressed via an explicit factorization through the left/right homology isos.

Русский

Сопоставление лево-правой гомологии может быть выражено через явное факторизование через левые и правые изоморфизмы гомологии.

LaTeX

$$$\\text{leftRightHomologyComparison} = h_1.\\text{leftHomologyIso}.hom \\circ h_2.\\text{rightHomologyIso}.inv$$$

Lean4

@[reassoc]
theorem leftRightHomologyComparison_fac [S.HasHomology] :
    S.leftRightHomologyComparison = S.leftHomologyIso.hom ≫ S.rightHomologyIso.inv := by
  simpa only [LeftHomologyData.homologyIso_leftHomologyData, Iso.symm_inv,
    RightHomologyData.homologyIso_rightHomologyData, Iso.symm_hom] using
    leftRightHomologyComparison'_fac S.leftHomologyData S.rightHomologyData

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