of_hasBinaryCoproduct — Mathlib

English

If binary coproducts exist in a preadditive category, then binary biproducts exist as well, by duality with the coproduct-to-biproduct construction.

Русский

Если существуют бинарные coproducts, то существуют и бинарные biproducts, по двойности дуальной конструкции coproduct → biproduct.

LaTeX

$$HasBinaryCoproduct X Y ⇒ HasBinaryBiproduct X Y$$

Lean4

/-- In a preadditive category, if the coproduct of `X` and `Y` exists, then the
binary biproduct of `X` and `Y` exists. -/
theorem of_hasBinaryCoproduct (X Y : C) [HasBinaryCoproduct X Y] : HasBinaryBiproduct X Y :=
  HasBinaryBiproduct.mk
    { bicone := _
      isBilimit := binaryBiconeIsBilimitOfColimitCoconeOfIsColimit (colimit.isColimit _) }

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