Theorems · Definition · category theory

CategoryTheory.Limits.BinaryBicone.inr

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

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

47 results in Mathlib

Foundations

Depth 4 from the axioms · uses no axioms

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasZeroMorphisms