π_leftRightHomologyComparison_ι

English

Under left/right homology assumptions, the left-right homology comparison composed with the right injection equals the cycle embedding followed by open cycles projection.

Русский

При предположениях по левой и правой гомологическим данным, композиция лево-правого сопоставления с инъекцией справаEquiv циклового смысла равна включению в цикл и проекции п/циклов.

LaTeX

$$$\\text{leftHomologyπ} \\; \\circ \\text{leftRightHomologyComparison}'(h_1,h_2) \\circ \\text{rightHomology${}\\!\\iota} = \\text{cycles} \\circ \\text{pOpcycles}$$$

Lean4

@[reassoc (attr := simp)]
theorem π_leftRightHomologyComparison_ι [S.HasLeftHomology] [S.HasRightHomology] :
    S.leftHomologyπ ≫ S.leftRightHomologyComparison ≫ S.rightHomologyι = S.iCycles ≫ S.pOpcycles :=
  π_leftRightHomologyComparison'_ι _ _

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