Loogle!

Result

Found 107 declarations mentioning CategoryTheory.Limits.Bicone.

• CategoryTheory.Limits.Bicone 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] (F : J → C) : Type (max (max uC uC') w)
• CategoryTheory.Limits.Bicone.IsBilimit 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} (B : CategoryTheory.Limits.Bicone F) : Type (max (max uC uC') w)
• CategoryTheory.Limits.Bicone.category 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} : CategoryTheory.Category.{uC', max (max uC uC') w} (CategoryTheory.Limits.Bicone F)
• CategoryTheory.Limits.Bicone.pt 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} (self : CategoryTheory.Limits.Bicone F) : C
• CategoryTheory.Limits.LimitBicone.bicone 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} (self : CategoryTheory.Limits.LimitBicone F) : CategoryTheory.Limits.Bicone F
• CategoryTheory.Limits.biproduct.bicone 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] (F : J → C) [CategoryTheory.Limits.HasBiproduct F] : CategoryTheory.Limits.Bicone F
• CategoryTheory.Limits.BiconeMorphism 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} (A B : CategoryTheory.Limits.Bicone F) : Type uC'
• CategoryTheory.Limits.Bicone.subsingleton_isBilimit 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {f : J → C} {c : CategoryTheory.Limits.Bicone f} : Subsingleton c.IsBilimit
• CategoryTheory.Limits.Bicone.toCocone 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} (B : CategoryTheory.Limits.Bicone F) : CategoryTheory.Limits.Cocone (CategoryTheory.Discrete.functor F)
• CategoryTheory.Limits.Bicone.toCone 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} (B : CategoryTheory.Limits.Bicone F) : CategoryTheory.Limits.Cone (CategoryTheory.Discrete.functor F)
• CategoryTheory.Limits.Bicone.retract 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} (B : CategoryTheory.Limits.Bicone F) (j : J) : CategoryTheory.Retract (F j) B.pt
• CategoryTheory.Limits.LimitBicone.mk 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} (bicone : CategoryTheory.Limits.Bicone F) (isBilimit : bicone.IsBilimit) : CategoryTheory.Limits.LimitBicone F
• CategoryTheory.Limits.Bicone.ι 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} (self : CategoryTheory.Limits.Bicone F) (j : J) : F j ⟶ self.pt
• CategoryTheory.Limits.Bicone.π 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} (self : CategoryTheory.Limits.Bicone F) (j : J) : self.pt ⟶ F j
• CategoryTheory.Limits.Bicone.instIsSplitEpiπ 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} (B : CategoryTheory.Limits.Bicone F) (j : J) : CategoryTheory.IsSplitEpi (B.π j)
• CategoryTheory.Limits.Bicone.instIsSplitMonoι 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} (B : CategoryTheory.Limits.Bicone F) (j : J) : CategoryTheory.IsSplitMono (B.ι j)
• CategoryTheory.Limits.Bicone.ofColimitCocone 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {f : J → C} {t : CategoryTheory.Limits.Cocone (CategoryTheory.Discrete.functor f)} (ht : CategoryTheory.Limits.IsColimit t) : CategoryTheory.Limits.Bicone f
• CategoryTheory.Limits.Bicone.ofLimitCone 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {f : J → C} {t : CategoryTheory.Limits.Cone (CategoryTheory.Discrete.functor f)} (ht : CategoryTheory.Limits.IsLimit t) : CategoryTheory.Limits.Bicone f
• CategoryTheory.Limits.Bicone.IsBilimit.isColimit 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} {B : CategoryTheory.Limits.Bicone F} (self : B.IsBilimit) : CategoryTheory.Limits.IsColimit B.toCocone
• CategoryTheory.Limits.Bicone.IsBilimit.isLimit 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} {B : CategoryTheory.Limits.Bicone F} (self : B.IsBilimit) : CategoryTheory.Limits.IsLimit B.toCone
• CategoryTheory.Limits.Bicone.toCocone_pt 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} (B : CategoryTheory.Limits.Bicone F) : B.toCocone.pt = B.pt
• CategoryTheory.Limits.Bicone.toCone_pt 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} (B : CategoryTheory.Limits.Bicone F) : B.toCone.pt = B.pt
• CategoryTheory.Limits.biproduct.uniqueUpToIso 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [CategoryTheory.Limits.HasBiproduct f] {b : CategoryTheory.Limits.Bicone f} (hb : b.IsBilimit) : b.pt ≅ ⨁ f
• CategoryTheory.Limits.Bicone.toCoconeFunctor 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} : CategoryTheory.Functor (CategoryTheory.Limits.Bicone F) (CategoryTheory.Limits.Cocone (CategoryTheory.Discrete.functor F))
• CategoryTheory.Limits.Bicone.toConeFunctor 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} : CategoryTheory.Functor (CategoryTheory.Limits.Bicone F) (CategoryTheory.Limits.Cone (CategoryTheory.Discrete.functor F))
• CategoryTheory.Limits.Bicone.whisker 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : Type w'} {f : J → C} (c : CategoryTheory.Limits.Bicone f) (g : K ≃ J) : CategoryTheory.Limits.Bicone (f ∘ ⇑g)
• CategoryTheory.Limits.BiconeMorphism.hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} {A B : CategoryTheory.Limits.Bicone F} (self : CategoryTheory.Limits.BiconeMorphism A B) : A.pt ⟶ B.pt
• CategoryTheory.Limits.Bicone.IsBilimit.mk 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} {B : CategoryTheory.Limits.Bicone F} (isLimit : CategoryTheory.Limits.IsLimit B.toCone) (isColimit : CategoryTheory.Limits.IsColimit B.toCocone) : B.IsBilimit
• CategoryTheory.Limits.Bicone.whiskerIsBilimitIff 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : Type w'} {f : J → C} (c : CategoryTheory.Limits.Bicone f) (g : K ≃ J) : (c.whisker g).IsBilimit ≃ c.IsBilimit
• CategoryTheory.Limits.Bicone.whisker_pt 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : Type w'} {f : J → C} (c : CategoryTheory.Limits.Bicone f) (g : K ≃ J) : (c.whisker g).pt = c.pt
• CategoryTheory.Limits.Bicone.toCocone_inj 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} (B : CategoryTheory.Limits.Bicone F) (j : J) : CategoryTheory.Limits.Cofan.inj B.toCocone j = B.ι j
• CategoryTheory.Limits.Bicone.toCone_proj 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} (B : CategoryTheory.Limits.Bicone F) (j : J) : CategoryTheory.Limits.Fan.proj B.toCone j = B.π j
• CategoryTheory.Limits.bicone_ι_π_self 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} (B : CategoryTheory.Limits.Bicone F) (j : J) : CategoryTheory.CategoryStruct.comp (B.ι j) (B.π j) = CategoryTheory.CategoryStruct.id (F j)
• CategoryTheory.Limits.Bicones.functoriality 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {D : Type uD} [CategoryTheory.Category.{uD', uD} D] [CategoryTheory.Limits.HasZeroMorphisms D] (F : J → C) (G : CategoryTheory.Functor C D) [G.PreservesZeroMorphisms] : CategoryTheory.Functor (CategoryTheory.Limits.Bicone F) (CategoryTheory.Limits.Bicone (G.obj ∘ F))
• CategoryTheory.Limits.Bicone.category_id_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} (B : CategoryTheory.Limits.Bicone F) : (CategoryTheory.CategoryStruct.id B).hom = CategoryTheory.CategoryStruct.id B.pt
• CategoryTheory.Limits.bicone_ι_π_self_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} (B : CategoryTheory.Limits.Bicone F) (j : J) {Z : C} (h : F j ⟶ Z) : CategoryTheory.CategoryStruct.comp (B.ι j) (CategoryTheory.CategoryStruct.comp (B.π j) h) = h
• CategoryTheory.Limits.Bicones.functoriality_faithful 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {D : Type uD} [CategoryTheory.Category.{uD', uD} D] [CategoryTheory.Limits.HasZeroMorphisms D] {F : J → C} (G : CategoryTheory.Functor C D) [G.PreservesZeroMorphisms] [G.Faithful] : (CategoryTheory.Limits.Bicones.functoriality F G).Faithful
• CategoryTheory.Limits.BiconeMorphism.wι 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} {A B : CategoryTheory.Limits.Bicone F} (self : CategoryTheory.Limits.BiconeMorphism A B) (j : J) : CategoryTheory.CategoryStruct.comp (A.ι j) self.hom = B.ι j
• CategoryTheory.Limits.BiconeMorphism.wπ 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} {A B : CategoryTheory.Limits.Bicone F} (self : CategoryTheory.Limits.BiconeMorphism A B) (j : J) : CategoryTheory.CategoryStruct.comp self.hom (B.π j) = A.π j
• CategoryTheory.Limits.Bicones.functoriality_full 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {D : Type uD} [CategoryTheory.Category.{uD', uD} D] [CategoryTheory.Limits.HasZeroMorphisms D] {F : J → C} (G : CategoryTheory.Functor C D) [G.PreservesZeroMorphisms] [G.Full] [G.Faithful] : (CategoryTheory.Limits.Bicones.functoriality F G).Full
• CategoryTheory.Limits.biproduct.uniqueUpToIso_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [CategoryTheory.Limits.HasBiproduct f] {b : CategoryTheory.Limits.Bicone f} (hb : b.IsBilimit) : (CategoryTheory.Limits.biproduct.uniqueUpToIso f hb).hom = CategoryTheory.Limits.biproduct.lift b.π
• CategoryTheory.Limits.biproduct.uniqueUpToIso_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [CategoryTheory.Limits.HasBiproduct f] {b : CategoryTheory.Limits.Bicone f} (hb : b.IsBilimit) : (CategoryTheory.Limits.biproduct.uniqueUpToIso f hb).inv = CategoryTheory.Limits.biproduct.desc b.ι
• CategoryTheory.Limits.bicone_ι_π_ne 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} (B : CategoryTheory.Limits.Bicone F) {j j' : J} (h : j ≠ j') : CategoryTheory.CategoryStruct.comp (B.ι j) (B.π j') = 0
• CategoryTheory.Limits.Bicone.IsBilimit.ext 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} {inst✝ : CategoryTheory.Category.{uC', uC} C} {inst✝¹ : CategoryTheory.Limits.HasZeroMorphisms C} {F : J → C} {B : CategoryTheory.Limits.Bicone F} {x y : B.IsBilimit} (isLimit : x.isLimit = y.isLimit) (isColimit : x.isColimit = y.isColimit) : x = y
• CategoryTheory.Limits.Bicone.IsBilimit.ext_iff 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} {inst✝ : CategoryTheory.Category.{uC', uC} C} {inst✝¹ : CategoryTheory.Limits.HasZeroMorphisms C} {F : J → C} {B : CategoryTheory.Limits.Bicone F} {x y : B.IsBilimit} : x = y ↔ x.isLimit = y.isLimit ∧ x.isColimit = y.isColimit
• CategoryTheory.Limits.Bicone.whisker_ι 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : Type w'} {f : J → C} (c : CategoryTheory.Limits.Bicone f) (g : K ≃ J) (k : K) : (c.whisker g).ι k = c.ι (g k)
• CategoryTheory.Limits.Bicone.whisker_π 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : Type w'} {f : J → C} (c : CategoryTheory.Limits.Bicone f) (g : K ≃ J) (k : K) : (c.whisker g).π k = c.π (g k)
• CategoryTheory.Limits.Bicones.functoriality_obj_pt 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {D : Type uD} [CategoryTheory.Category.{uD', uD} D] [CategoryTheory.Limits.HasZeroMorphisms D] (F : J → C) (G : CategoryTheory.Functor C D) [G.PreservesZeroMorphisms] (A : CategoryTheory.Limits.Bicone F) : ((CategoryTheory.Limits.Bicones.functoriality F G).obj A).pt = G.obj A.pt
• CategoryTheory.Limits.bicone_ι_π_ne_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} (B : CategoryTheory.Limits.Bicone F) {j j' : J} (h : j ≠ j') {Z : C} (h✝ : F j' ⟶ Z) : CategoryTheory.CategoryStruct.comp (B.ι j) (CategoryTheory.CategoryStruct.comp (B.π j') h✝) = CategoryTheory.CategoryStruct.comp 0 h✝
• CategoryTheory.Limits.BiconeMorphism.wι_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} {A B : CategoryTheory.Limits.Bicone F} (self : CategoryTheory.Limits.BiconeMorphism A B) (j : J) {Z : C} (h : B.pt ⟶ Z) : CategoryTheory.CategoryStruct.comp (A.ι j) (CategoryTheory.CategoryStruct.comp self.hom h) = CategoryTheory.CategoryStruct.comp (B.ι j) h
• CategoryTheory.Limits.BiconeMorphism.wπ_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} {A B : CategoryTheory.Limits.Bicone F} (self : CategoryTheory.Limits.BiconeMorphism A B) (j : J) {Z : C} (h : F j ⟶ Z) : CategoryTheory.CategoryStruct.comp self.hom (CategoryTheory.CategoryStruct.comp (B.π j) h) = CategoryTheory.CategoryStruct.comp (A.π j) h
• CategoryTheory.Limits.Bicone.ι_π 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} (self : CategoryTheory.Limits.Bicone F) (j j' : J) : CategoryTheory.CategoryStruct.comp (self.ι j) (self.π j') = if h : j = j' then CategoryTheory.eqToHom ⋯ else 0
• CategoryTheory.Limits.Bicone.category_comp_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} {X✝ Y✝ Z✝ : CategoryTheory.Limits.Bicone F} (f : CategoryTheory.Limits.BiconeMorphism X✝ Y✝) (g : CategoryTheory.Limits.BiconeMorphism Y✝ Z✝) : (CategoryTheory.CategoryStruct.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom
• CategoryTheory.Limits.Bicone.mk 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} (pt : C) (π : (j : J) → pt ⟶ F j) (ι : (j : J) → F j ⟶ pt) (ι_π : ∀ (j j' : J), CategoryTheory.CategoryStruct.comp (ι j) (π j') = if h : j = j' then CategoryTheory.eqToHom ⋯ else 0 := by aesop) : CategoryTheory.Limits.Bicone F
• CategoryTheory.Limits.BiconeMorphism.ext 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} {c c' : CategoryTheory.Limits.Bicone F} (f g : c ⟶ c') (w : f.hom = g.hom) : f = g
• CategoryTheory.Limits.BiconeMorphism.ext_iff 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} {c c' : CategoryTheory.Limits.Bicone F} {f g : c ⟶ c'} : f = g ↔ f.hom = g.hom
• CategoryTheory.Limits.Bicones.functoriality_obj_ι 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {D : Type uD} [CategoryTheory.Category.{uD', uD} D] [CategoryTheory.Limits.HasZeroMorphisms D] (F : J → C) (G : CategoryTheory.Functor C D) [G.PreservesZeroMorphisms] (A : CategoryTheory.Limits.Bicone F) (j : J) : ((CategoryTheory.Limits.Bicones.functoriality F G).obj A).ι j = G.map (A.ι j)
• CategoryTheory.Limits.Bicones.functoriality_obj_π 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {D : Type uD} [CategoryTheory.Category.{uD', uD} D] [CategoryTheory.Limits.HasZeroMorphisms D] (F : J → C) (G : CategoryTheory.Functor C D) [G.PreservesZeroMorphisms] (A : CategoryTheory.Limits.Bicone F) (j : J) : ((CategoryTheory.Limits.Bicones.functoriality F G).obj A).π j = G.map (A.π j)
• CategoryTheory.Limits.BiconeMorphism.mk 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} {A B : CategoryTheory.Limits.Bicone F} (hom : A.pt ⟶ B.pt) (wπ : ∀ (j : J), CategoryTheory.CategoryStruct.comp hom (B.π j) = A.π j := by cat_disch) (wι : ∀ (j : J), CategoryTheory.CategoryStruct.comp (A.ι j) hom = B.ι j := by cat_disch) : CategoryTheory.Limits.BiconeMorphism A B
• CategoryTheory.Limits.Bicone.ι_of_isLimit 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {f : J → C} {t : CategoryTheory.Limits.Bicone f} (ht : CategoryTheory.Limits.IsLimit t.toCone) (j : J) : t.ι j = ht.lift (CategoryTheory.Limits.Fan.mk (f j) fun j' => if h : j = j' then CategoryTheory.eqToHom ⋯ else 0)
• CategoryTheory.Limits.Bicone.π_of_isColimit 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {f : J → C} {t : CategoryTheory.Limits.Bicone f} (ht : CategoryTheory.Limits.IsColimit t.toCocone) (j : J) : t.π j = ht.desc (CategoryTheory.Limits.Cofan.mk (f j) fun j' => if h : j' = j then CategoryTheory.eqToHom ⋯ else 0)
• CategoryTheory.Limits.Bicone.toCocone_ι_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} (B : CategoryTheory.Limits.Bicone F) (j : CategoryTheory.Discrete J) : B.toCocone.ι.app j = B.ι j.as
• CategoryTheory.Limits.Bicone.toCone_π_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} (B : CategoryTheory.Limits.Bicone F) (j : CategoryTheory.Discrete J) : B.toCone.π.app j = B.π j.as
• CategoryTheory.Limits.Bicone.toCocone_ι_app_mk 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} (B : CategoryTheory.Limits.Bicone F) (j : J) : B.toCocone.ι.app { as := j } = B.ι j
• CategoryTheory.Limits.Bicone.toCone_π_app_mk 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} (B : CategoryTheory.Limits.Bicone F) (j : J) : B.toCone.π.app { as := j } = B.π j
• CategoryTheory.Limits.biproduct.conePointUniqueUpToIso_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [CategoryTheory.Limits.HasBiproduct f] {b : CategoryTheory.Limits.Bicone f} (hb : b.IsBilimit) : (hb.isLimit.conePointUniqueUpToIso (CategoryTheory.Limits.biproduct.isLimit f)).hom = CategoryTheory.Limits.biproduct.lift b.π
• CategoryTheory.Limits.biproduct.conePointUniqueUpToIso_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [CategoryTheory.Limits.HasBiproduct f] {b : CategoryTheory.Limits.Bicone f} (hb : b.IsBilimit) : (hb.isLimit.conePointUniqueUpToIso (CategoryTheory.Limits.biproduct.isLimit f)).inv = CategoryTheory.Limits.biproduct.desc b.ι
• CategoryTheory.Limits.Bicones.ext 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} {c c' : CategoryTheory.Limits.Bicone F} (φ : c.pt ≅ c'.pt) (wι : ∀ (j : J), CategoryTheory.CategoryStruct.comp (c.ι j) φ.hom = c'.ι j := by cat_disch) (wπ : ∀ (j : J), CategoryTheory.CategoryStruct.comp φ.hom (c'.π j) = c.π j := by cat_disch) : c ≅ c'
• CategoryTheory.Limits.Bicones.ext_hom_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} {c c' : CategoryTheory.Limits.Bicone F} (φ : c.pt ≅ c'.pt) (wι : ∀ (j : J), CategoryTheory.CategoryStruct.comp (c.ι j) φ.hom = c'.ι j := by cat_disch) (wπ : ∀ (j : J), CategoryTheory.CategoryStruct.comp φ.hom (c'.π j) = c.π j := by cat_disch) : (CategoryTheory.Limits.Bicones.ext φ wι wπ).hom.hom = φ.hom
• CategoryTheory.Limits.Bicones.ext_inv_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} {c c' : CategoryTheory.Limits.Bicone F} (φ : c.pt ≅ c'.pt) (wι : ∀ (j : J), CategoryTheory.CategoryStruct.comp (c.ι j) φ.hom = c'.ι j := by cat_disch) (wπ : ∀ (j : J), CategoryTheory.CategoryStruct.comp φ.hom (c'.π j) = c.π j := by cat_disch) : (CategoryTheory.Limits.Bicones.ext φ wι wπ).inv.hom = φ.inv
• CategoryTheory.Limits.Bicones.functoriality_map_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {D : Type uD} [CategoryTheory.Category.{uD', uD} D] [CategoryTheory.Limits.HasZeroMorphisms D] (F : J → C) (G : CategoryTheory.Functor C D) [G.PreservesZeroMorphisms] {X✝ Y✝ : CategoryTheory.Limits.Bicone F} (f : X✝ ⟶ Y✝) : ((CategoryTheory.Limits.Bicones.functoriality F G).map f).hom = G.map f.hom
• CategoryTheory.Limits.Bicone.whiskerToCocone 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : Type w'} {f : J → C} (c : CategoryTheory.Limits.Bicone f) (g : K ≃ J) : (c.whisker g).toCocone ≅ (CategoryTheory.Limits.Cocone.precompose (CategoryTheory.Discrete.functorComp f ⇑g).hom).obj (CategoryTheory.Limits.Cocone.whisker (CategoryTheory.Discrete.functor (CategoryTheory.Discrete.mk ∘ ⇑g)) c.toCocone)
• CategoryTheory.Limits.Bicone.whiskerToCone 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : Type w'} {f : J → C} (c : CategoryTheory.Limits.Bicone f) (g : K ≃ J) : (c.whisker g).toCone ≅ (CategoryTheory.Limits.Cone.postcompose (CategoryTheory.Discrete.functorComp f ⇑g).inv).obj (CategoryTheory.Limits.Cone.whisker (CategoryTheory.Discrete.functor (CategoryTheory.Discrete.mk ∘ ⇑g)) c.toCone)
• CategoryTheory.Limits.Bicone.toBinaryBicone 📋 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.BinaryBicone X Y
• CategoryTheory.Limits.BinaryBicone.toBicone 📋 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.Bicone (CategoryTheory.Limits.pairFunction X Y)
• CategoryTheory.Limits.Bicone.toBinaryBiconeFunctor 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} : CategoryTheory.Functor (CategoryTheory.Limits.Bicone (CategoryTheory.Limits.pairFunction X Y)) (CategoryTheory.Limits.BinaryBicone X Y)
• CategoryTheory.Limits.BinaryBicone.toBiconeFunctor 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} : CategoryTheory.Functor (CategoryTheory.Limits.BinaryBicone X Y) (CategoryTheory.Limits.Bicone (CategoryTheory.Limits.pairFunction X Y))
• CategoryTheory.Limits.Bicone.toBinaryBiconeIsBilimit 📋 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)) : b.toBinaryBicone.IsBilimit ≃ b.IsBilimit
• CategoryTheory.Limits.Bicone.toBinaryBiconeIsColimit 📋 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.IsColimit b.toBinaryBicone.toCocone ≃ CategoryTheory.Limits.IsColimit b.toCocone
• CategoryTheory.Limits.Bicone.toBinaryBiconeIsLimit 📋 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.IsLimit b.toBinaryBicone.toCone ≃ CategoryTheory.Limits.IsLimit b.toCone
• 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.Bicone.toBinaryBiconeFunctor_obj_fst 📋 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).fst = b.π CategoryTheory.Limits.WalkingPair.left
• CategoryTheory.Limits.Bicone.toBinaryBiconeFunctor_obj_inl 📋 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).inl = b.ι CategoryTheory.Limits.WalkingPair.left
• CategoryTheory.Limits.Bicone.toBinaryBiconeFunctor_obj_inr 📋 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).inr = b.ι CategoryTheory.Limits.WalkingPair.right
• CategoryTheory.Limits.Bicone.toBinaryBiconeFunctor_obj_snd 📋 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).snd = b.π CategoryTheory.Limits.WalkingPair.right
• 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.Bicone.toBinaryBiconeFunctor_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.Bicone (CategoryTheory.Limits.pairFunction X Y)} (f : X✝ ⟶ Y✝) : (CategoryTheory.Limits.Bicone.toBinaryBiconeFunctor.map f).hom = f.hom
• 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.Functor.mapBicone 📋 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] {J : Type w₁} {f : J → C} (b : CategoryTheory.Limits.Bicone f) : CategoryTheory.Limits.Bicone (F.obj ∘ f)
• CategoryTheory.Functor.mapBicone_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] {J : Type w₁} {f : J → C} (b : CategoryTheory.Limits.Bicone f) : (F.mapBicone b).pt = F.obj b.pt
• CategoryTheory.Limits.isBilimitOfPreserves 📋 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] {J : Type w₁} {f : J → C} (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [CategoryTheory.Limits.PreservesBiproduct f F] {b : CategoryTheory.Limits.Bicone f} (hb : b.IsBilimit) : (F.mapBicone b).IsBilimit
• CategoryTheory.Limits.PreservesBiproduct.mk 📋 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] {J : Type w₁} {f : J → C} {F : CategoryTheory.Functor C D} [F.PreservesZeroMorphisms] (preserves : ∀ {b : CategoryTheory.Limits.Bicone f} (a : b.IsBilimit), Nonempty (F.mapBicone b).IsBilimit) : CategoryTheory.Limits.PreservesBiproduct f F
• CategoryTheory.Limits.PreservesBiproduct.preserves 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
  {C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst✝¹ : CategoryTheory.Category.{v₂, u₂} D} {inst✝² : CategoryTheory.Limits.HasZeroMorphisms C} {inst✝³ : CategoryTheory.Limits.HasZeroMorphisms D} {J : Type w₁} {f : J → C} {F : CategoryTheory.Functor C D} {inst✝⁴ : F.PreservesZeroMorphisms} [self : CategoryTheory.Limits.PreservesBiproduct f F] {b : CategoryTheory.Limits.Bicone f} : ∀ (a : b.IsBilimit), Nonempty (F.mapBicone b).IsBilimit
• CategoryTheory.Functor.mapBicone_ι 📋 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] {J : Type w₁} {f : J → C} (b : CategoryTheory.Limits.Bicone f) (j : J) : (F.mapBicone b).ι j = F.map (b.ι j)
• CategoryTheory.Functor.mapBicone_π 📋 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] {J : Type w₁} {f : J → C} (b : CategoryTheory.Limits.Bicone f) (j : J) : (F.mapBicone b).π j = F.map (b.π j)
• CategoryTheory.Functor.mapBicone_whisker 📋 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] {J : Type w₁} {K : Type w₂} {g : K ≃ J} {f : J → C} (c : CategoryTheory.Limits.Bicone f) : F.mapBicone (c.whisker g) = (F.mapBicone c).whisker g
• CategoryTheory.Limits.isBilimitOfIsColimit 📋 Mathlib.CategoryTheory.Preadditive.Biproducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {J : Type u_1} [Fintype J] {f : J → C} (t : CategoryTheory.Limits.Bicone f) (ht : CategoryTheory.Limits.IsColimit t.toCocone) : t.IsBilimit
• CategoryTheory.Limits.isBilimitOfIsLimit 📋 Mathlib.CategoryTheory.Preadditive.Biproducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {J : Type u_1} [Fintype J] {f : J → C} (t : CategoryTheory.Limits.Bicone f) (ht : CategoryTheory.Limits.IsLimit t.toCone) : t.IsBilimit
• CategoryTheory.Limits.hasBiproduct_of_total 📋 Mathlib.CategoryTheory.Preadditive.Biproducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {J : Type u_1} [Fintype J] {f : J → C} (b : CategoryTheory.Limits.Bicone f) (total : ∑ j, CategoryTheory.CategoryStruct.comp (b.π j) (b.ι j) = CategoryTheory.CategoryStruct.id b.pt) : CategoryTheory.Limits.HasBiproduct f
• CategoryTheory.Limits.isBilimitOfTotal 📋 Mathlib.CategoryTheory.Preadditive.Biproducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {J : Type u_1} [Fintype J] {f : J → C} (b : CategoryTheory.Limits.Bicone f) (total : ∑ j, CategoryTheory.CategoryStruct.comp (b.π j) (b.ι j) = CategoryTheory.CategoryStruct.id b.pt) : b.IsBilimit
• CategoryTheory.Limits.IsBilimit.total 📋 Mathlib.CategoryTheory.Preadditive.Biproducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {J : Type u_1} [Fintype J] {f : J → C} {b : CategoryTheory.Limits.Bicone f} (i : b.IsBilimit) : ∑ j, CategoryTheory.CategoryStruct.comp (b.π j) (b.ι j) = CategoryTheory.CategoryStruct.id b.pt
• CategoryTheory.ObjectProperty.IsStableUnderRetracts.of_bicone 📋 Mathlib.CategoryTheory.ObjectProperty.Retract
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) [P.IsStableUnderRetracts] [CategoryTheory.Limits.HasZeroMorphisms C] {J : Type u_1} (F : J → C) (c : CategoryTheory.Limits.Bicone F) (h : P c.pt) (j : J) : P (F j)
• CategoryTheory.Abelian.Ext.addEquivBiproduct 📋 Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] (X : C) {J : Type u_1} [Fintype J] {Y : J → C} {c : CategoryTheory.Limits.Bicone Y} (hc : c.IsBilimit) (n : ℕ) : CategoryTheory.Abelian.Ext X c.pt n ≃+ ((i : J) → CategoryTheory.Abelian.Ext X (Y i) n)
• CategoryTheory.Abelian.Ext.biproductAddEquiv 📋 Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {J : Type u_1} [Fintype J] {X : J → C} {c : CategoryTheory.Limits.Bicone X} (hc : c.IsBilimit) (Y : C) (n : ℕ) : CategoryTheory.Abelian.Ext c.pt Y n ≃+ ((i : J) → CategoryTheory.Abelian.Ext (X i) Y n)
• CategoryTheory.Idempotents.Karoubi.Biproducts.bicone 📋 Mathlib.CategoryTheory.Idempotents.Biproducts
  {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Finite J] (F : J → CategoryTheory.Idempotents.Karoubi C) : CategoryTheory.Limits.Bicone F

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