g_shortComplexTruncLEX₃ToTruncGE

English

In a Abelian category, for a complementary pair of truncations ac, the composed morphism g from the short complex truncLE side with the truncLEX₃ToTruncGE side equals the truncation morphism πTruncGE on the second boundary.

Русский

В абелевой категории композиция г на стороне короткого комплекса truncLE со стороны truncLEX₃ToTruncGE равна морфизму отсечения πTruncGE на второй границе для парыac.

LaTeX

$$$ (K.shortComplexTruncLE\\, e_1).g \\;\\circ\\; K.shortComplexTruncLEX₃ToTruncGE\\, ac = K.\\piTruncGE\\, e_2 $$$

Lean4

@[reassoc (attr := simp)]
theorem g_shortComplexTruncLEX₃ToTruncGE :
    (K.shortComplexTruncLE e₁).g ≫ K.shortComplexTruncLEX₃ToTruncGE ac = K.πTruncGE e₂ :=
  cokernel.π_desc _ _ _

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