Loogle!

Result

Found 117 declarations mentioning CategoryTheory.Limits.IsColimit.desc.

• CategoryTheory.Limits.IsColimit.desc 📋 Mathlib.CategoryTheory.Limits.IsLimit
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {t : CategoryTheory.Limits.Cocone F} (self : CategoryTheory.Limits.IsColimit t) (s : CategoryTheory.Limits.Cocone F) : t.pt ⟶ s.pt
• CategoryTheory.Limits.IsColimit.ofPointIso 📋 Mathlib.CategoryTheory.Limits.IsLimit
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {r t : CategoryTheory.Limits.Cocone F} (P : CategoryTheory.Limits.IsColimit r) [i : CategoryTheory.IsIso (P.desc t)] : CategoryTheory.Limits.IsColimit t
• CategoryTheory.Limits.IsColimit.nonempty_isColimit_iff_isIso_desc 📋 Mathlib.CategoryTheory.Limits.IsLimit
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {s t : CategoryTheory.Limits.Cocone F} (hs : CategoryTheory.Limits.IsColimit s) : Nonempty (CategoryTheory.Limits.IsColimit t) ↔ CategoryTheory.IsIso (hs.desc t)
• CategoryTheory.Limits.IsColimit.desc_self 📋 Mathlib.CategoryTheory.Limits.IsLimit
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone F} (t : CategoryTheory.Limits.IsColimit c) : t.desc c = CategoryTheory.CategoryStruct.id c.pt
• CategoryTheory.Limits.IsColimit.descCoconeMorphism_hom 📋 Mathlib.CategoryTheory.Limits.IsLimit
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {t : CategoryTheory.Limits.Cocone F} (h : CategoryTheory.Limits.IsColimit t) (s : CategoryTheory.Limits.Cocone F) : (h.descCoconeMorphism s).hom = h.desc s
• CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso_hom_desc 📋 Mathlib.CategoryTheory.Limits.IsLimit
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {r s t : CategoryTheory.Limits.Cocone F} (P : CategoryTheory.Limits.IsColimit s) (Q : CategoryTheory.Limits.IsColimit t) : CategoryTheory.CategoryStruct.comp (P.coconePointUniqueUpToIso Q).hom (Q.desc r) = P.desc r
• CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso_inv_desc 📋 Mathlib.CategoryTheory.Limits.IsLimit
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {r s t : CategoryTheory.Limits.Cocone F} (P : CategoryTheory.Limits.IsColimit s) (Q : CategoryTheory.Limits.IsColimit t) : CategoryTheory.CategoryStruct.comp (P.coconePointUniqueUpToIso Q).inv (P.desc r) = Q.desc r
• CategoryTheory.Limits.IsColimit.ofIsoColimit_desc 📋 Mathlib.CategoryTheory.Limits.IsLimit
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {r t : CategoryTheory.Limits.Cocone F} (P : CategoryTheory.Limits.IsColimit r) (i : r ≅ t) (s : CategoryTheory.Limits.Cocone F) : (P.ofIsoColimit i).desc s = CategoryTheory.CategoryStruct.comp i.inv.hom (P.desc s)
• CategoryTheory.Limits.IsColimit.fac 📋 Mathlib.CategoryTheory.Limits.IsLimit
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {t : CategoryTheory.Limits.Cocone F} (self : CategoryTheory.Limits.IsColimit t) (s : CategoryTheory.Limits.Cocone F) (j : J) : CategoryTheory.CategoryStruct.comp (t.ι.app j) (self.desc s) = s.ι.app j
• CategoryTheory.Limits.IsColimit.coconePointsIsoOfNatIso_hom_desc 📋 Mathlib.CategoryTheory.Limits.IsLimit
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F G : CategoryTheory.Functor J C} {r s : CategoryTheory.Limits.Cocone G} {t : CategoryTheory.Limits.Cocone F} (P : CategoryTheory.Limits.IsColimit t) (Q : CategoryTheory.Limits.IsColimit s) (w : F ≅ G) : CategoryTheory.CategoryStruct.comp (P.coconePointsIsoOfNatIso Q w).hom (Q.desc r) = P.map r w.hom
• CategoryTheory.Limits.IsColimit.coconePointsIsoOfNatIso_inv_desc 📋 Mathlib.CategoryTheory.Limits.IsLimit
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F G : CategoryTheory.Functor J C} {r s : CategoryTheory.Limits.Cocone F} {t : CategoryTheory.Limits.Cocone G} (P : CategoryTheory.Limits.IsColimit s) (Q : CategoryTheory.Limits.IsColimit t) (w : F ≅ G) : CategoryTheory.CategoryStruct.comp (P.coconePointsIsoOfNatIso Q w).inv (P.desc r) = Q.map r w.inv
• CategoryTheory.Limits.IsColimit.mkCoconeMorphism_desc 📋 Mathlib.CategoryTheory.Limits.IsLimit
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {t : CategoryTheory.Limits.Cocone F} (desc : (s : CategoryTheory.Limits.Cocone F) → t ⟶ s) (uniq : ∀ (s : CategoryTheory.Limits.Cocone F) (m : t ⟶ s), m = desc s) (s : CategoryTheory.Limits.Cocone F) : (CategoryTheory.Limits.IsColimit.mkCoconeMorphism desc uniq).desc s = (desc s).hom
• CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso_hom_desc_assoc 📋 Mathlib.CategoryTheory.Limits.IsLimit
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {r s t : CategoryTheory.Limits.Cocone F} (P : CategoryTheory.Limits.IsColimit s) (Q : CategoryTheory.Limits.IsColimit t) {Z : C} (h : r.pt ⟶ Z) : CategoryTheory.CategoryStruct.comp (P.coconePointUniqueUpToIso Q).hom (CategoryTheory.CategoryStruct.comp (Q.desc r) h) = CategoryTheory.CategoryStruct.comp (P.desc r) h
• CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso_inv_desc_assoc 📋 Mathlib.CategoryTheory.Limits.IsLimit
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {r s t : CategoryTheory.Limits.Cocone F} (P : CategoryTheory.Limits.IsColimit s) (Q : CategoryTheory.Limits.IsColimit t) {Z : C} (h : r.pt ⟶ Z) : CategoryTheory.CategoryStruct.comp (P.coconePointUniqueUpToIso Q).inv (CategoryTheory.CategoryStruct.comp (P.desc r) h) = CategoryTheory.CategoryStruct.comp (Q.desc r) h
• CategoryTheory.Limits.IsColimit.ofFaithful 📋 Mathlib.CategoryTheory.Limits.IsLimit
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {t : CategoryTheory.Limits.Cocone F} {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (G : CategoryTheory.Functor C D) [G.Faithful] (ht : CategoryTheory.Limits.IsColimit (G.mapCocone t)) (desc : (s : CategoryTheory.Limits.Cocone F) → t.pt ⟶ s.pt) (h : ∀ (s : CategoryTheory.Limits.Cocone F), G.map (desc s) = ht.desc (G.mapCocone s)) : CategoryTheory.Limits.IsColimit t
• CategoryTheory.Limits.IsColimit.hom_desc 📋 Mathlib.CategoryTheory.Limits.IsLimit
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {t : CategoryTheory.Limits.Cocone F} (h : CategoryTheory.Limits.IsColimit t) {W : C} (m : t.pt ⟶ W) : m = h.desc { pt := W, ι := CategoryTheory.NatTrans.mk' (fun b => CategoryTheory.CategoryStruct.comp (t.ι.app b) m) ⋯ }
• CategoryTheory.Limits.IsColimit.uniq 📋 Mathlib.CategoryTheory.Limits.IsLimit
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {t : CategoryTheory.Limits.Cocone F} (self : CategoryTheory.Limits.IsColimit t) (s : CategoryTheory.Limits.Cocone F) (m : t.pt ⟶ s.pt) : (∀ (j : J), CategoryTheory.CategoryStruct.comp (t.ι.app j) m = s.ι.app j) → m = self.desc s
• CategoryTheory.Limits.IsColimit.fac_assoc 📋 Mathlib.CategoryTheory.Limits.IsLimit
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {t : CategoryTheory.Limits.Cocone F} (self : CategoryTheory.Limits.IsColimit t) (s : CategoryTheory.Limits.Cocone F) (j : J) {Z : C} (h : s.pt ⟶ Z) : CategoryTheory.CategoryStruct.comp (t.ι.app j) (CategoryTheory.CategoryStruct.comp (self.desc s) h) = CategoryTheory.CategoryStruct.comp (s.ι.app j) h
• CategoryTheory.Limits.IsColimit.coconePointsIsoOfNatIso_hom_desc_assoc 📋 Mathlib.CategoryTheory.Limits.IsLimit
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F G : CategoryTheory.Functor J C} {r s : CategoryTheory.Limits.Cocone G} {t : CategoryTheory.Limits.Cocone F} (P : CategoryTheory.Limits.IsColimit t) (Q : CategoryTheory.Limits.IsColimit s) (w : F ≅ G) {Z : C} (h : r.pt ⟶ Z) : CategoryTheory.CategoryStruct.comp (P.coconePointsIsoOfNatIso Q w).hom (CategoryTheory.CategoryStruct.comp (Q.desc r) h) = CategoryTheory.CategoryStruct.comp (P.map r w.hom) h
• CategoryTheory.Limits.IsColimit.coconePointsIsoOfNatIso_inv_desc_assoc 📋 Mathlib.CategoryTheory.Limits.IsLimit
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F G : CategoryTheory.Functor J C} {r s : CategoryTheory.Limits.Cocone F} {t : CategoryTheory.Limits.Cocone G} (P : CategoryTheory.Limits.IsColimit s) (Q : CategoryTheory.Limits.IsColimit t) (w : F ≅ G) {Z : C} (h : r.pt ⟶ Z) : CategoryTheory.CategoryStruct.comp (P.coconePointsIsoOfNatIso Q w).inv (CategoryTheory.CategoryStruct.comp (P.desc r) h) = CategoryTheory.CategoryStruct.comp (Q.map r w.inv) h
• CategoryTheory.Limits.IsColimit.coconePointsIsoOfEquivalence_hom 📋 Mathlib.CategoryTheory.Limits.IsLimit
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {s : CategoryTheory.Limits.Cocone F} {G : CategoryTheory.Functor K C} {t : CategoryTheory.Limits.Cocone G} (P : CategoryTheory.Limits.IsColimit s) (Q : CategoryTheory.Limits.IsColimit t) (e : J ≌ K) (w : e.functor.comp G ≅ F) : (P.coconePointsIsoOfEquivalence Q e w).hom = P.desc ((CategoryTheory.Limits.Cocone.equivalenceOfReindexing e w).functor.obj t)
• CategoryTheory.Limits.IsColimit.coconePointsIsoOfEquivalence_inv 📋 Mathlib.CategoryTheory.Limits.IsLimit
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {s : CategoryTheory.Limits.Cocone F} {G : CategoryTheory.Functor K C} {t : CategoryTheory.Limits.Cocone G} (P : CategoryTheory.Limits.IsColimit s) (Q : CategoryTheory.Limits.IsColimit t) (e : J ≌ K) (w : e.functor.comp G ≅ F) : (P.coconePointsIsoOfEquivalence Q e w).inv = Q.desc ((CategoryTheory.Limits.Cocone.equivalenceOfReindexing e.symm ((e.inverse.isoWhiskerLeft w).symm ≪≫ e.invFunIdAssoc G)).functor.obj s)
• CategoryTheory.Limits.IsColimit.ofCoconeEquiv_symm_apply_desc 📋 Mathlib.CategoryTheory.Limits.IsLimit
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {G : CategoryTheory.Functor K D} (h : CategoryTheory.Limits.Cocone G ≌ CategoryTheory.Limits.Cocone F) {c : CategoryTheory.Limits.Cocone G} (P : CategoryTheory.Limits.IsColimit c) (s : CategoryTheory.Limits.Cocone F) : ((CategoryTheory.Limits.IsColimit.ofCoconeEquiv h).symm P).desc s = CategoryTheory.CategoryStruct.comp (h.functor.map (P.descCoconeMorphism (h.inverse.obj s))).hom (h.counitIso.hom.app s).hom
• CategoryTheory.Limits.IsColimit.ofCoconeEquiv_apply_desc 📋 Mathlib.CategoryTheory.Limits.IsLimit
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {G : CategoryTheory.Functor K D} (h : CategoryTheory.Limits.Cocone G ≌ CategoryTheory.Limits.Cocone F) {c : CategoryTheory.Limits.Cocone G} (P : CategoryTheory.Limits.IsColimit (h.functor.obj c)) (s : CategoryTheory.Limits.Cocone G) : ((CategoryTheory.Limits.IsColimit.ofCoconeEquiv h) P).desc s = CategoryTheory.CategoryStruct.comp (h.unitIso.hom.app c).hom (CategoryTheory.CategoryStruct.comp (h.inverse.map (P.descCoconeMorphism (h.functor.obj s))).hom (h.unitIso.inv.app s).hom)
• CategoryTheory.Limits.colimit.isColimit_desc 📋 Mathlib.CategoryTheory.Limits.HasLimits
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor J C} [CategoryTheory.Limits.HasColimit F] (c : CategoryTheory.Limits.Cocone F) : (CategoryTheory.Limits.colimit.isColimit F).desc c = CategoryTheory.Limits.colimit.desc F c
• CategoryTheory.Limits.colimit.pre_eq 📋 Mathlib.CategoryTheory.Limits.HasLimits
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor J C} [CategoryTheory.Limits.HasColimit F] {E : CategoryTheory.Functor K J} [CategoryTheory.Limits.HasColimit (E.comp F)] (s : CategoryTheory.Limits.ColimitCocone (E.comp F)) (t : CategoryTheory.Limits.ColimitCocone F) : CategoryTheory.Limits.colimit.pre F E = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.isoColimitCocone s).hom (CategoryTheory.CategoryStruct.comp (s.isColimit.desc (CategoryTheory.Limits.Cocone.whisker E t.cocone)) (CategoryTheory.Limits.colimit.isoColimitCocone t).inv)
• CategoryTheory.Limits.Cofan.IsColimit.inj_desc 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : β → C} {c : CategoryTheory.Limits.Cofan X} (d : CategoryTheory.Limits.Cofan X) (hc : CategoryTheory.Limits.IsColimit c) (i : β) : CategoryTheory.CategoryStruct.comp (c.inj i) (hc.desc d) = d.inj i
• CategoryTheory.Limits.Cofan.IsColimit.inj_desc_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : β → C} {c : CategoryTheory.Limits.Cofan X} (d : CategoryTheory.Limits.Cofan X) (hc : CategoryTheory.Limits.IsColimit c) (i : β) {Z : C} (h : d.pt ⟶ Z) : CategoryTheory.CategoryStruct.comp (c.inj i) (CategoryTheory.CategoryStruct.comp (hc.desc d) h) = CategoryTheory.CategoryStruct.comp (d.inj i) h
• CategoryTheory.Limits.Cofan.IsColimit.mk_desc 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : β → C} (s : CategoryTheory.Limits.Cofan f) (desc : (t : CategoryTheory.Limits.Cofan f) → s.pt ⟶ t.pt) (fac : ∀ (t : CategoryTheory.Limits.Cofan f) (j : β), CategoryTheory.CategoryStruct.comp (s.inj j) (desc t) = t.inj j := by cat_disch) (uniq : ∀ (t : CategoryTheory.Limits.Cofan f) (m : s.pt ⟶ t.pt), (∀ (j : β), CategoryTheory.CategoryStruct.comp (s.inj j) m = t.inj j) → m = desc t := by cat_disch) (t : CategoryTheory.Limits.Cofan f) : (CategoryTheory.Limits.Cofan.IsColimit.mk s desc fac uniq).desc t = desc t
• CategoryTheory.Limits.colimitCoconeOfUnique_isColimit_desc 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [Unique β] (f : β → C) (s : CategoryTheory.Limits.Cocone (CategoryTheory.Discrete.functor f)) : (CategoryTheory.Limits.colimitCoconeOfUnique f).isColimit.desc s = s.ι.app default
• CategoryTheory.Limits.BinaryCofan.IsColimit.desc'_coe 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {W X Y : C} {s : CategoryTheory.Limits.BinaryCofan X Y} (h : CategoryTheory.Limits.IsColimit s) (f : X ⟶ W) (g : Y ⟶ W) : ↑(CategoryTheory.Limits.BinaryCofan.IsColimit.desc' h f g) = h.desc (CategoryTheory.Limits.BinaryCofan.mk f g)
• CategoryTheory.Limits.Cofork.IsColimit.π_desc 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} {s t : CategoryTheory.Limits.Cofork f g} (hs : CategoryTheory.Limits.IsColimit s) : CategoryTheory.CategoryStruct.comp s.π (hs.desc t) = t.π
• CategoryTheory.Limits.Cofork.IsColimit.π_desc_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} {s t : CategoryTheory.Limits.Cofork f g} (hs : CategoryTheory.Limits.IsColimit s) {Z : C} (h : t.pt ⟶ Z) : CategoryTheory.CategoryStruct.comp s.π (CategoryTheory.CategoryStruct.comp (hs.desc t) h) = CategoryTheory.CategoryStruct.comp t.π h
• CategoryTheory.Limits.splitEpiOfIdempotentOfIsColimitCofork_section_ 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  (C : Type u) [CategoryTheory.Category.{v, u} C] {X : C} {f : X ⟶ X} (hf : CategoryTheory.CategoryStruct.comp f f = f) {c : CategoryTheory.Limits.Cofork (CategoryTheory.CategoryStruct.id X) f} (i : CategoryTheory.Limits.IsColimit c) : (CategoryTheory.Limits.splitEpiOfIdempotentOfIsColimitCofork C hf i).section_ = i.desc (CategoryTheory.Limits.Cofork.ofπ f ⋯)
• CategoryTheory.Limits.isCokernelEpiComp_desc 📋 Mathlib.CategoryTheory.Limits.Shapes.Kernels
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} {c : CategoryTheory.Limits.CokernelCofork f} (i : CategoryTheory.Limits.IsColimit c) {W : C} (g : W ⟶ X) [hg : CategoryTheory.Epi g] {h : W ⟶ Y} (hh : h = CategoryTheory.CategoryStruct.comp g f) (s : CategoryTheory.Limits.CokernelCofork h) : (CategoryTheory.Limits.isCokernelEpiComp i g hh).desc s = i.desc (CategoryTheory.Limits.Cofork.ofπ (CategoryTheory.Limits.Cofork.π s) ⋯)
• CategoryTheory.Preadditive.isColimitCoforkOfCokernelCofork_desc 📋 Mathlib.CategoryTheory.Preadditive.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} {f g : X ⟶ Y} {c : CategoryTheory.Limits.CokernelCofork (f - g)} (i : CategoryTheory.Limits.IsColimit c) (s : CategoryTheory.Limits.Cofork f g) : (CategoryTheory.Preadditive.isColimitCoforkOfCokernelCofork i).desc s = i.desc (CategoryTheory.Preadditive.cokernelCoforkOfCofork s)
• 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.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) (j : J) : (CategoryTheory.Limits.Bicone.ofColimitCocone ht).π j = ht.desc (CategoryTheory.Limits.Cofan.mk (f j) fun j' => if h : j' = j then CategoryTheory.eqToHom ⋯ else 0)
• CategoryTheory.Limits.cokernelBiproductιIso_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) (i : J) [CategoryTheory.Limits.HasBiproduct f] [CategoryTheory.Limits.HasBiproduct (Subtype.restrict (fun j => j ≠ i) f)] : (CategoryTheory.Limits.cokernelBiproductιIso f i).inv = (CategoryTheory.Limits.biproduct.isColimitToSubtype f i).desc (CategoryTheory.Limits.colimit.cocone (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.biproduct.ι f i) 0))
• CategoryTheory.Limits.cokernelBiproductFromSubtypeIso_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : Type} [Finite K] [CategoryTheory.Limits.HasFiniteBiproducts C] (f : K → C) (p : K → Prop) : (CategoryTheory.Limits.cokernelBiproductFromSubtypeIso f p).inv = (CategoryTheory.Limits.CokernelCofork.IsColimit.ofπ (CategoryTheory.Limits.biproduct.toSubtype f pᶜ) ⋯ (fun {x} g x_1 => CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.fromSubtype f pᶜ) g) ⋯ ⋯).desc (CategoryTheory.Limits.colimit.cocone (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.biproduct.fromSubtype f p) 0))
• CategoryTheory.Limits.cokernelBiprodInlIso_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] : CategoryTheory.Limits.cokernelBiprodInlIso.inv = (CategoryTheory.Limits.biprod.isCokernelInlCokernelFork X Y).desc (CategoryTheory.Limits.colimit.cocone (CategoryTheory.Limits.parallelPair CategoryTheory.Limits.biprod.inl 0))
• CategoryTheory.Limits.cokernelBiprodInrIso_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] : CategoryTheory.Limits.cokernelBiprodInrIso.inv = (CategoryTheory.Limits.biprod.isCokernelInrCokernelFork X Y).desc (CategoryTheory.Limits.colimit.cocone (CategoryTheory.Limits.parallelPair CategoryTheory.Limits.biprod.inr 0))
• CategoryTheory.preserves_desc_mapCocone 📋 Mathlib.CategoryTheory.Limits.Preserves.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {J : Type w} [CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor J C) [CategoryTheory.Limits.PreservesColimit F G] (c₁ c₂ : CategoryTheory.Limits.Cocone F) (t : CategoryTheory.Limits.IsColimit c₁) : (CategoryTheory.Limits.isColimitOfPreserves G t).desc (G.mapCocone c₂) = G.map (t.desc c₂)
• CategoryTheory.Limits.combineCocones_pt_map 📋 Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) (c : (k : K) → CategoryTheory.Limits.ColimitCocone (F.flip.obj k)) {k₁ k₂ : K} (f : k₁ ⟶ k₂) : (CategoryTheory.Limits.combineCocones F c).pt.map f = (c k₁).isColimit.desc { pt := (c k₂).cocone.pt, ι := CategoryTheory.CategoryStruct.comp (F.flip.map f) (c k₂).cocone.ι }
• CategoryTheory.Limits.combineCocones_ι_app_app 📋 Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) (c : (k : K) → CategoryTheory.Limits.ColimitCocone (F.flip.obj k)) (j : J) (k : K) : ((CategoryTheory.Limits.combineCocones F c).ι.app j).app k = (c k).cocone.ι.app j
• CategoryTheory.Coyoneda.colimitCoconeIsColimit_desc 📋 Mathlib.CategoryTheory.Limits.Yoneda
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : Cᵒᵖ) (s : CategoryTheory.Limits.Cocone (CategoryTheory.coyoneda.obj X)) : (CategoryTheory.Coyoneda.colimitCoconeIsColimit X).desc s = TypeCat.ofHom fun x => (CategoryTheory.ConcreteCategory.hom (s.ι.app (Opposite.unop X))) (CategoryTheory.CategoryStruct.id (Opposite.unop X))
• ModuleCat.directLimitIsColimit_desc 📋 Mathlib.Algebra.Category.ModuleCat.Limits
  {R : Type u} [Ring R] {ι : Type v} [DecidableEq ι] [Preorder ι] (G : ι → Type v) [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] (f : (i j : ι) → i ≤ j → G i →ₗ[R] G j) [DirectedSystem G fun i j h => ⇑(f i j h)] (s : CategoryTheory.Limits.Cocone (ModuleCat.directLimitDiagram G f)) : (ModuleCat.directLimitIsColimit G f).desc s = ModuleCat.ofHom (Module.DirectLimit.lift R ι G f (fun i => ModuleCat.Hom.hom (s.ι.app i)) ⋯)
• CategoryTheory.Limits.isColimitCoconeLeftOpOfCone_desc 📋 Mathlib.CategoryTheory.Limits.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J Cᵒᵖ) {c : CategoryTheory.Limits.Cone F} (hc : CategoryTheory.Limits.IsLimit c) (s : CategoryTheory.Limits.Cocone F.leftOp) : (CategoryTheory.Limits.isColimitCoconeLeftOpOfCone F hc).desc s = (hc.lift (CategoryTheory.Limits.coneOfCoconeLeftOp s)).unop
• CategoryTheory.Limits.isLimitConeLeftOpOfCocone_lift 📋 Mathlib.CategoryTheory.Limits.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J Cᵒᵖ) {c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.Limits.IsColimit c) (s : CategoryTheory.Limits.Cone F.leftOp) : (CategoryTheory.Limits.isLimitConeLeftOpOfCocone F hc).lift s = (hc.desc (CategoryTheory.Limits.coconeOfConeLeftOp s)).unop
• CategoryTheory.Limits.isColimitCoconeRightOpOfCone_desc 📋 Mathlib.CategoryTheory.Limits.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor Jᵒᵖ C) {c : CategoryTheory.Limits.Cone F} (hc : CategoryTheory.Limits.IsLimit c) (s : CategoryTheory.Limits.Cocone F.rightOp) : (CategoryTheory.Limits.isColimitCoconeRightOpOfCone F hc).desc s = (hc.lift (CategoryTheory.Limits.coneOfCoconeRightOp s)).op
• CategoryTheory.Limits.isLimitConeRightOpOfCocone_lift 📋 Mathlib.CategoryTheory.Limits.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor Jᵒᵖ C) {c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.Limits.IsColimit c) (s : CategoryTheory.Limits.Cone F.rightOp) : (CategoryTheory.Limits.isLimitConeRightOpOfCocone F hc).lift s = (hc.desc (CategoryTheory.Limits.coconeOfConeRightOp s)).op
• CategoryTheory.Limits.isColimitCoconeOfConeUnop_desc 📋 Mathlib.CategoryTheory.Limits.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ) {c : CategoryTheory.Limits.Cone F.unop} (hc : CategoryTheory.Limits.IsLimit c) (s : CategoryTheory.Limits.Cocone F) : (CategoryTheory.Limits.isColimitCoconeOfConeUnop F hc).desc s = (hc.lift (CategoryTheory.Limits.coneUnopOfCocone s)).op
• CategoryTheory.Limits.isLimitConeOfCoconeUnop_lift 📋 Mathlib.CategoryTheory.Limits.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ) {c : CategoryTheory.Limits.Cocone F.unop} (hc : CategoryTheory.Limits.IsColimit c) (s : CategoryTheory.Limits.Cone F) : (CategoryTheory.Limits.isLimitConeOfCoconeUnop F hc).lift s = (hc.desc (CategoryTheory.Limits.coconeUnopOfCone s)).op
• CategoryTheory.Limits.isColimitCoconeUnopOfCone_desc 📋 Mathlib.CategoryTheory.Limits.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ) {c : CategoryTheory.Limits.Cone F} (hc : CategoryTheory.Limits.IsLimit c) (s : CategoryTheory.Limits.Cocone F.unop) : (CategoryTheory.Limits.isColimitCoconeUnopOfCone F hc).desc s = (hc.lift (CategoryTheory.Limits.coneOfCoconeUnop s)).unop
• CategoryTheory.Limits.isLimitConeUnopOfCocone_lift 📋 Mathlib.CategoryTheory.Limits.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ) {c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.Limits.IsColimit c) (s : CategoryTheory.Limits.Cone F.unop) : (CategoryTheory.Limits.isLimitConeUnopOfCocone F hc).lift s = (hc.desc (CategoryTheory.Limits.coconeOfConeUnop s)).unop
• CategoryTheory.Limits.isColimitOfConeRightOpOfCocone_desc 📋 Mathlib.CategoryTheory.Limits.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor Jᵒᵖ C) {c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.coneRightOpOfCocone c)) (s : CategoryTheory.Limits.Cocone F) : (CategoryTheory.Limits.isColimitOfConeRightOpOfCocone F hc).desc s = (hc.lift (CategoryTheory.Limits.coneRightOpOfCocone s)).unop
• CategoryTheory.Limits.isLimitOfCoconeRightOpOfCone_lift 📋 Mathlib.CategoryTheory.Limits.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor Jᵒᵖ C) {c : CategoryTheory.Limits.Cone F} (hc : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.coconeRightOpOfCone c)) (s : CategoryTheory.Limits.Cone F) : (CategoryTheory.Limits.isLimitOfCoconeRightOpOfCone F hc).lift s = (hc.desc (CategoryTheory.Limits.coconeRightOpOfCone s)).unop
• CategoryTheory.Limits.isColimitOfConeLeftOpOfCocone_desc 📋 Mathlib.CategoryTheory.Limits.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J Cᵒᵖ) {c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.coneLeftOpOfCocone c)) (s : CategoryTheory.Limits.Cocone F) : (CategoryTheory.Limits.isColimitOfConeLeftOpOfCocone F hc).desc s = (hc.lift (CategoryTheory.Limits.coneLeftOpOfCocone s)).op
• CategoryTheory.Limits.isLimitOfCoconeLeftOpOfCone_lift 📋 Mathlib.CategoryTheory.Limits.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J Cᵒᵖ) {c : CategoryTheory.Limits.Cone F} (hc : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.coconeLeftOpOfCone c)) (s : CategoryTheory.Limits.Cone F) : (CategoryTheory.Limits.isLimitOfCoconeLeftOpOfCone F hc).lift s = (hc.desc (CategoryTheory.Limits.coconeLeftOpOfCone s)).op
• CategoryTheory.Limits.isColimitCoconeOfConeRightOp_desc 📋 Mathlib.CategoryTheory.Limits.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor Jᵒᵖ C) {c : CategoryTheory.Limits.Cone F.rightOp} (hc : CategoryTheory.Limits.IsLimit c) (s : CategoryTheory.Limits.Cocone F) : (CategoryTheory.Limits.isColimitCoconeOfConeRightOp F hc).desc s = (hc.lift (CategoryTheory.Limits.coneRightOpOfCocone s)).unop
• CategoryTheory.Limits.isColimitOfConeOfCoconeLeftOp_desc 📋 Mathlib.CategoryTheory.Limits.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J Cᵒᵖ) {c : CategoryTheory.Limits.Cocone F.leftOp} (hc : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.coneOfCoconeLeftOp c)) (s : CategoryTheory.Limits.Cocone F.leftOp) : (CategoryTheory.Limits.isColimitOfConeOfCoconeLeftOp F hc).desc s = (hc.lift (CategoryTheory.Limits.coneOfCoconeLeftOp s)).unop
• CategoryTheory.Limits.isColimitOfConeOfCoconeUnop_desc 📋 Mathlib.CategoryTheory.Limits.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ) {c : CategoryTheory.Limits.Cocone F.unop} (hc : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.coneOfCoconeUnop c)) (s : CategoryTheory.Limits.Cocone F.unop) : (CategoryTheory.Limits.isColimitOfConeOfCoconeUnop F hc).desc s = (hc.lift (CategoryTheory.Limits.coneOfCoconeUnop s)).unop
• CategoryTheory.Limits.isLimitConeOfCoconeRightOp_lift 📋 Mathlib.CategoryTheory.Limits.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor Jᵒᵖ C) {c : CategoryTheory.Limits.Cocone F.rightOp} (hc : CategoryTheory.Limits.IsColimit c) (s : CategoryTheory.Limits.Cone F) : (CategoryTheory.Limits.isLimitConeOfCoconeRightOp F hc).lift s = (hc.desc (CategoryTheory.Limits.coconeRightOpOfCone s)).unop
• CategoryTheory.Limits.isLimitOfCoconeOfConeLeftOp_lift 📋 Mathlib.CategoryTheory.Limits.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J Cᵒᵖ) {c : CategoryTheory.Limits.Cone F.leftOp} (hc : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.coconeOfConeLeftOp c)) (s : CategoryTheory.Limits.Cone F.leftOp) : (CategoryTheory.Limits.isLimitOfCoconeOfConeLeftOp F hc).lift s = (hc.desc (CategoryTheory.Limits.coconeOfConeLeftOp s)).unop
• CategoryTheory.Limits.isLimitOfCoconeOfConeUnop_lift 📋 Mathlib.CategoryTheory.Limits.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ) {c : CategoryTheory.Limits.Cone F.unop} (hc : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.coconeOfConeUnop c)) (s : CategoryTheory.Limits.Cone F.unop) : (CategoryTheory.Limits.isLimitOfCoconeOfConeUnop F hc).lift s = (hc.desc (CategoryTheory.Limits.coconeOfConeUnop s)).unop
• CategoryTheory.Limits.isColimitCoconeOfConeLeftOp_desc 📋 Mathlib.CategoryTheory.Limits.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J Cᵒᵖ) {c : CategoryTheory.Limits.Cone F.leftOp} (hc : CategoryTheory.Limits.IsLimit c) (s : CategoryTheory.Limits.Cocone F) : (CategoryTheory.Limits.isColimitCoconeOfConeLeftOp F hc).desc s = (hc.lift (CategoryTheory.Limits.coneLeftOpOfCocone s)).op
• CategoryTheory.Limits.isColimitOfConeOfCoconeRightOp_desc 📋 Mathlib.CategoryTheory.Limits.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor Jᵒᵖ C) {c : CategoryTheory.Limits.Cocone F.rightOp} (hc : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.coneOfCoconeRightOp c)) (s : CategoryTheory.Limits.Cocone F.rightOp) : (CategoryTheory.Limits.isColimitOfConeOfCoconeRightOp F hc).desc s = (hc.lift (CategoryTheory.Limits.coneOfCoconeRightOp s)).op
• CategoryTheory.Limits.isLimitConeOfCoconeLeftOp_lift 📋 Mathlib.CategoryTheory.Limits.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J Cᵒᵖ) {c : CategoryTheory.Limits.Cocone F.leftOp} (hc : CategoryTheory.Limits.IsColimit c) (s : CategoryTheory.Limits.Cone F) : (CategoryTheory.Limits.isLimitConeOfCoconeLeftOp F hc).lift s = (hc.desc (CategoryTheory.Limits.coconeLeftOpOfCone s)).op
• CategoryTheory.Limits.isLimitOfCoconeOfConeRightOp_lift 📋 Mathlib.CategoryTheory.Limits.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor Jᵒᵖ C) {c : CategoryTheory.Limits.Cone F.rightOp} (hc : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.coconeOfConeRightOp c)) (s : CategoryTheory.Limits.Cone F.rightOp) : (CategoryTheory.Limits.isLimitOfCoconeOfConeRightOp F hc).lift s = (hc.desc (CategoryTheory.Limits.coconeOfConeRightOp s)).op
• CategoryTheory.Limits.isColimitOfConeUnopOfCocone_desc 📋 Mathlib.CategoryTheory.Limits.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ) {c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.coneUnopOfCocone c)) (s : CategoryTheory.Limits.Cocone F) : (CategoryTheory.Limits.isColimitOfConeUnopOfCocone F hc).desc s = (hc.lift (CategoryTheory.Limits.coneUnopOfCocone s)).op
• CategoryTheory.Limits.isLimitOfCoconeUnopOfCone_lift 📋 Mathlib.CategoryTheory.Limits.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ) {c : CategoryTheory.Limits.Cone F} (hc : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.coconeUnopOfCone c)) (s : CategoryTheory.Limits.Cone F) : (CategoryTheory.Limits.isLimitOfCoconeUnopOfCone F hc).lift s = (hc.desc (CategoryTheory.Limits.coconeUnopOfCone s)).op
• AddCommGrpCat.Colimits.Quot.desc_toCocone_desc 📋 Mathlib.Algebra.Category.Grp.Colimits
  {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J AddCommGrpCat) (c : CategoryTheory.Limits.Cocone F) [DecidableEq J] {A : Type w} [AddCommGroup A] (f : AddCommGrpCat.Colimits.Quot F →+ A) (hc : CategoryTheory.Limits.IsColimit c) : (AddCommGrpCat.Hom.hom (hc.desc (AddCommGrpCat.Colimits.toCocone F f))).comp (AddCommGrpCat.Colimits.Quot.desc F c) = f
• AddCommGrpCat.Colimits.Quot.desc_toCocone_desc_app 📋 Mathlib.Algebra.Category.Grp.Colimits
  {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J AddCommGrpCat) (c : CategoryTheory.Limits.Cocone F) [DecidableEq J] {A : Type w} [AddCommGroup A] (f : AddCommGrpCat.Colimits.Quot F →+ A) (hc : CategoryTheory.Limits.IsColimit c) (x : AddCommGrpCat.Colimits.Quot F) : (CategoryTheory.ConcreteCategory.hom (hc.desc (AddCommGrpCat.Colimits.toCocone F f))) ((AddCommGrpCat.Colimits.Quot.desc F c) x) = f x
• CommRingCat.coproductCoconeIsColimit_desc 📋 Mathlib.Algebra.Category.Ring.Constructions
  (A B : CommRingCat) (s : CategoryTheory.Limits.BinaryCofan A B) : (A.coproductCoconeIsColimit B).desc s = CommRingCat.ofHom (Algebra.TensorProduct.lift (CommRingCat.Hom.hom s.inl).toIntAlgHom (CommRingCat.Hom.hom s.inr).toIntAlgHom ⋯).toRingHom
• CategoryTheory.Comma.coconeOfPreserves_pt_hom 📋 Mathlib.CategoryTheory.Limits.Comma
  {J : Type w} [CategoryTheory.Category.{w', w} J] {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} (F : CategoryTheory.Functor J (CategoryTheory.Comma L R)) [CategoryTheory.Limits.PreservesColimit (F.comp (CategoryTheory.Comma.fst L R)) L] {c₁ : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.Comma.fst L R))} (t₁ : CategoryTheory.Limits.IsColimit c₁) (c₂ : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.Comma.snd L R))) : (CategoryTheory.Comma.coconeOfPreserves F t₁ c₂).pt.hom = (CategoryTheory.Limits.isColimitOfPreserves L t₁).desc (CategoryTheory.Comma.colimitAuxiliaryCocone F c₂)
• CategoryTheory.Comma.coconeOfPreserves_ι_app_left 📋 Mathlib.CategoryTheory.Limits.Comma
  {J : Type w} [CategoryTheory.Category.{w', w} J] {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} (F : CategoryTheory.Functor J (CategoryTheory.Comma L R)) [CategoryTheory.Limits.PreservesColimit (F.comp (CategoryTheory.Comma.fst L R)) L] {c₁ : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.Comma.fst L R))} (t₁ : CategoryTheory.Limits.IsColimit c₁) (c₂ : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.Comma.snd L R))) (j : J) : ((CategoryTheory.Comma.coconeOfPreserves F t₁ c₂).ι.app j).left = c₁.ι.app j
• CategoryTheory.Comma.coconeOfPreserves_ι_app_right 📋 Mathlib.CategoryTheory.Limits.Comma
  {J : Type w} [CategoryTheory.Category.{w', w} J] {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} (F : CategoryTheory.Functor J (CategoryTheory.Comma L R)) [CategoryTheory.Limits.PreservesColimit (F.comp (CategoryTheory.Comma.fst L R)) L] {c₁ : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.Comma.fst L R))} (t₁ : CategoryTheory.Limits.IsColimit c₁) (c₂ : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.Comma.snd L R))) (j : J) : ((CategoryTheory.Comma.coconeOfPreserves F t₁ c₂).ι.app j).right = c₂.ι.app j
• CategoryTheory.WithInitial.isColimitEquiv_apply_desc_right 📋 Mathlib.CategoryTheory.WithTerminal.Cone
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type w} [CategoryTheory.Category.{w', w} J] {X : C} {K : CategoryTheory.Functor J (CategoryTheory.Under X)} {t : CategoryTheory.Limits.Cocone K} (P : CategoryTheory.Limits.IsColimit (CategoryTheory.WithInitial.coconeEquiv.functor.obj t)) (s : CategoryTheory.Limits.Cocone K) : ((CategoryTheory.WithInitial.isColimitEquiv P).desc s).right = ((CategoryTheory.Limits.IsColimit.ofLeftAdjoint CategoryTheory.WithInitial.coconeEquiv.symm.toAdjunction P).desc s).right
• CategoryTheory.WithInitial.isColimitEquiv_symm_apply_desc 📋 Mathlib.CategoryTheory.WithTerminal.Cone
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type w} [CategoryTheory.Category.{w', w} J] {X : C} {K : CategoryTheory.Functor J (CategoryTheory.Under X)} {t : CategoryTheory.Limits.Cocone K} (t✝ : CategoryTheory.Limits.IsColimit t) (s : CategoryTheory.Limits.Cocone (CategoryTheory.WithInitial.liftFromUnder.obj K)) : (CategoryTheory.WithInitial.isColimitEquiv.symm t✝).desc s = ((CategoryTheory.WithInitial.coconeEquiv.toAdjunction.homEquiv' s t) (t✝.descCoconeMorphism (CategoryTheory.WithInitial.coconeEquiv.inverse.obj s))).hom
• CategoryTheory.MorphismProperty.colimitsOfShape.mk 📋 Mathlib.CategoryTheory.MorphismProperty.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C} {J : Type u_1} [CategoryTheory.Category.{v_1, u_1} J] (X₁ X₂ : CategoryTheory.Functor J C) (c₁ : CategoryTheory.Limits.Cocone X₁) (c₂ : CategoryTheory.Limits.Cocone X₂) (h₁ : CategoryTheory.Limits.IsColimit c₁) (h₂ : CategoryTheory.Limits.IsColimit c₂) (f : X₁ ⟶ X₂) : W.functorCategory J f → W.colimitsOfShape J (h₁.desc { pt := c₂.pt, ι := CategoryTheory.CategoryStruct.comp f c₂.ι })
• CategoryTheory.ShortComplex.RightHomologyData.wι 📋 Mathlib.Algebra.Homology.ShortComplex.RightHomology
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (self : S.RightHomologyData) : CategoryTheory.CategoryStruct.comp self.ι (self.hp.desc (CategoryTheory.Limits.CokernelCofork.ofπ S.g ⋯)) = 0
• CategoryTheory.ShortComplex.RightHomologyData.wι_assoc 📋 Mathlib.Algebra.Homology.ShortComplex.RightHomology
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (self : S.RightHomologyData) {Z : C} (h : (CategoryTheory.Limits.CokernelCofork.ofπ S.g ⋯).pt ⟶ Z) : CategoryTheory.CategoryStruct.comp self.ι (CategoryTheory.CategoryStruct.comp (self.hp.desc (CategoryTheory.Limits.CokernelCofork.ofπ S.g ⋯)) h) = CategoryTheory.CategoryStruct.comp 0 h
• CategoryTheory.ShortComplex.RightHomologyData.hι 📋 Mathlib.Algebra.Homology.ShortComplex.RightHomology
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (self : S.RightHomologyData) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι self.ι ⋯)
• CategoryTheory.ShortComplex.RightHomologyData.mk 📋 Mathlib.Algebra.Homology.ShortComplex.RightHomology
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (Q H : C) (p : S.X₂ ⟶ Q) (ι : H ⟶ Q) (wp : CategoryTheory.CategoryStruct.comp S.f p = 0) (hp : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ p wp)) (wι : CategoryTheory.CategoryStruct.comp ι (hp.desc (CategoryTheory.Limits.CokernelCofork.ofπ S.g ⋯)) = 0) (hι : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι ι wι)) : S.RightHomologyData
• CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.g'_eq 📋 Mathlib.Algebra.Homology.ShortComplex.Abelian
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) {cc : CategoryTheory.Limits.CokernelCofork S.f} (hcc : CategoryTheory.Limits.IsColimit cc) : hcc.desc (CategoryTheory.Limits.CokernelCofork.ofπ S.g ⋯) = CategoryTheory.CategoryStruct.comp (S.isoOpcyclesOfIsColimit hcc).hom S.fromOpcycles
• CategoryTheory.Limits.desc_op_comp_opCoproductIsoProduct'_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} {c : CategoryTheory.Limits.Cofan Z} {f : CategoryTheory.Limits.Fan fun x => Opposite.op (Z x)} (hc : CategoryTheory.Limits.IsColimit c) (hf : CategoryTheory.Limits.IsLimit f) (c' : CategoryTheory.Limits.Cofan Z) : CategoryTheory.CategoryStruct.comp (hc.desc c').op (CategoryTheory.Limits.opCoproductIsoProduct' hc hf).hom = hf.lift c'.op
• CategoryTheory.Limits.opProductIsoCoproduct'_inv_comp_lift 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} {f : CategoryTheory.Limits.Fan Z} {c : CategoryTheory.Limits.Cofan fun x => Opposite.op (Z x)} (hf : CategoryTheory.Limits.IsLimit f) (hc : CategoryTheory.Limits.IsColimit c) (f' : CategoryTheory.Limits.Fan Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.opProductIsoCoproduct' hf hc).inv (hf.lift f').op = hc.desc f'.op
• CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetColimitCocone_isColimit_desc 📋 Mathlib.CategoryTheory.Limits.Constructions.Filtered
  {C : Type u} [CategoryTheory.Category.{v, u} C] {α : Type w} [CategoryTheory.Limits.HasFiniteCoproducts C] [CategoryTheory.Limits.HasColimitsOfShape (Finset (CategoryTheory.Discrete α)) C] (F : CategoryTheory.Functor (CategoryTheory.Discrete α) C) (s : CategoryTheory.Limits.Cocone F) : (CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetColimitCocone F).isColimit.desc s = CategoryTheory.Limits.colimit.desc (CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetObj F) { pt := s.pt, ι := { app := fun x => CategoryTheory.Limits.Sigma.desc fun x_1 => s.ι.app ↑x_1, naturality := ⋯ } }
• CategoryTheory.Functor.isColimitCoconeOfIsLeftKanExtension_desc 📋 Mathlib.CategoryTheory.Functor.KanExtension.Basic
  {C : Type u_1} {H : Type u_3} {D : Type u_5} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_3, u_3} H] [CategoryTheory.Category.{v_5, u_5} D] (F' : CategoryTheory.Functor D H) {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} (α : F ⟶ L.comp F') [F'.IsLeftKanExtension α] {c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.Limits.IsColimit c) (s : CategoryTheory.Limits.Cocone F') : (F'.isColimitCoconeOfIsLeftKanExtension α hc).desc s = hc.desc { pt := s.1, ι := CategoryTheory.CategoryStruct.comp α (L.whiskerLeft s.ι) }
• CategoryTheory.Limits.Types.binaryCoproductColimit_desc 📋 Mathlib.CategoryTheory.Limits.Types.Coproducts
  (X Y : Type u) (s : CategoryTheory.Limits.BinaryCofan X Y) : (CategoryTheory.Limits.Types.binaryCoproductColimit X Y).desc s = TypeCat.ofHom (Sum.elim ⇑(CategoryTheory.ConcreteCategory.hom s.inl) ⇑(CategoryTheory.ConcreteCategory.hom s.inr))
• CategoryTheory.Limits.Multicofork.IsColimit.mk_desc 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape} {I : CategoryTheory.Limits.MultispanIndex J C} (K : CategoryTheory.Limits.Multicofork I) (desc : (E : CategoryTheory.Limits.Multicofork I) → K.pt ⟶ E.pt) (fac : ∀ (E : CategoryTheory.Limits.Multicofork I) (i : J.R), CategoryTheory.CategoryStruct.comp (K.π i) (desc E) = E.π i) (uniq : ∀ (E : CategoryTheory.Limits.Multicofork I) (m : K.pt ⟶ E.pt), (∀ (i : J.R), CategoryTheory.CategoryStruct.comp (K.π i) m = E.π i) → m = desc E) (E : CategoryTheory.Limits.Multicofork I) : (CategoryTheory.Limits.Multicofork.IsColimit.mk K desc fac uniq).desc E = desc E
• CategoryTheory.Comonad.ForgetCreatesColimits'.coconePoint_a 📋 Mathlib.CategoryTheory.Monad.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [CategoryTheory.Category.{v, u} J] {T : CategoryTheory.Comonad C} (D : CategoryTheory.Functor J T.Coalgebra) (c : CategoryTheory.Limits.Cocone (D.comp T.forget)) (t : CategoryTheory.Limits.IsColimit c) : (CategoryTheory.Comonad.ForgetCreatesColimits'.coconePoint D c t).a = t.desc (CategoryTheory.Comonad.ForgetCreatesColimits'.newCocone D c)
• CategoryTheory.Comonad.ForgetCreatesColimits'.liftedCoconeIsColimit_desc_f 📋 Mathlib.CategoryTheory.Monad.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [CategoryTheory.Category.{v, u} J] {T : CategoryTheory.Comonad C} (D : CategoryTheory.Functor J T.Coalgebra) (c : CategoryTheory.Limits.Cocone (D.comp T.forget)) (t : CategoryTheory.Limits.IsColimit c) (s : CategoryTheory.Limits.Cocone D) : ((CategoryTheory.Comonad.ForgetCreatesColimits'.liftedCoconeIsColimit D c t).desc s).f = t.desc (T.forget.mapCocone s)
• CategoryTheory.Monad.ForgetCreatesColimits.liftedCoconeIsColimit_desc_f 📋 Mathlib.CategoryTheory.Monad.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u} [CategoryTheory.Category.{v, u} J] {D : CategoryTheory.Functor J T.Algebra} (c : CategoryTheory.Limits.Cocone (D.comp T.forget)) (t : CategoryTheory.Limits.IsColimit c) [CategoryTheory.Limits.PreservesColimit (D.comp T.forget) T.toFunctor] [CategoryTheory.Limits.PreservesColimit ((D.comp T.forget).comp T.toFunctor) T.toFunctor] (s : CategoryTheory.Limits.Cocone D) : ((CategoryTheory.Monad.ForgetCreatesColimits.liftedCoconeIsColimit c t).desc s).f = t.desc (T.forget.mapCocone s)
• HomologicalComplex.extend.rightHomologyData.kernelFork 📋 Mathlib.Algebra.Homology.Embedding.ExtendHomology
  {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c) (e : c.Embedding c') {i j k : ι} {i' j' k' : ι'} (hj' : e.f j = j') (hi : c.prev j = i) (hi' : c'.prev j' = i') (hk : c.next j = k) (hk' : c'.next j' = k') (cocone : CategoryTheory.Limits.CokernelCofork (K.d i j)) (hcocone : CategoryTheory.Limits.IsColimit cocone) (cone : CategoryTheory.Limits.KernelFork (hcocone.desc (CategoryTheory.Limits.CokernelCofork.ofπ (K.d j k) ⋯))) : CategoryTheory.Limits.KernelFork ((HomologicalComplex.extend.rightHomologyData.isColimitCokernelCofork K e hj' hi hi' cocone hcocone).desc (CategoryTheory.Limits.CokernelCofork.ofπ ((K.extend e).d j' k') ⋯))
• HomologicalComplex.extend.rightHomologyData.d_comp_desc_eq_zero_iff 📋 Mathlib.Algebra.Homology.Embedding.ExtendHomology
  {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c) (e : c.Embedding c') {i j k : ι} {i' j' k' : ι'} (hj' : e.f j = j') (hi : c.prev j = i) (hi' : c'.prev j' = i') (hk : c.next j = k) (hk' : c'.next j' = k') (cocone : CategoryTheory.Limits.CokernelCofork (K.d i j)) (hcocone : CategoryTheory.Limits.IsColimit cocone) ⦃W : C⦄ (φ : W ⟶ cocone.pt) : CategoryTheory.CategoryStruct.comp φ (hcocone.desc (CategoryTheory.Limits.CokernelCofork.ofπ (K.d j k) ⋯)) = 0 ↔ CategoryTheory.CategoryStruct.comp φ ((HomologicalComplex.extend.rightHomologyData.isColimitCokernelCofork K e hj' hi hi' cocone hcocone).desc (CategoryTheory.Limits.CokernelCofork.ofπ ((K.extend e).d j' k') ⋯)) = 0
• HomologicalComplex.extend.rightHomologyData.isLimitKernelFork 📋 Mathlib.Algebra.Homology.Embedding.ExtendHomology
  {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c) (e : c.Embedding c') {i j k : ι} {i' j' k' : ι'} (hj' : e.f j = j') (hi : c.prev j = i) (hi' : c'.prev j' = i') (hk : c.next j = k) (hk' : c'.next j' = k') (cocone : CategoryTheory.Limits.CokernelCofork (K.d i j)) (hcocone : CategoryTheory.Limits.IsColimit cocone) (cone : CategoryTheory.Limits.KernelFork (hcocone.desc (CategoryTheory.Limits.CokernelCofork.ofπ (K.d j k) ⋯))) (hcone : CategoryTheory.Limits.IsLimit cone) : CategoryTheory.Limits.IsLimit (HomologicalComplex.extend.rightHomologyData.kernelFork K e hj' hi hi' hk hk' cocone hcocone cone)
• CategoryTheory.Limits.coconeOfCoconeUncurry_ι_app 📋 Mathlib.CategoryTheory.Limits.Fubini
  {J : Type u_1} {K : Type u_2} [CategoryTheory.Category.{v_1, u_1} J] [CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [CategoryTheory.Category.{v_3, u_3} C] {F : CategoryTheory.Functor J (CategoryTheory.Functor K C)} {D : CategoryTheory.Limits.DiagramOfCocones F} (Q : (j : J) → CategoryTheory.Limits.IsColimit (D.obj j)) (c : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.uncurry.obj F)) (j : J) : (CategoryTheory.Limits.coconeOfCoconeUncurry Q c).ι.app j = (Q j).desc { pt := c.pt, ι := { app := fun k => c.ι.app (j, k), naturality := ⋯ } }
• CategoryTheory.Limits.coconeOfCoconeCurry_ι_app 📋 Mathlib.CategoryTheory.Limits.Fubini
  {J : Type u_1} {K : Type u_2} [CategoryTheory.Category.{v_1, u_1} J] [CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [CategoryTheory.Category.{v_3, u_3} C] (G : CategoryTheory.Functor (J × K) C) {D : CategoryTheory.Limits.DiagramOfCocones (CategoryTheory.Functor.curry.obj G)} (Q : (j : J) → CategoryTheory.Limits.IsColimit (D.obj j)) (c : CategoryTheory.Limits.Cocone G) (j : J) : (CategoryTheory.Limits.coconeOfCoconeCurry G Q c).ι.app j = (Q j).desc { pt := c.pt, ι := { app := fun k => c.ι.app (j, k), naturality := ⋯ } }
• CategoryTheory.Limits.CompleteLattice.finiteColimitCocone_isColimit_desc 📋 Mathlib.CategoryTheory.Limits.Lattice
  {α : Type u} {J : Type w} [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] [SemilatticeSup α] [OrderBot α] (F : CategoryTheory.Functor J α) (s : CategoryTheory.Limits.Cocone F) : (CategoryTheory.Limits.CompleteLattice.finiteColimitCocone F).isColimit.desc s = CategoryTheory.homOfLE ⋯
• CategoryTheory.Limits.CompleteLattice.colimitCocone_isColimit_desc 📋 Mathlib.CategoryTheory.Limits.Lattice
  {α : Type u} [CompleteLattice α] {J : Type w} [CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor J α) (s : CategoryTheory.Limits.Cocone F) : (CategoryTheory.Limits.CompleteLattice.colimitCocone F).isColimit.desc s = CategoryTheory.homOfLE ⋯
• CategoryTheory.Limits.IsColimit.pushoutCoconeEquivBinaryCofanFunctor_desc_right 📋 Mathlib.CategoryTheory.Limits.Constructions.Over.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} {c : CategoryTheory.Limits.PushoutCocone f g} (hc : CategoryTheory.Limits.IsColimit c) (s : CategoryTheory.Limits.BinaryCofan (CategoryTheory.Under.mk f) (CategoryTheory.Under.mk g)) : (hc.pushoutCoconeEquivBinaryCofanFunctor.desc s).right = hc.desc (CategoryTheory.Limits.PushoutCocone.mk (CategoryTheory.Under.Hom.right s.inl) (CategoryTheory.Under.Hom.right s.inr) ⋯)
• CategoryTheory.CostructuredArrow.isClosedUnderColimitsOfShape 📋 Mathlib.CategoryTheory.Limits.MorphismProperty
  {T : Type u_1} [CategoryTheory.Category.{v_1, u_1} T] {A : Type u_2} [CategoryTheory.Category.{v_2, u_2} A] {L : CategoryTheory.Functor A T} {J : Type u_3} [CategoryTheory.Category.{v_3, u_3} J] {P : CategoryTheory.MorphismProperty T} [P.RespectsIso] [CategoryTheory.Limits.PreservesColimitsOfShape J L] [CategoryTheory.Limits.HasColimitsOfShape J A] (c : (D : CategoryTheory.Functor J T) → [CategoryTheory.Limits.HasColimit D] → CategoryTheory.Limits.Cocone D) (hc : (D : CategoryTheory.Functor J T) → [inst : CategoryTheory.Limits.HasColimit D] → CategoryTheory.Limits.IsColimit (c D)) (H : ∀ (D : CategoryTheory.Functor J T) [inst : CategoryTheory.Limits.HasColimit D] {X : T} (s : D ⟶ (CategoryTheory.Functor.const J).obj X), (∀ (j : J), P (s.app j)) → P ((hc D).desc { pt := X, ι := s })) (X : T) : (CategoryTheory.MorphismProperty.costructuredArrowObj L P).IsClosedUnderColimitsOfShape J
• CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows_isColimit_desc 📋 Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
  {C : Type u} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) {n : ℕ} (F : CategoryTheory.ComposableArrows C n) (hF : ∀ (i : Fin n), W (F.map (CategoryTheory.homOfLE ⋯))) (s : CategoryTheory.Limits.Cocone F) : (CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows W F hF).isColimit.desc s = s.ι.app (Fin.last n)
• CategoryTheory.Limits.IndObjectPresentation.yoneda_isColimit_desc 📋 Mathlib.CategoryTheory.Limits.Indization.IndObject
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) (s : CategoryTheory.Limits.Cocone ((CategoryTheory.Functor.fromPUnit X).comp CategoryTheory.yoneda)) : (CategoryTheory.Limits.IndObjectPresentation.yoneda X).isColimit.desc s = s.ι.app { as := PUnit.unit }
• CategoryTheory.Limits.IndObjectPresentation.extend_isColimit_desc_app_hom_apply 📋 Mathlib.CategoryTheory.Limits.Indization.IndObject
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A B : CategoryTheory.Functor Cᵒᵖ (Type v)} (P : CategoryTheory.Limits.IndObjectPresentation A) (η : A ⟶ B) [CategoryTheory.IsIso η] (s : CategoryTheory.Limits.Cocone (P.F.comp CategoryTheory.yoneda)) (X : Cᵒᵖ) (a✝ : (P.cocone.extend η).pt.obj X) : (CategoryTheory.ConcreteCategory.hom (((P.extend η).isColimit.desc s).app X)) a✝ = ((P.coconeIsColimit.desc s).app X).hom' ((CategoryTheory.inv (η.app X)).hom' a✝)
• CategoryTheory.Monad.beckCoequalizer_desc 📋 Mathlib.CategoryTheory.Monad.Coequalizer
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (X : T.Algebra) (s : CategoryTheory.Limits.Cofork (T.map X.a) (T.μ.app X.A)) : (CategoryTheory.Monad.beckCoequalizer X).desc s = CategoryTheory.CategoryStruct.comp (T.η.app X.A) s.π
• CategoryTheory.effectiveEpiStructIsColimitDescOfEffectiveEpiFamily 📋 Mathlib.CategoryTheory.EffectiveEpi.Coproduct
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {B : C} {α : Type u_2} (X : α → C) (c : CategoryTheory.Limits.Cofan X) (hc : CategoryTheory.Limits.IsColimit c) (π : (a : α) → X a ⟶ B) [CategoryTheory.EffectiveEpiFamily X π] : CategoryTheory.EffectiveEpiStruct (hc.desc (CategoryTheory.Limits.Cofan.mk B π))
• CategoryTheory.Limits.FormalCoproduct.isColimitCofan_desc_f 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (𝒜 : Type w) (f : 𝒜 → CategoryTheory.Limits.FormalCoproduct C) (t : CategoryTheory.Limits.Cofan f) (p : (CategoryTheory.Limits.FormalCoproduct.cofan 𝒜 f).pt.I) : ((CategoryTheory.Limits.FormalCoproduct.isColimitCofan 𝒜 f).desc t).f p = (t.inj p.fst).f p.snd
• CategoryTheory.Limits.FormalCoproduct.isColimitCofan_desc_φ 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (𝒜 : Type w) (f : 𝒜 → CategoryTheory.Limits.FormalCoproduct C) (t : CategoryTheory.Limits.Cofan f) (p : (CategoryTheory.Limits.FormalCoproduct.cofan 𝒜 f).pt.I) : ((CategoryTheory.Limits.FormalCoproduct.isColimitCofan 𝒜 f).desc t).φ p = (t.inj p.fst).φ p.snd
• CategoryTheory.FunctorToTypes.binaryCoproductColimit_desc 📋 Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
  {C : Type u} [CategoryTheory.Category.{v, u} C] (F G : CategoryTheory.Functor C (Type w)) (s : CategoryTheory.Limits.BinaryCofan F G) : (CategoryTheory.FunctorToTypes.binaryCoproductColimit F G).desc s = CategoryTheory.FunctorToTypes.coprod.desc s.inl s.inr
• CategoryTheory.Presheaf.coconeCompShrinkYonedaHomEquiv_symm_apply 📋 Mathlib.CategoryTheory.Limits.Types.PreservesLimit
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u'} [CategoryTheory.Category.{v', u'} J] [CategoryTheory.LocallySmall.{w, v, u} C] {F : CategoryTheory.Functor J Cᵒᵖ} {c' : CategoryTheory.Limits.Cocone (F.leftOp.comp CategoryTheory.shrinkYoneda.{w, v, u})} (hc' : CategoryTheory.Limits.IsColimit c') {P : CategoryTheory.Functor Cᵒᵖ (Type w)} (s : ↑(F.comp P).sections) : (CategoryTheory.Presheaf.coconeCompShrinkYonedaHomEquiv hc').symm s = hc'.desc { pt := P, ι := { app := fun j => CategoryTheory.shrinkYonedaEquiv.symm (↑s (Opposite.unop j)), naturality := ⋯ } }
• CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction_unit_f 📋 Mathlib.CategoryTheory.Monad.Monadicity
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {G : CategoryTheory.Functor D C} {F : CategoryTheory.Functor C D} {adj : F ⊣ G} [∀ (A : adj.toMonad.Algebra), CategoryTheory.Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))] (A : adj.toMonad.Algebra) : ((CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction adj).unit.app A).f = (CategoryTheory.Monad.beckCoequalizer A).desc (CategoryTheory.Monad.MonadicityInternal.unitCofork A)
• LightCondensed.isColimitLocallyConstantPresheafDiagram_desc_apply 📋 Mathlib.Condensed.Discrete.Colimit
  (X : Type u) (S : LightProfinite) (s : CategoryTheory.Limits.Cocone (S.diagram.rightOp.comp (LightCondensed.locallyConstantPresheaf X))) (n : ℕ) (f : LocallyConstant (↑(S.diagram.obj (Opposite.op n)).toTop) X) : (CategoryTheory.ConcreteCategory.hom ((LightCondensed.isColimitLocallyConstantPresheafDiagram X S).desc s)) (LocallyConstant.comap (TopCat.Hom.hom (S.asLimitCone.π.app (Opposite.op n)).hom) f) = (CategoryTheory.ConcreteCategory.hom (s.ι.app n)) f
• Condensed.isColimitLocallyConstantPresheaf_desc_apply 📋 Mathlib.Condensed.Discrete.Colimit
  {I : Type u} [CategoryTheory.Category.{u, u} I] [CategoryTheory.IsCofiltered I] {F : CategoryTheory.Functor I FintypeCat} (c : CategoryTheory.Limits.Cone (F.comp FintypeCat.toProfinite)) (X : Type (u + 1)) (hc : CategoryTheory.Limits.IsLimit c) [∀ (i : I), CategoryTheory.Epi (c.π.app i)] (s : CategoryTheory.Limits.Cocone ((F.comp FintypeCat.toProfinite).op.comp (Condensed.locallyConstantPresheaf X))) (i : I) (f : LocallyConstant (↑(FintypeCat.toProfinite.obj (F.obj i)).toTop) X) : (CategoryTheory.ConcreteCategory.hom ((Condensed.isColimitLocallyConstantPresheaf c X hc).desc s)) (LocallyConstant.comap (TopCat.Hom.hom (c.π.app i).hom) f) = (CategoryTheory.ConcreteCategory.hom (s.ι.app (Opposite.op i))) f
• LightCondensed.isColimitLocallyConstantPresheaf_desc_apply 📋 Mathlib.Condensed.Discrete.Colimit
  {F : CategoryTheory.Functor ℕᵒᵖ FintypeCat} (c : CategoryTheory.Limits.Cone (F.comp FintypeCat.toLightProfinite)) (X : Type u) (hc : CategoryTheory.Limits.IsLimit c) [∀ (i : ℕᵒᵖ), CategoryTheory.Epi (c.π.app i)] (s : CategoryTheory.Limits.Cocone ((F.comp FintypeCat.toLightProfinite).op.comp (LightCondensed.locallyConstantPresheaf X))) (n : ℕᵒᵖ) (f : LocallyConstant (↑(FintypeCat.toLightProfinite.obj (F.obj n)).toTop) X) : (CategoryTheory.ConcreteCategory.hom ((LightCondensed.isColimitLocallyConstantPresheaf c X hc).desc s)) (LocallyConstant.comap (TopCat.Hom.hom (c.π.app n).hom) f) = (CategoryTheory.ConcreteCategory.hom (s.ι.app (Opposite.op n))) f
• Condensed.isColimitLocallyConstantPresheafDiagram_desc_apply 📋 Mathlib.Condensed.Discrete.Colimit
  (X : Type (u + 1)) (S : Profinite) (s : CategoryTheory.Limits.Cocone (S.diagram.op.comp (Condensed.locallyConstantPresheaf X))) (i : DiscreteQuotient ↑S.toTop) (f : LocallyConstant (↑(S.diagram.obj i).toTop) X) : (CategoryTheory.ConcreteCategory.hom ((Condensed.isColimitLocallyConstantPresheafDiagram X S).desc s)) (LocallyConstant.comap (TopCat.Hom.hom (S.asLimitCone.π.app i).hom) f) = (CategoryTheory.ConcreteCategory.hom (s.ι.app (Opposite.op i))) 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