total — Mathlib

English

In a preadditive category, a colimit cocone for a discrete diagram yields a bilimit bicone for the same diagram.

Русский

В преддобавительной категории колимитный кокон для дискретной диаграммы задаёт билимитный бикокон той же диаграммы.

LaTeX

$$biconeIsBilimitOfColimitCoconeOfIsColimit f ht$$

Lean4

/-- In any preadditive category, any biproduct satisfies
`∑ j : J, biproduct.π f j ≫ biproduct.ι f j = 𝟙 (⨁ f)`
-/
@[simp]
theorem total : ∑ j : J, biproduct.π f j ≫ biproduct.ι f j = 𝟙 (⨁ f) :=
  IsBilimit.total (biproduct.isBilimit _)

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