homology_π_ι — Mathlib

English

The composition of homologyπ with homologyι equals iCycles composed with pOpcycles: homologyπ ≫ homologyι = iCycles ≫ pOpcycles.

Русский

Сочетание отображения гомологии π с ι даёт отображение iCycles с pOpcycles: homologyπ ≫ homologyι = iCycles ≫ pOpcycles.

LaTeX

$$$S.homology\pi \circ S.homology\iota = S.iCycles \circ S.pOpcycles$$$

Lean4

@[reassoc (attr := simp)]
theorem homology_π_ι : S.homologyπ ≫ S.homologyι = S.iCycles ≫ S.pOpcycles :=
  by
  dsimp only [homologyπ, homologyι]
  simpa only [assoc, S.leftRightHomologyComparison_fac] using S.π_leftRightHomologyComparison_ι

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