Theorems · Theorem · category theory

CategoryTheory.Limits.BinaryBicone.inr_snd_assoc

∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {P Q : C} (self : CategoryTheory.Limits.BinaryBicone P Q) {Z : C} (h : Q ⟶ Z),
  CategoryTheory.CategoryStruct.comp self.inr (CategoryTheory.CategoryStruct.comp self.snd h) = h

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

15 results in Mathlib

Foundations

Depth 6 from the axioms · uses Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasZeroMorphisms