homology_π_ι — Mathlib

English

At index i, the composition K.homologyπ i ≫ K.homologyι i equals K.iCycles i ≫ K.pOpcycles i, expressing the standard relation between the π and ι maps on a chain complex.

Русский

В позиции i композиция K.homologyπ i ≫ K.homologyι i равна K.iCycles i ≫ K.pOpcycles i, выражая стандартное соотношение между отображениями π и ι в цепочном контексте.

LaTeX

$$$$ K.homologyπ i \;\\circ\\; K.homologyι i = K.iCycles i \;\\circ\\; K.pOpcycles i $$$$

Lean4

@[reassoc (attr := simp)]
theorem homology_π_ι : K.homologyπ i ≫ K.homologyι i = K.iCycles i ≫ K.pOpcycles i :=
  (K.sc i).homology_π_ι

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