Loogle!

Result

Found 115 declarations mentioning CategoryTheory.Limits.BinaryBicone.pt.

• CategoryTheory.Limits.BinaryBicone.pt 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {P Q : C} (self : CategoryTheory.Limits.BinaryBicone P Q) : C
• CategoryTheory.Limits.BinaryBicone.retract_left 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {P Q : C} (c : CategoryTheory.Limits.BinaryBicone P Q) : CategoryTheory.Retract P c.pt
• CategoryTheory.Limits.BinaryBicone.retract_right 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {P Q : C} (c : CategoryTheory.Limits.BinaryBicone P Q) : CategoryTheory.Retract Q c.pt
• CategoryTheory.Limits.BinaryBicone.fst 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {P Q : C} (self : CategoryTheory.Limits.BinaryBicone P Q) : self.pt ⟶ P
• CategoryTheory.Limits.BinaryBicone.inl 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {P Q : C} (self : CategoryTheory.Limits.BinaryBicone P Q) : P ⟶ self.pt
• CategoryTheory.Limits.BinaryBicone.inr 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {P Q : C} (self : CategoryTheory.Limits.BinaryBicone P Q) : Q ⟶ self.pt
• CategoryTheory.Limits.BinaryBicone.snd 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {P Q : C} (self : CategoryTheory.Limits.BinaryBicone P Q) : self.pt ⟶ Q
• CategoryTheory.Limits.BinaryBicone.instIsSplitEpiFst 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {P Q : C} (c : CategoryTheory.Limits.BinaryBicone P Q) : CategoryTheory.IsSplitEpi c.fst
• CategoryTheory.Limits.BinaryBicone.instIsSplitEpiSnd 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {P Q : C} (c : CategoryTheory.Limits.BinaryBicone P Q) : CategoryTheory.IsSplitEpi c.snd
• CategoryTheory.Limits.BinaryBicone.instIsSplitMonoInl 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {P Q : C} (c : CategoryTheory.Limits.BinaryBicone P Q) : CategoryTheory.IsSplitMono c.inl
• CategoryTheory.Limits.BinaryBicone.instIsSplitMonoInr 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {P Q : C} (c : CategoryTheory.Limits.BinaryBicone P Q) : CategoryTheory.IsSplitMono c.inr
• CategoryTheory.Limits.BinaryBicone.fstKernelFork 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (c : CategoryTheory.Limits.BinaryBicone X Y) : CategoryTheory.Limits.KernelFork c.fst
• CategoryTheory.Limits.BinaryBicone.inlCokernelCofork 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (c : CategoryTheory.Limits.BinaryBicone X Y) : CategoryTheory.Limits.CokernelCofork c.inl
• CategoryTheory.Limits.BinaryBicone.inrCokernelCofork 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (c : CategoryTheory.Limits.BinaryBicone X Y) : CategoryTheory.Limits.CokernelCofork c.inr
• CategoryTheory.Limits.BinaryBicone.sndKernelFork 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (c : CategoryTheory.Limits.BinaryBicone X Y) : CategoryTheory.Limits.KernelFork c.snd
• CategoryTheory.Limits.BinaryBicone.toCocone_pt 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {P Q : C} (c : CategoryTheory.Limits.BinaryBicone P Q) : c.toCocone.pt = c.pt
• CategoryTheory.Limits.BinaryBicone.toCone_pt 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {P Q : C} (c : CategoryTheory.Limits.BinaryBicone P Q) : c.toCone.pt = c.pt
• CategoryTheory.Limits.biprod.uniqueUpToIso 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C) [CategoryTheory.Limits.HasBinaryBiproduct X Y] {b : CategoryTheory.Limits.BinaryBicone X Y} (hb : b.IsBilimit) : b.pt ≅ X ⊞ Y
• CategoryTheory.Limits.BinaryBicone.op_pt 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {P Q : C} (b : CategoryTheory.Limits.BinaryBicone P Q) : b.op.pt = Opposite.op b.pt
• CategoryTheory.Limits.BinaryBiconeMorphism.hom 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {P Q : C} {A B : CategoryTheory.Limits.BinaryBicone P Q} (self : CategoryTheory.Limits.BinaryBiconeMorphism A B) : A.pt ⟶ B.pt
• CategoryTheory.Limits.BinaryBicone.ofIso_pt 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {P P' Q Q' : C} (b : CategoryTheory.Limits.BinaryBicone P Q) (eP : P ≅ P') (eQ : Q ≅ Q') : (b.ofIso eP eQ).pt = b.pt
• CategoryTheory.Limits.BinaryBiproduct.bicone_fst 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} [CategoryTheory.Limits.HasBinaryBiproduct X Y] : (CategoryTheory.Limits.BinaryBiproduct.bicone X Y).fst = CategoryTheory.Limits.biprod.fst
• CategoryTheory.Limits.BinaryBiproduct.bicone_inl 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} [CategoryTheory.Limits.HasBinaryBiproduct X Y] : (CategoryTheory.Limits.BinaryBiproduct.bicone X Y).inl = CategoryTheory.Limits.biprod.inl
• CategoryTheory.Limits.BinaryBiproduct.bicone_inr 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} [CategoryTheory.Limits.HasBinaryBiproduct X Y] : (CategoryTheory.Limits.BinaryBiproduct.bicone X Y).inr = CategoryTheory.Limits.biprod.inr
• CategoryTheory.Limits.BinaryBiproduct.bicone_snd 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} [CategoryTheory.Limits.HasBinaryBiproduct X Y] : (CategoryTheory.Limits.BinaryBiproduct.bicone X Y).snd = CategoryTheory.Limits.biprod.snd
• CategoryTheory.Limits.BinaryBicone.inl_fst 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {P Q : C} (self : CategoryTheory.Limits.BinaryBicone P Q) : CategoryTheory.CategoryStruct.comp self.inl self.fst = CategoryTheory.CategoryStruct.id P
• CategoryTheory.Limits.BinaryBicone.inr_snd 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {P Q : C} (self : CategoryTheory.Limits.BinaryBicone P Q) : CategoryTheory.CategoryStruct.comp self.inr self.snd = CategoryTheory.CategoryStruct.id Q
• CategoryTheory.Limits.BinaryBicone.toBiconeFunctor_obj_pt 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (b : CategoryTheory.Limits.BinaryBicone X Y) : (CategoryTheory.Limits.BinaryBicone.toBiconeFunctor.obj b).pt = b.pt
• CategoryTheory.Limits.Bicone.toBinaryBiconeFunctor_obj_pt 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (b : CategoryTheory.Limits.Bicone (CategoryTheory.Limits.pairFunction X Y)) : (CategoryTheory.Limits.Bicone.toBinaryBiconeFunctor.obj b).pt = b.pt
• CategoryTheory.Limits.BinaryBicone.category_id_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {P Q : C} (B : CategoryTheory.Limits.BinaryBicone P Q) : (CategoryTheory.CategoryStruct.id B).hom = CategoryTheory.CategoryStruct.id B.pt
• CategoryTheory.Limits.BinaryBicone.inl_fst_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {P Q : C} (self : CategoryTheory.Limits.BinaryBicone P Q) {Z : C} (h : P ⟶ Z) : CategoryTheory.CategoryStruct.comp self.inl (CategoryTheory.CategoryStruct.comp self.fst h) = h
• CategoryTheory.Limits.BinaryBicone.inr_snd_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [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
• CategoryTheory.Limits.BinaryBicone.inl_snd 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {P Q : C} (self : CategoryTheory.Limits.BinaryBicone P Q) : CategoryTheory.CategoryStruct.comp self.inl self.snd = 0
• CategoryTheory.Limits.BinaryBicone.inr_fst 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {P Q : C} (self : CategoryTheory.Limits.BinaryBicone P Q) : CategoryTheory.CategoryStruct.comp self.inr self.fst = 0
• CategoryTheory.Limits.BinaryBicone.op_fst 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {P Q : C} (b : CategoryTheory.Limits.BinaryBicone P Q) : b.op.fst = b.inl.op
• CategoryTheory.Limits.BinaryBicone.op_inl 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {P Q : C} (b : CategoryTheory.Limits.BinaryBicone P Q) : b.op.inl = b.fst.op
• CategoryTheory.Limits.BinaryBicone.op_inr 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {P Q : C} (b : CategoryTheory.Limits.BinaryBicone P Q) : b.op.inr = b.snd.op
• CategoryTheory.Limits.BinaryBicone.op_snd 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {P Q : C} (b : CategoryTheory.Limits.BinaryBicone P Q) : b.op.snd = b.inr.op
• CategoryTheory.Limits.BinaryBicone.ofIso_fst 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {P P' Q Q' : C} (b : CategoryTheory.Limits.BinaryBicone P Q) (eP : P ≅ P') (eQ : Q ≅ Q') : (b.ofIso eP eQ).fst = CategoryTheory.CategoryStruct.comp b.fst eP.hom
• CategoryTheory.Limits.BinaryBicone.ofIso_inl 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {P P' Q Q' : C} (b : CategoryTheory.Limits.BinaryBicone P Q) (eP : P ≅ P') (eQ : Q ≅ Q') : (b.ofIso eP eQ).inl = CategoryTheory.CategoryStruct.comp eP.inv b.inl
• CategoryTheory.Limits.BinaryBicone.ofIso_inr 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {P P' Q Q' : C} (b : CategoryTheory.Limits.BinaryBicone P Q) (eP : P ≅ P') (eQ : Q ≅ Q') : (b.ofIso eP eQ).inr = CategoryTheory.CategoryStruct.comp eQ.inv b.inr
• CategoryTheory.Limits.BinaryBicone.ofIso_snd 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {P P' Q Q' : C} (b : CategoryTheory.Limits.BinaryBicone P Q) (eP : P ≅ P') (eQ : Q ≅ Q') : (b.ofIso eP eQ).snd = CategoryTheory.CategoryStruct.comp b.snd eQ.hom
• CategoryTheory.Limits.BinaryBiconeMorphism.wfst 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {P Q : C} {A B : CategoryTheory.Limits.BinaryBicone P Q} (self : CategoryTheory.Limits.BinaryBiconeMorphism A B) : CategoryTheory.CategoryStruct.comp self.hom B.fst = A.fst
• CategoryTheory.Limits.BinaryBiconeMorphism.winl 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {P Q : C} {A B : CategoryTheory.Limits.BinaryBicone P Q} (self : CategoryTheory.Limits.BinaryBiconeMorphism A B) : CategoryTheory.CategoryStruct.comp A.inl self.hom = B.inl
• CategoryTheory.Limits.BinaryBiconeMorphism.winr 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {P Q : C} {A B : CategoryTheory.Limits.BinaryBicone P Q} (self : CategoryTheory.Limits.BinaryBiconeMorphism A B) : CategoryTheory.CategoryStruct.comp A.inr self.hom = B.inr
• CategoryTheory.Limits.BinaryBiconeMorphism.wsnd 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {P Q : C} {A B : CategoryTheory.Limits.BinaryBicone P Q} (self : CategoryTheory.Limits.BinaryBiconeMorphism A B) : CategoryTheory.CategoryStruct.comp self.hom B.snd = A.snd
• CategoryTheory.Limits.biprod.uniqueUpToIso_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C) [CategoryTheory.Limits.HasBinaryBiproduct X Y] {b : CategoryTheory.Limits.BinaryBicone X Y} (hb : b.IsBilimit) : (CategoryTheory.Limits.biprod.uniqueUpToIso X Y hb).hom = CategoryTheory.Limits.biprod.lift b.fst b.snd
• CategoryTheory.Limits.biprod.uniqueUpToIso_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C) [CategoryTheory.Limits.HasBinaryBiproduct X Y] {b : CategoryTheory.Limits.BinaryBicone X Y} (hb : b.IsBilimit) : (CategoryTheory.Limits.biprod.uniqueUpToIso X Y hb).inv = CategoryTheory.Limits.biprod.desc b.inl b.inr
• CategoryTheory.Limits.BinaryBicone.isColimitInlCokernelCofork 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} {c : CategoryTheory.Limits.BinaryBicone X Y} (i : CategoryTheory.Limits.IsColimit c.toCocone) : CategoryTheory.Limits.IsColimit c.inlCokernelCofork
• CategoryTheory.Limits.BinaryBicone.isColimitInrCokernelCofork 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} {c : CategoryTheory.Limits.BinaryBicone X Y} (i : CategoryTheory.Limits.IsColimit c.toCocone) : CategoryTheory.Limits.IsColimit c.inrCokernelCofork
• CategoryTheory.Limits.BinaryBicone.isLimitFstKernelFork 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} {c : CategoryTheory.Limits.BinaryBicone X Y} (i : CategoryTheory.Limits.IsLimit c.toCone) : CategoryTheory.Limits.IsLimit c.fstKernelFork
• CategoryTheory.Limits.BinaryBicone.isLimitSndKernelFork 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} {c : CategoryTheory.Limits.BinaryBicone X Y} (i : CategoryTheory.Limits.IsLimit c.toCone) : CategoryTheory.Limits.IsLimit c.sndKernelFork
• CategoryTheory.Limits.BinaryBicone.inl_snd_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {P Q : C} (self : CategoryTheory.Limits.BinaryBicone P Q) {Z : C} (h : Q ⟶ Z) : CategoryTheory.CategoryStruct.comp self.inl (CategoryTheory.CategoryStruct.comp self.snd h) = CategoryTheory.CategoryStruct.comp 0 h
• CategoryTheory.Limits.BinaryBicone.inr_fst_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {P Q : C} (self : CategoryTheory.Limits.BinaryBicone P Q) {Z : C} (h : P ⟶ Z) : CategoryTheory.CategoryStruct.comp self.inr (CategoryTheory.CategoryStruct.comp self.fst h) = CategoryTheory.CategoryStruct.comp 0 h
• CategoryTheory.Limits.BinaryBicone.toBiconeFunctor_obj_ι 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (b : CategoryTheory.Limits.BinaryBicone X Y) (j : CategoryTheory.Limits.WalkingPair) : (CategoryTheory.Limits.BinaryBicone.toBiconeFunctor.obj b).ι j = CategoryTheory.Limits.WalkingPair.casesOn j b.inl b.inr
• CategoryTheory.Limits.BinaryBicone.toBiconeFunctor_obj_π 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (b : CategoryTheory.Limits.BinaryBicone X Y) (j : CategoryTheory.Limits.WalkingPair) : (CategoryTheory.Limits.BinaryBicone.toBiconeFunctor.obj b).π j = CategoryTheory.Limits.WalkingPair.casesOn j b.fst b.snd
• CategoryTheory.Limits.BinaryBiconeMorphism.wfst_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {P Q : C} {A B : CategoryTheory.Limits.BinaryBicone P Q} (self : CategoryTheory.Limits.BinaryBiconeMorphism A B) {Z : C} (h : P ⟶ Z) : CategoryTheory.CategoryStruct.comp self.hom (CategoryTheory.CategoryStruct.comp B.fst h) = CategoryTheory.CategoryStruct.comp A.fst h
• CategoryTheory.Limits.BinaryBiconeMorphism.winl_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {P Q : C} {A B : CategoryTheory.Limits.BinaryBicone P Q} (self : CategoryTheory.Limits.BinaryBiconeMorphism A B) {Z : C} (h : B.pt ⟶ Z) : CategoryTheory.CategoryStruct.comp A.inl (CategoryTheory.CategoryStruct.comp self.hom h) = CategoryTheory.CategoryStruct.comp B.inl h
• CategoryTheory.Limits.BinaryBiconeMorphism.winr_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {P Q : C} {A B : CategoryTheory.Limits.BinaryBicone P Q} (self : CategoryTheory.Limits.BinaryBiconeMorphism A B) {Z : C} (h : B.pt ⟶ Z) : CategoryTheory.CategoryStruct.comp A.inr (CategoryTheory.CategoryStruct.comp self.hom h) = CategoryTheory.CategoryStruct.comp B.inr h
• CategoryTheory.Limits.BinaryBiconeMorphism.wsnd_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {P Q : C} {A B : CategoryTheory.Limits.BinaryBicone P Q} (self : CategoryTheory.Limits.BinaryBiconeMorphism A B) {Z : C} (h : Q ⟶ Z) : CategoryTheory.CategoryStruct.comp self.hom (CategoryTheory.CategoryStruct.comp B.snd h) = CategoryTheory.CategoryStruct.comp A.snd h
• CategoryTheory.Limits.BinaryBicones.functoriality_obj_pt 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {D : Type uD} [CategoryTheory.Category.{uD', uD} D] [CategoryTheory.Limits.HasZeroMorphisms D] (P Q : C) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] (A : CategoryTheory.Limits.BinaryBicone P Q) : ((CategoryTheory.Limits.BinaryBicones.functoriality P Q F).obj A).pt = F.obj A.pt
• CategoryTheory.Limits.BinaryBicone.category_comp_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {P Q : C} {X✝ Y✝ Z✝ : CategoryTheory.Limits.BinaryBicone P Q} (f : CategoryTheory.Limits.BinaryBiconeMorphism X✝ Y✝) (g : CategoryTheory.Limits.BinaryBiconeMorphism Y✝ Z✝) : (CategoryTheory.CategoryStruct.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom
• CategoryTheory.Limits.BinaryBiconeMorphism.ext 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {P Q : C} {c c' : CategoryTheory.Limits.BinaryBicone P Q} (f g : c ⟶ c') (w : f.hom = g.hom) : f = g
• CategoryTheory.Limits.BinaryBiconeMorphism.ext_iff 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {P Q : C} {c c' : CategoryTheory.Limits.BinaryBicone P Q} {f g : c ⟶ c'} : f = g ↔ f.hom = g.hom
• CategoryTheory.Limits.BinaryBicones.functoriality_obj_fst 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {D : Type uD} [CategoryTheory.Category.{uD', uD} D] [CategoryTheory.Limits.HasZeroMorphisms D] (P Q : C) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] (A : CategoryTheory.Limits.BinaryBicone P Q) : ((CategoryTheory.Limits.BinaryBicones.functoriality P Q F).obj A).fst = F.map A.fst
• CategoryTheory.Limits.BinaryBicones.functoriality_obj_inl 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {D : Type uD} [CategoryTheory.Category.{uD', uD} D] [CategoryTheory.Limits.HasZeroMorphisms D] (P Q : C) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] (A : CategoryTheory.Limits.BinaryBicone P Q) : ((CategoryTheory.Limits.BinaryBicones.functoriality P Q F).obj A).inl = F.map A.inl
• CategoryTheory.Limits.BinaryBicones.functoriality_obj_inr 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {D : Type uD} [CategoryTheory.Category.{uD', uD} D] [CategoryTheory.Limits.HasZeroMorphisms D] (P Q : C) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] (A : CategoryTheory.Limits.BinaryBicone P Q) : ((CategoryTheory.Limits.BinaryBicones.functoriality P Q F).obj A).inr = F.map A.inr
• CategoryTheory.Limits.BinaryBicones.functoriality_obj_snd 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {D : Type uD} [CategoryTheory.Category.{uD', uD} D] [CategoryTheory.Limits.HasZeroMorphisms D] (P Q : C) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] (A : CategoryTheory.Limits.BinaryBicone P Q) : ((CategoryTheory.Limits.BinaryBicones.functoriality P Q F).obj A).snd = F.map A.snd
• CategoryTheory.Limits.BinaryBicone.fstKernelFork_ι 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (c : CategoryTheory.Limits.BinaryBicone X Y) : CategoryTheory.Limits.Fork.ι c.fstKernelFork = c.inr
• CategoryTheory.Limits.BinaryBicone.inlCokernelCofork_π 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (c : CategoryTheory.Limits.BinaryBicone X Y) : CategoryTheory.Limits.Cofork.π c.inlCokernelCofork = c.snd
• CategoryTheory.Limits.BinaryBicone.inrCokernelCofork_π 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (c : CategoryTheory.Limits.BinaryBicone X Y) : CategoryTheory.Limits.Cofork.π c.inrCokernelCofork = c.fst
• CategoryTheory.Limits.BinaryBicone.sndKernelFork_ι 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (c : CategoryTheory.Limits.BinaryBicone X Y) : CategoryTheory.Limits.Fork.ι c.sndKernelFork = c.inl
• CategoryTheory.Limits.biprod.conePointUniqueUpToIso_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C) [CategoryTheory.Limits.HasBinaryBiproduct X Y] {b : CategoryTheory.Limits.BinaryBicone X Y} (hb : b.IsBilimit) : (hb.isLimit.conePointUniqueUpToIso (CategoryTheory.Limits.BinaryBiproduct.isLimit X Y)).hom = CategoryTheory.Limits.biprod.lift b.fst b.snd
• CategoryTheory.Limits.biprod.conePointUniqueUpToIso_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C) [CategoryTheory.Limits.HasBinaryBiproduct X Y] {b : CategoryTheory.Limits.BinaryBicone X Y} (hb : b.IsBilimit) : (hb.isLimit.conePointUniqueUpToIso (CategoryTheory.Limits.BinaryBiproduct.isLimit X Y)).inv = CategoryTheory.Limits.biprod.desc b.inl b.inr
• CategoryTheory.Limits.BinaryBiconeMorphism.mk 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {P Q : C} {A B : CategoryTheory.Limits.BinaryBicone P Q} (hom : A.pt ⟶ B.pt) (wfst : CategoryTheory.CategoryStruct.comp hom B.fst = A.fst := by cat_disch) (wsnd : CategoryTheory.CategoryStruct.comp hom B.snd = A.snd := by cat_disch) (winl : CategoryTheory.CategoryStruct.comp A.inl hom = B.inl := by cat_disch) (winr : CategoryTheory.CategoryStruct.comp A.inr hom = B.inr := by cat_disch) : CategoryTheory.Limits.BinaryBiconeMorphism A B
• CategoryTheory.Limits.BinaryBicone.toBiconeFunctor_map_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} {X✝ Y✝ : CategoryTheory.Limits.BinaryBicone X Y} (f : X✝ ⟶ Y✝) : (CategoryTheory.Limits.BinaryBicone.toBiconeFunctor.map f).hom = f.hom
• CategoryTheory.Limits.BinaryBicones.ext 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {P Q : C} {c c' : CategoryTheory.Limits.BinaryBicone P Q} (φ : c.pt ≅ c'.pt) (winl : CategoryTheory.CategoryStruct.comp c.inl φ.hom = c'.inl := by cat_disch) (winr : CategoryTheory.CategoryStruct.comp c.inr φ.hom = c'.inr := by cat_disch) (wfst : CategoryTheory.CategoryStruct.comp φ.hom c'.fst = c.fst := by cat_disch) (wsnd : CategoryTheory.CategoryStruct.comp φ.hom c'.snd = c.snd := by cat_disch) : c ≅ c'
• CategoryTheory.Limits.BinaryBicones.ext_hom_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {P Q : C} {c c' : CategoryTheory.Limits.BinaryBicone P Q} (φ : c.pt ≅ c'.pt) (winl : CategoryTheory.CategoryStruct.comp c.inl φ.hom = c'.inl := by cat_disch) (winr : CategoryTheory.CategoryStruct.comp c.inr φ.hom = c'.inr := by cat_disch) (wfst : CategoryTheory.CategoryStruct.comp φ.hom c'.fst = c.fst := by cat_disch) (wsnd : CategoryTheory.CategoryStruct.comp φ.hom c'.snd = c.snd := by cat_disch) : (CategoryTheory.Limits.BinaryBicones.ext φ winl winr wfst wsnd).hom.hom = φ.hom
• CategoryTheory.Limits.BinaryBicones.ext_inv_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {P Q : C} {c c' : CategoryTheory.Limits.BinaryBicone P Q} (φ : c.pt ≅ c'.pt) (winl : CategoryTheory.CategoryStruct.comp c.inl φ.hom = c'.inl := by cat_disch) (winr : CategoryTheory.CategoryStruct.comp c.inr φ.hom = c'.inr := by cat_disch) (wfst : CategoryTheory.CategoryStruct.comp φ.hom c'.fst = c.fst := by cat_disch) (wsnd : CategoryTheory.CategoryStruct.comp φ.hom c'.snd = c.snd := by cat_disch) : (CategoryTheory.Limits.BinaryBicones.ext φ winl winr wfst wsnd).inv.hom = φ.inv
• CategoryTheory.Limits.BinaryBicones.functoriality_map_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {D : Type uD} [CategoryTheory.Category.{uD', uD} D] [CategoryTheory.Limits.HasZeroMorphisms D] (P Q : C) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] {X✝ Y✝ : CategoryTheory.Limits.BinaryBicone P Q} (f : X✝ ⟶ Y✝) : ((CategoryTheory.Limits.BinaryBicones.functoriality P Q F).map f).hom = F.map f.hom
• CategoryTheory.Functor.mapBinaryBicone_pt 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] {X Y : C} (b : CategoryTheory.Limits.BinaryBicone X Y) : (F.mapBinaryBicone b).pt = F.obj b.pt
• CategoryTheory.Functor.mapBinaryBicone_fst 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] {X Y : C} (b : CategoryTheory.Limits.BinaryBicone X Y) : (F.mapBinaryBicone b).fst = F.map b.fst
• CategoryTheory.Functor.mapBinaryBicone_inl 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] {X Y : C} (b : CategoryTheory.Limits.BinaryBicone X Y) : (F.mapBinaryBicone b).inl = F.map b.inl
• CategoryTheory.Functor.mapBinaryBicone_inr 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] {X Y : C} (b : CategoryTheory.Limits.BinaryBicone X Y) : (F.mapBinaryBicone b).inr = F.map b.inr
• CategoryTheory.Functor.mapBinaryBicone_snd 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] {X Y : C} (b : CategoryTheory.Limits.BinaryBicone X Y) : (F.mapBinaryBicone b).snd = F.map b.snd
• CategoryTheory.Limits.BinaryBicone.ofColimitCocone_pt 📋 Mathlib.CategoryTheory.Preadditive.Biproducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} {t : CategoryTheory.Limits.Cocone (CategoryTheory.Limits.pair X Y)} (ht : CategoryTheory.Limits.IsColimit t) : (CategoryTheory.Limits.BinaryBicone.ofColimitCocone ht).pt = t.pt
• CategoryTheory.Limits.BinaryBicone.ofLimitCone_pt 📋 Mathlib.CategoryTheory.Preadditive.Biproducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} {t : CategoryTheory.Limits.Cone (CategoryTheory.Limits.pair X Y)} (ht : CategoryTheory.Limits.IsLimit t) : (CategoryTheory.Limits.BinaryBicone.ofLimitCone ht).pt = t.pt
• CategoryTheory.Limits.fst_of_isColimit 📋 Mathlib.CategoryTheory.Preadditive.Biproducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} {t : CategoryTheory.Limits.BinaryBicone X Y} (ht : CategoryTheory.Limits.IsColimit t.toCocone) : t.fst = CategoryTheory.Limits.BinaryCofan.IsColimit.desc ht (CategoryTheory.CategoryStruct.id X) 0
• CategoryTheory.Limits.inl_of_isLimit 📋 Mathlib.CategoryTheory.Preadditive.Biproducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} {t : CategoryTheory.Limits.BinaryBicone X Y} (ht : CategoryTheory.Limits.IsLimit t.toCone) : t.inl = CategoryTheory.Limits.BinaryFan.IsLimit.lift ht (CategoryTheory.CategoryStruct.id X) 0
• CategoryTheory.Limits.inr_of_isLimit 📋 Mathlib.CategoryTheory.Preadditive.Biproducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} {t : CategoryTheory.Limits.BinaryBicone X Y} (ht : CategoryTheory.Limits.IsLimit t.toCone) : t.inr = CategoryTheory.Limits.BinaryFan.IsLimit.lift ht 0 (CategoryTheory.CategoryStruct.id Y)
• CategoryTheory.Limits.snd_of_isColimit 📋 Mathlib.CategoryTheory.Preadditive.Biproducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} {t : CategoryTheory.Limits.BinaryBicone X Y} (ht : CategoryTheory.Limits.IsColimit t.toCocone) : t.snd = CategoryTheory.Limits.BinaryCofan.IsColimit.desc ht 0 (CategoryTheory.CategoryStruct.id Y)
• CategoryTheory.Limits.BinaryBicone.isBilimitOfCokernelFst 📋 Mathlib.CategoryTheory.Preadditive.Biproducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} (b : CategoryTheory.Limits.BinaryBicone X Y) (hb : CategoryTheory.Limits.IsColimit b.inrCokernelCofork) : b.IsBilimit
• CategoryTheory.Limits.BinaryBicone.isBilimitOfCokernelSnd 📋 Mathlib.CategoryTheory.Preadditive.Biproducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} (b : CategoryTheory.Limits.BinaryBicone X Y) (hb : CategoryTheory.Limits.IsColimit b.inlCokernelCofork) : b.IsBilimit
• CategoryTheory.Limits.BinaryBicone.isBilimitOfKernelInl 📋 Mathlib.CategoryTheory.Preadditive.Biproducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} (b : CategoryTheory.Limits.BinaryBicone X Y) (hb : CategoryTheory.Limits.IsLimit b.sndKernelFork) : b.IsBilimit
• CategoryTheory.Limits.BinaryBicone.isBilimitOfKernelInr 📋 Mathlib.CategoryTheory.Preadditive.Biproducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} (b : CategoryTheory.Limits.BinaryBicone X Y) (hb : CategoryTheory.Limits.IsLimit b.fstKernelFork) : b.IsBilimit
• CategoryTheory.Limits.binaryBiconeOfIsSplitEpiOfKernel_pt 📋 Mathlib.CategoryTheory.Preadditive.Biproducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} {f : X ⟶ Y} [CategoryTheory.IsSplitEpi f] {c : CategoryTheory.Limits.KernelFork f} (i : CategoryTheory.Limits.IsLimit c) : (CategoryTheory.Limits.binaryBiconeOfIsSplitEpiOfKernel i).pt = X
• CategoryTheory.Limits.binaryBiconeOfIsSplitMonoOfCokernel_pt 📋 Mathlib.CategoryTheory.Preadditive.Biproducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} {f : X ⟶ Y} [CategoryTheory.IsSplitMono f] {c : CategoryTheory.Limits.CokernelCofork f} (i : CategoryTheory.Limits.IsColimit c) : (CategoryTheory.Limits.binaryBiconeOfIsSplitMonoOfCokernel i).pt = Y
• CategoryTheory.Limits.hasBinaryBiproduct_of_total 📋 Mathlib.CategoryTheory.Preadditive.Biproducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} (b : CategoryTheory.Limits.BinaryBicone X Y) (total : CategoryTheory.CategoryStruct.comp b.fst b.inl + CategoryTheory.CategoryStruct.comp b.snd b.inr = CategoryTheory.CategoryStruct.id b.pt) : CategoryTheory.Limits.HasBinaryBiproduct X Y
• CategoryTheory.Limits.isBinaryBilimitOfTotal 📋 Mathlib.CategoryTheory.Preadditive.Biproducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} (b : CategoryTheory.Limits.BinaryBicone X Y) (total : CategoryTheory.CategoryStruct.comp b.fst b.inl + CategoryTheory.CategoryStruct.comp b.snd b.inr = CategoryTheory.CategoryStruct.id b.pt) : b.IsBilimit
• CategoryTheory.Limits.IsBilimit.binary_total 📋 Mathlib.CategoryTheory.Preadditive.Biproducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} {b : CategoryTheory.Limits.BinaryBicone X Y} (i : b.IsBilimit) : CategoryTheory.CategoryStruct.comp b.fst b.inl + CategoryTheory.CategoryStruct.comp b.snd b.inr = CategoryTheory.CategoryStruct.id b.pt
• CategoryTheory.ObjectProperty.IsStableUnderRetracts.of_binaryBicone_left 📋 Mathlib.CategoryTheory.ObjectProperty.Retract
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) [P.IsStableUnderRetracts] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (c : CategoryTheory.Limits.BinaryBicone X Y) (h : P c.pt) : P X
• CategoryTheory.ObjectProperty.IsStableUnderRetracts.of_binaryBicone_right 📋 Mathlib.CategoryTheory.ObjectProperty.Retract
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) [P.IsStableUnderRetracts] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (c : CategoryTheory.Limits.BinaryBicone X Y) (h : P c.pt) : P Y
• CategoryTheory.Pretriangulated.binaryBiproductData_bicone_pt 📋 Mathlib.CategoryTheory.Triangulated.Pretriangulated
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C] (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (hT₀ : T.mor₃ = 0) (inr : T.obj₃ ⟶ T.obj₂) (inr_snd : CategoryTheory.CategoryStruct.comp inr T.mor₂ = CategoryTheory.CategoryStruct.id T.obj₃) (fst : T.obj₂ ⟶ T.obj₁) (total : CategoryTheory.CategoryStruct.comp fst T.mor₁ + CategoryTheory.CategoryStruct.comp T.mor₂ inr = CategoryTheory.CategoryStruct.id T.obj₂) : (CategoryTheory.Pretriangulated.binaryBiproductData T hT hT₀ inr inr_snd fst total).bicone.pt = T.obj₂
• CategoryTheory.Limits.pointwiseBinaryBicone_pt_obj 📋 Mathlib.CategoryTheory.Limits.FunctorCategory.BinaryBiproducts
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] (F G : CategoryTheory.Functor D C) (P : D) : (CategoryTheory.Limits.pointwiseBinaryBicone F G).pt.obj P = (F.obj P ⊞ G.obj P)
• CategoryTheory.Limits.pointwiseBinaryBicone_pt_map 📋 Mathlib.CategoryTheory.Limits.FunctorCategory.BinaryBiproducts
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] (F G : CategoryTheory.Functor D C) {X✝ Y✝ : D} (f : X✝ ⟶ Y✝) : (CategoryTheory.Limits.pointwiseBinaryBicone F G).pt.map f = CategoryTheory.Limits.biprod.map (F.map f) (G.map f)
• CategoryTheory.BicartesianSq.of_is_biproduct₁ 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} {b : CategoryTheory.Limits.BinaryBicone X Y} (h : b.IsBilimit) : CategoryTheory.BicartesianSq b.fst b.snd 0 0
• CategoryTheory.BicartesianSq.of_is_biproduct₂ 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} {b : CategoryTheory.Limits.BinaryBicone X Y} (h : b.IsBilimit) : CategoryTheory.BicartesianSq 0 0 b.inl b.inr
• CategoryTheory.IsPullback.inl_snd' 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} {b : CategoryTheory.Limits.BinaryBicone X Y} (h : b.IsBilimit) : CategoryTheory.IsPullback b.inl 0 b.snd 0
• CategoryTheory.IsPullback.inr_fst' 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} {b : CategoryTheory.Limits.BinaryBicone X Y} (h : b.IsBilimit) : CategoryTheory.IsPullback b.inr 0 b.fst 0
• CategoryTheory.IsPullback.of_isBilimit 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} {b : CategoryTheory.Limits.BinaryBicone X Y} (h : b.IsBilimit) : CategoryTheory.IsPullback b.fst b.snd 0 0
• CategoryTheory.IsPullback.of_is_bilimit' 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} {b : CategoryTheory.Limits.BinaryBicone X Y} (h : b.IsBilimit) : CategoryTheory.IsPullback 0 0 b.inl b.inr
• CategoryTheory.IsPushout.inl_snd' 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} {b : CategoryTheory.Limits.BinaryBicone X Y} (h : b.IsBilimit) : CategoryTheory.IsPushout b.inl 0 b.snd 0
• CategoryTheory.IsPushout.inr_fst' 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} {b : CategoryTheory.Limits.BinaryBicone X Y} (h : b.IsBilimit) : CategoryTheory.IsPushout b.inr 0 b.fst 0
• CategoryTheory.IsPushout.of_isBilimit 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} {b : CategoryTheory.Limits.BinaryBicone X Y} (h : b.IsBilimit) : CategoryTheory.IsPushout 0 0 b.inl b.inr
• CategoryTheory.IsPushout.of_is_bilimit' 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} {b : CategoryTheory.Limits.BinaryBicone X Y} (h : b.IsBilimit) : CategoryTheory.IsPushout b.fst b.snd 0 0

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision ce5dd8c