hasBinaryBiproduct_of_total — Mathlib

English

Any morphism f : Z → X ⊞ Y factors uniquely as f₁ ≫ inl + f₂ ≫ inr for suitable f₁, f₂.

Русский

Любой морфизм f : Z → X ⊞ Y факторизуется единственным образом как f₁ ≫ inl + f₂ ≫ inr для подходящих f₁, f₂.

LaTeX

$$$\exists f_1, f_2,\; f = f_1 \;\gg\; \operatorname{biprod.inl} + f_2 \;\gg\; \operatorname{biprod.inr}$$$

Lean4

/-- In a preadditive category, we can construct a binary biproduct for `X Y : C` from
any binary bicone `b` satisfying `total : b.fst ≫ b.inl + b.snd ≫ b.inr = 𝟙 b.X`.

(That is, such a bicone is a limit cone and a colimit cocone.)
-/
theorem hasBinaryBiproduct_of_total {X Y : C} (b : BinaryBicone X Y) (total : b.fst ≫ b.inl + b.snd ≫ b.inr = 𝟙 b.pt) :
    HasBinaryBiproduct X Y :=
  HasBinaryBiproduct.mk
    { bicone := b
      isBilimit := isBinaryBilimitOfTotal b total }

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