Theorems · Definition · category theory

CategoryTheory.Limits.BinaryBicone.pt

{C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] → {P Q : C} → CategoryTheory.Limits.BinaryBicone P Q → C

A binary bicone for a pair of objects P Q : C consists of the cone point X, maps from X to both P and Q, and maps from both P and Q to X, so that inl ≫ fst = 𝟙 P, inl ≫ snd = 0, inr ≫ fst = 0, and inr ≫ snd = 𝟙 Q

Defined in

Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

Cited by

95 results in Mathlib

Foundations

Depth 3 from the axioms, rests on 4 definitions · uses no axioms

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasZeroMorphisms