isIso_leftRightHomologyComparison'

English

The compatibility statement asserts that composing left and right maps around the canonical morphism yields a diagram that commutes.

Русский

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

LaTeX

$$$\\text{leftHomologyMap}'(\\mathrm{Id}_S) \\circ \\text{leftRightHomologyComparison}'(h_1,h_2) \\circ \\text{rightHomologyMap}'(\\mathrm{Id}_S) = \\text{...}$$$

Lean4

instance isIso_leftRightHomologyComparison' [S.HasHomology] (h₁ : S.LeftHomologyData) (h₂ : S.RightHomologyData) :
    IsIso (leftRightHomologyComparison' h₁ h₂) :=
  by
  rw [leftRightHomologyComparison'_compatibility h₁ S.homologyData.left h₂ S.homologyData.right]
  infer_instance

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