leftRightHomologyComparison_eq — Mathlib

English

The canonical left-right homology map equals the composition of the left-homology iso, the central left-right morphism, and the right-homology iso inverted as appropriate.

Русский

Каноническое отображение лево-правой гомологии равно композиции левого гомологического изо, центрального сопоставления и правого гомологического изо, инвертированного по мере необходимости.

LaTeX

$$$\\text{leftRightHomologyComparison}'(h_1,h_2) = h_1.\\mathrm{leftHomologyIso}.\\mathrm{hom} \\; \\circ \\; \\text{leftRightHomologyComparison}'(h_1,h_2) \\circ h_2.\\mathrm{rightHomologyIso}.\\mathrm{inv}$$$

Lean4

theorem leftRightHomologyComparison_eq [S.HasLeftHomology] [S.HasRightHomology] (h₁ : S.LeftHomologyData)
    (h₂ : S.RightHomologyData) :
    S.leftRightHomologyComparison =
      h₁.leftHomologyIso.hom ≫ leftRightHomologyComparison' h₁ h₂ ≫ h₂.rightHomologyIso.inv :=
  leftRightHomologyComparison'_compatibility _ _ _ _

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