Theorems · Theorem · category theory

CategoryTheory.Limits.BinaryBicone.inl_fst

∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {P Q : C} (self : CategoryTheory.Limits.BinaryBicone P Q),
  CategoryTheory.CategoryStruct.comp self.inl self.fst = CategoryTheory.CategoryStruct.id P

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

39 results in Mathlib

Foundations

Depth 5 from the axioms · uses no axioms

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasZeroMorphisms