Theorems · Definition · category theory

CategoryTheory.Limits.isBinaryBilimitOfTotal

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {X Y : C} →
        (b : CategoryTheory.Limits.BinaryBicone X Y) →
          CategoryTheory.CategoryStruct.comp b.fst b.inl + CategoryTheory.CategoryStruct.comp b.snd b.inr =
              CategoryTheory.CategoryStruct.id b.pt →
            b.IsBilimit

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.)

Defined in

Mathlib.CategoryTheory.Preadditive.Biproducts

Cited by

1 results in Mathlib

Foundations

Depth 26 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.Preadditive