Loogle!

Result

Found 134 declarations mentioning CategoryTheory.Limits.colim.

• CategoryTheory.Limits.colim 📋 Mathlib.CategoryTheory.Limits.HasLimits
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimitsOfShape J C] : CategoryTheory.Functor (CategoryTheory.Functor J C) C
• CategoryTheory.Limits.instIsLeftAdjointFunctorColim 📋 Mathlib.CategoryTheory.Limits.HasLimits
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimitsOfShape J C] : CategoryTheory.Limits.colim.IsLeftAdjoint
• CategoryTheory.Limits.colimConstAdj 📋 Mathlib.CategoryTheory.Limits.HasLimits
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimitsOfShape J C] : CategoryTheory.Limits.colim ⊣ CategoryTheory.Functor.const J
• CategoryTheory.Limits.colim_obj 📋 Mathlib.CategoryTheory.Limits.HasLimits
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimitsOfShape J C] (F : CategoryTheory.Functor J C) : CategoryTheory.Limits.colim.obj F = CategoryTheory.Limits.colimit F
• CategoryTheory.Limits.colim.ι 📋 Mathlib.CategoryTheory.Limits.HasLimits
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimitsOfShape J C] (j : J) : (CategoryTheory.evaluation J C).obj j ⟶ CategoryTheory.Limits.colim
• CategoryTheory.Limits.colim.ι_app 📋 Mathlib.CategoryTheory.Limits.HasLimits
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimitsOfShape J C] (j : J) (F : CategoryTheory.Functor J C) : (CategoryTheory.Limits.colim.ι j).app F = CategoryTheory.Limits.colimit.ι F j
• CategoryTheory.Limits.colimMap_eq 📋 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.HasColimitsOfShape J C] {G : CategoryTheory.Functor J C} (α : F ⟶ G) : CategoryTheory.Limits.colimMap α = CategoryTheory.Limits.colim.map α
• CategoryTheory.Limits.colim_map 📋 Mathlib.CategoryTheory.Limits.HasLimits
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimitsOfShape J C] {X✝ Y✝ : CategoryTheory.Functor J C} (α : X✝ ⟶ Y✝) : CategoryTheory.Limits.colim.map α = CategoryTheory.Limits.colimMap α
• CategoryTheory.Limits.colimit.pre_id 📋 Mathlib.CategoryTheory.Limits.HasLimits
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimitsOfShape J C] (F : CategoryTheory.Functor J C) : CategoryTheory.Limits.colimit.pre F (CategoryTheory.Functor.id J) = CategoryTheory.Limits.colim.map F.leftUnitor.hom
• CategoryTheory.Limits.colimCoyoneda 📋 Mathlib.CategoryTheory.Limits.HasLimits
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimitsOfShape J C] : CategoryTheory.Limits.colim.op.comp (CategoryTheory.coyoneda.comp ((CategoryTheory.Functor.whiskeringRight C (Type v) (Type (max v u₁))).obj CategoryTheory.uliftFunctor.{u₁, v})) ≅ CategoryTheory.cocones J C
• CategoryTheory.Limits.colimit.ι_map 📋 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.HasColimitsOfShape J C] {G : CategoryTheory.Functor J C} (α : F ⟶ G) (j : J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F j) (CategoryTheory.Limits.colim.map α) = CategoryTheory.CategoryStruct.comp (α.app j) (CategoryTheory.Limits.colimit.ι G j)
• CategoryTheory.Limits.colimit.ι_map_assoc 📋 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.HasColimitsOfShape J C] {G : CategoryTheory.Functor J C} (α : F ⟶ G) (j : J) {Z : C} (h : CategoryTheory.Limits.colim.obj G ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colim.map α) h) = CategoryTheory.CategoryStruct.comp (α.app j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι G j) h)
• CategoryTheory.Limits.colimit.pre_map' 📋 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] [CategoryTheory.Limits.HasColimitsOfShape J C] [CategoryTheory.Limits.HasColimitsOfShape K C] (F : CategoryTheory.Functor J C) {E₁ E₂ : CategoryTheory.Functor K J} (α : E₁ ⟶ E₂) : CategoryTheory.Limits.colimit.pre F E₁ = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colim.map (CategoryTheory.Functor.whiskerRight α F)) (CategoryTheory.Limits.colimit.pre F E₂)
• CategoryTheory.Limits.colimit.pre_map 📋 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.HasColimitsOfShape J C] {G : CategoryTheory.Functor J C} (α : F ⟶ G) [CategoryTheory.Limits.HasColimitsOfShape K C] (E : CategoryTheory.Functor K J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.pre F E) (CategoryTheory.Limits.colim.map α) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colim.map (E.whiskerLeft α)) (CategoryTheory.Limits.colimit.pre G E)
• CategoryTheory.Limits.colimit.map_post 📋 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.HasColimitsOfShape J C] {G : CategoryTheory.Functor J C} (α : F ⟶ G) {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Limits.HasColimitsOfShape J D] (H : CategoryTheory.Functor C D) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.post F H) (H.map (CategoryTheory.Limits.colim.map α)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colim.map (CategoryTheory.Functor.whiskerRight α H)) (CategoryTheory.Limits.colimit.post G H)
• CategoryTheory.Limits.piEquivalenceFunctorDiscrete_functor_comp_colim 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproductsOfShape α C] : (CategoryTheory.piEquivalenceFunctorDiscrete α C).functor.comp CategoryTheory.Limits.colim = CategoryTheory.Limits.Sigma.functor α
• CategoryTheory.Limits.piEquivalenceFunctorDiscreteCompColim 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  (α : Type w₂) {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproductsOfShape α C] : (CategoryTheory.piEquivalenceFunctorDiscrete α C).functor.comp CategoryTheory.Limits.colim ≅ CategoryTheory.Limits.Sigma.functor α
• CategoryTheory.Limits.piEquivalenceFunctorDiscreteCompColim_hom_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  (α : Type w₂) {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproductsOfShape α C] (X : α → C) : (CategoryTheory.Limits.piEquivalenceFunctorDiscreteCompColim α).hom.app X = CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.colimit (CategoryTheory.Discrete.functor X))
• CategoryTheory.Limits.piEquivalenceFunctorDiscreteCompColim_inv_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  (α : Type w₂) {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproductsOfShape α C] (X : α → C) : (CategoryTheory.Limits.piEquivalenceFunctorDiscreteCompColim α).inv.app X = CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.colimit (CategoryTheory.Discrete.functor X))
• CategoryTheory.Limits.piEquivalenceFunctorDiscreteCompColim_comp_functorι 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproductsOfShape α C] (a : α) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.piEquivalenceFunctorDiscrete α C).functor.whiskerLeft (CategoryTheory.Limits.colim.ι { as := a })) (CategoryTheory.Limits.piEquivalenceFunctorDiscreteCompColim α).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.piEquivalenceFunctorDiscreteCompEvaluationIso C a).hom (CategoryTheory.Limits.Sigma.functorι a)
• CategoryTheory.Limits.piEquivalenceFunctorDiscreteCompColim_comp_functorι_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproductsOfShape α C] (a : α) {Z : CategoryTheory.Functor (α → C) C} (h : CategoryTheory.Limits.Sigma.functor α ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.piEquivalenceFunctorDiscrete α C).functor.whiskerLeft (CategoryTheory.Limits.colim.ι { as := a })) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.piEquivalenceFunctorDiscreteCompColim α).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.piEquivalenceFunctorDiscreteCompEvaluationIso C a).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.functorι a) h)
• CategoryTheory.Limits.HasBiproductsOfShape.colimIsoLim 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBiproductsOfShape J C] : CategoryTheory.Limits.colim ≅ CategoryTheory.Limits.lim
• CategoryTheory.Limits.HasBiproductsOfShape.colimIsoLim_hom_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBiproductsOfShape J C] (X : CategoryTheory.Functor (CategoryTheory.Discrete J) C) : CategoryTheory.Limits.HasBiproductsOfShape.colimIsoLim.hom.app X = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.isoColimit X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.desc (CategoryTheory.Limits.biproduct.ι fun j => X.obj { as := j })) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.lift (CategoryTheory.Limits.biproduct.π fun j => X.obj { as := j })) (CategoryTheory.Limits.Pi.isoLimit X).hom))
• CategoryTheory.Limits.HasBiproductsOfShape.colimIsoLim_inv_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBiproductsOfShape J C] (X : CategoryTheory.Functor (CategoryTheory.Discrete J) C) : CategoryTheory.Limits.HasBiproductsOfShape.colimIsoLim.inv.app X = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.isoLimit X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.lift (CategoryTheory.Limits.Pi.π fun j => X.obj { as := j })) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.desc (CategoryTheory.Limits.Sigma.ι fun j => X.obj { as := j })) (CategoryTheory.Limits.Sigma.isoColimit X).hom))
• CategoryTheory.Limits.colimit.ι_map_apply 📋 Mathlib.CategoryTheory.Limits.Types.Colimits
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor J C} [CategoryTheory.Limits.HasColimitsOfShape J C] {G : CategoryTheory.Functor J C} (α : F ⟶ G) (j : J) {F✝ : C → C → Type uF} {carrier : C → Type w} {instFunLike : (X Y : C) → FunLike (F✝ X Y) (carrier X) (carrier Y)} [inst : CategoryTheory.ConcreteCategory C F✝] (x : carrier (F.obj j)) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimMap α)) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimit.ι F j)) x) = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimit.ι G j)) ((CategoryTheory.ConcreteCategory.hom (α.app j)) x)
• CategoryTheory.Limits.Types.Colimit.ι_map_apply 📋 Mathlib.CategoryTheory.Limits.Types.Colimits
  {J : Type v} [CategoryTheory.Category.{w, v} J] {F G : CategoryTheory.Functor J (Type u)} [CategoryTheory.Limits.HasColimitsOfShape J (Type u)] (α : F ⟶ G) (j : J) (x : F.obj j) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colim.map α)) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimit.ι F j)) x) = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimit.ι G j)) ((CategoryTheory.ConcreteCategory.hom (α.app j)) x)
• CategoryTheory.preservesColimitNatIso 📋 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] [CategoryTheory.Limits.PreservesColimitsOfShape J G] [CategoryTheory.Limits.HasColimitsOfShape J D] [CategoryTheory.Limits.HasColimitsOfShape J C] : CategoryTheory.Limits.colim.comp G ≅ ((CategoryTheory.Functor.whiskeringRight J C D).obj G).comp CategoryTheory.Limits.colim
• CategoryTheory.preservesColimitNatIso_hom_app 📋 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] [CategoryTheory.Limits.PreservesColimitsOfShape J G] [CategoryTheory.Limits.HasColimitsOfShape J D] [CategoryTheory.Limits.HasColimitsOfShape J C] (X : CategoryTheory.Functor J C) : (CategoryTheory.preservesColimitNatIso G).hom.app X = (CategoryTheory.preservesColimitIso G X).hom
• CategoryTheory.preservesColimitNatIso_inv_app 📋 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] [CategoryTheory.Limits.PreservesColimitsOfShape J G] [CategoryTheory.Limits.HasColimitsOfShape J D] [CategoryTheory.Limits.HasColimitsOfShape J C] (X : CategoryTheory.Functor J C) : (CategoryTheory.preservesColimitNatIso G).inv.app X = (CategoryTheory.preservesColimitIso G X).inv
• CategoryTheory.Limits.pointwiseCocone_pt 📋 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] [CategoryTheory.Limits.HasColimitsOfShape J C] (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) : (CategoryTheory.Limits.pointwiseCocone F).pt = F.flip.comp CategoryTheory.Limits.colim
• CategoryTheory.Limits.colimitIsoFlipCompColim 📋 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] [CategoryTheory.Limits.HasColimitsOfShape J C] (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) : CategoryTheory.Limits.colimit F ≅ F.flip.comp CategoryTheory.Limits.colim
• CategoryTheory.Limits.colimitFlipIsoCompColim 📋 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] [CategoryTheory.Limits.HasColimitsOfShape J C] (F : CategoryTheory.Functor K (CategoryTheory.Functor J C)) : CategoryTheory.Limits.colimit F.flip ≅ F.comp CategoryTheory.Limits.colim
• CategoryTheory.Limits.colimitIsoSwapCompColim 📋 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] [CategoryTheory.Limits.HasColimitsOfShape J C] (G : CategoryTheory.Functor J (CategoryTheory.Functor K C)) : CategoryTheory.Limits.colimit G ≅ (CategoryTheory.Functor.curry.obj ((CategoryTheory.Prod.swap K J).comp (CategoryTheory.Functor.uncurry.obj G))).comp CategoryTheory.Limits.colim
• CategoryTheory.Limits.colimCompFlipIsoWhiskerColim 📋 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] [CategoryTheory.Limits.HasColimitsOfShape J C] : (CategoryTheory.flipFunctor K J C).comp CategoryTheory.Limits.colim ≅ (CategoryTheory.Functor.whiskeringRight K (CategoryTheory.Functor J C) C).obj CategoryTheory.Limits.colim
• CategoryTheory.Limits.colimIsoFlipCompWhiskerColim 📋 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] [CategoryTheory.Limits.HasColimitsOfShape J C] : CategoryTheory.Limits.colim ≅ (CategoryTheory.flipFunctor J K C).comp ((CategoryTheory.Functor.whiskeringRight K (CategoryTheory.Functor J C) C).obj CategoryTheory.Limits.colim)
• CategoryTheory.Limits.colimitIsoFlipCompColim_hom_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] [CategoryTheory.Limits.HasColimitsOfShape J C] (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) (X : K) : (CategoryTheory.Limits.colimitIsoFlipCompColim F).hom.app X = (CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation F X).hom
• CategoryTheory.Limits.colimitIsoFlipCompColim_inv_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] [CategoryTheory.Limits.HasColimitsOfShape J C] (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) (X : K) : (CategoryTheory.Limits.colimitIsoFlipCompColim F).inv.app X = (CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation F X).inv
• CategoryTheory.Limits.pointwiseCocone_ι_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] [CategoryTheory.Limits.HasColimitsOfShape J C] (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) (X : J) (Y : K) : ((CategoryTheory.Limits.pointwiseCocone F).ι.app X).app Y = CategoryTheory.Limits.colimit.ι (F.flip.obj Y) X
• CategoryTheory.Limits.colimitFlipIsoCompColim_hom_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] [CategoryTheory.Limits.HasColimitsOfShape J C] (F : CategoryTheory.Functor K (CategoryTheory.Functor J C)) (X : K) : (CategoryTheory.Limits.colimitFlipIsoCompColim F).hom.app X = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation F.flip X).hom (CategoryTheory.Limits.HasColimit.isoOfNatIso (CategoryTheory.flipCompEvaluation F X)).hom
• CategoryTheory.Limits.colimitFlipIsoCompColim_inv_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] [CategoryTheory.Limits.HasColimitsOfShape J C] (F : CategoryTheory.Functor K (CategoryTheory.Functor J C)) (X : K) : (CategoryTheory.Limits.colimitFlipIsoCompColim F).inv.app X = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.HasColimit.isoOfNatIso (CategoryTheory.flipCompEvaluation F X)).inv (CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation F.flip X).inv
• CategoryTheory.Limits.colimIsoFlipCompWhiskerColim_hom_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] [CategoryTheory.Limits.HasColimitsOfShape J C] (X : CategoryTheory.Functor J (CategoryTheory.Functor K C)) (X✝ : K) : (CategoryTheory.Limits.colimIsoFlipCompWhiskerColim.hom.app X).app X✝ = (CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation X X✝).hom
• CategoryTheory.Limits.colimIsoFlipCompWhiskerColim_inv_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] [CategoryTheory.Limits.HasColimitsOfShape J C] (X : CategoryTheory.Functor J (CategoryTheory.Functor K C)) (X✝ : K) : (CategoryTheory.Limits.colimIsoFlipCompWhiskerColim.inv.app X).app X✝ = (CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation X X✝).inv
• CategoryTheory.Limits.colimCompFlipIsoWhiskerColim_hom_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] [CategoryTheory.Limits.HasColimitsOfShape J C] (X : CategoryTheory.Functor K (CategoryTheory.Functor J C)) (X✝ : K) : (CategoryTheory.Limits.colimCompFlipIsoWhiskerColim.hom.app X).app X✝ = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation X.flip X✝).hom (CategoryTheory.Limits.HasColimit.isoOfNatIso (CategoryTheory.flipCompEvaluation X X✝)).hom
• CategoryTheory.Limits.colimCompFlipIsoWhiskerColim_inv_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] [CategoryTheory.Limits.HasColimitsOfShape J C] (X : CategoryTheory.Functor K (CategoryTheory.Functor J C)) (X✝ : K) : (CategoryTheory.Limits.colimCompFlipIsoWhiskerColim.inv.app X).app X✝ = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.HasColimit.isoOfNatIso (CategoryTheory.flipCompEvaluation X X✝)).inv (CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation X.flip X✝).inv
• CategoryTheory.Limits.colimitIsoSwapCompColim_hom_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] [CategoryTheory.Limits.HasColimitsOfShape J C] (G : CategoryTheory.Functor J (CategoryTheory.Functor K C)) (X : K) : (CategoryTheory.Limits.colimitIsoSwapCompColim G).hom.app X = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation G X).hom (CategoryTheory.Limits.colimMap (G.flipIsoCurrySwapUncurry.hom.app X))
• CategoryTheory.Limits.colimitIsoSwapCompColim_inv_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] [CategoryTheory.Limits.HasColimitsOfShape J C] (G : CategoryTheory.Functor J (CategoryTheory.Functor K C)) (X : K) : (CategoryTheory.Limits.colimitIsoSwapCompColim G).inv.app X = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimMap (G.flipIsoCurrySwapUncurry.inv.app X)) (CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation G X).inv
• CategoryTheory.Adjunction.colim_preservesColimits 📋 Mathlib.CategoryTheory.Adjunction.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [CategoryTheory.Category.{v, u} J] [CategoryTheory.Limits.HasColimitsOfShape J C] : CategoryTheory.Limits.PreservesColimits CategoryTheory.Limits.colim
• CategoryTheory.Limits.fiberwiseColimCompColimIso 📋 Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {H : Type u₂} [CategoryTheory.Category.{v₂, u₂} H] [∀ (c : C), CategoryTheory.Limits.HasColimitsOfShape (↑(F.obj c)) H] [CategoryTheory.Limits.HasColimitsOfShape C H] : (CategoryTheory.Limits.fiberwiseColim F H).comp CategoryTheory.Limits.colim ≅ CategoryTheory.Limits.colim
• CategoryTheory.Limits.fiberwiseColimCompEvaluationIso 📋 Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {H : Type u₂} [CategoryTheory.Category.{v₂, u₂} H] [∀ (c : C), CategoryTheory.Limits.HasColimitsOfShape (↑(F.obj c)) H] (c : C) : (CategoryTheory.Limits.fiberwiseColim F H).comp ((CategoryTheory.evaluation C H).obj c) ≅ ((CategoryTheory.Functor.whiskeringLeft (↑(F.obj c)) (CategoryTheory.Grothendieck F) H).obj (CategoryTheory.Grothendieck.ι F c)).comp CategoryTheory.Limits.colim
• CategoryTheory.Limits.fiberwiseColimCompColimIso_hom_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {H : Type u₂} [CategoryTheory.Category.{v₂, u₂} H] [∀ (c : C), CategoryTheory.Limits.HasColimitsOfShape (↑(F.obj c)) H] [CategoryTheory.Limits.HasColimitsOfShape C H] (X : CategoryTheory.Functor (CategoryTheory.Grothendieck F) H) : CategoryTheory.Limits.fiberwiseColimCompColimIso.hom.app X = (CategoryTheory.Limits.colimitFiberwiseColimitIso X).hom
• CategoryTheory.Limits.fiberwiseColimCompColimIso_inv_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {H : Type u₂} [CategoryTheory.Category.{v₂, u₂} H] [∀ (c : C), CategoryTheory.Limits.HasColimitsOfShape (↑(F.obj c)) H] [CategoryTheory.Limits.HasColimitsOfShape C H] (X : CategoryTheory.Functor (CategoryTheory.Grothendieck F) H) : CategoryTheory.Limits.fiberwiseColimCompColimIso.inv.app X = (CategoryTheory.Limits.colimitFiberwiseColimitIso X).inv
• CategoryTheory.Limits.fiberwiseColim_map_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor C CategoryTheory.Cat) (H : Type u₂) [CategoryTheory.Category.{v₂, u₂} H] [∀ (c : C), CategoryTheory.Limits.HasColimitsOfShape (↑(F.obj c)) H] {X✝ Y✝ : CategoryTheory.Functor (CategoryTheory.Grothendieck F) H} (α : X✝ ⟶ Y✝) (c : C) : ((CategoryTheory.Limits.fiberwiseColim F H).map α).app c = CategoryTheory.Limits.colim.map ((CategoryTheory.Grothendieck.ι F c).whiskerLeft α)
• CategoryTheory.Limits.fiberwiseColimCompEvaluationIso_hom_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {H : Type u₂} [CategoryTheory.Category.{v₂, u₂} H] [∀ (c : C), CategoryTheory.Limits.HasColimitsOfShape (↑(F.obj c)) H] (c : C) (X : CategoryTheory.Functor (CategoryTheory.Grothendieck F) H) : (CategoryTheory.Limits.fiberwiseColimCompEvaluationIso c).hom.app X = CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.colimit ((CategoryTheory.Grothendieck.ι F c).comp X))
• CategoryTheory.Limits.fiberwiseColimCompEvaluationIso_inv_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {H : Type u₂} [CategoryTheory.Category.{v₂, u₂} H] [∀ (c : C), CategoryTheory.Limits.HasColimitsOfShape (↑(F.obj c)) H] (c : C) (X : CategoryTheory.Functor (CategoryTheory.Grothendieck F) H) : (CategoryTheory.Limits.fiberwiseColimCompEvaluationIso c).inv.app X = CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.colimit ((CategoryTheory.Grothendieck.ι F c).comp X))
• CategoryTheory.Functor.Final.colimIso 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.Final] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] [CategoryTheory.Limits.HasColimitsOfShape D E] [CategoryTheory.Limits.HasColimitsOfShape C E] : ((CategoryTheory.Functor.whiskeringLeft C D E).obj F).comp CategoryTheory.Limits.colim ≅ CategoryTheory.Limits.colim
• CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetColimIso 📋 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] [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete α) C] : (CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinset C α).comp CategoryTheory.Limits.colim ≅ CategoryTheory.Limits.colim
• CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetEvaluationIso 📋 Mathlib.CategoryTheory.Limits.Constructions.Filtered
  {C : Type u} [CategoryTheory.Category.{v, u} C] {α : Type w} [CategoryTheory.Limits.HasFiniteCoproducts C] (I : Finset (CategoryTheory.Discrete α)) : (CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinset C α).comp ((CategoryTheory.evaluation (Finset (CategoryTheory.Discrete α)) C).obj I) ≅ ((CategoryTheory.Functor.whiskeringLeft (CategoryTheory.Discrete ↥I) (CategoryTheory.Discrete α) C).obj (CategoryTheory.Discrete.functor fun x => ↑x)).comp CategoryTheory.Limits.colim
• CategoryTheory.Functor.lanCompColimIso 📋 Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D) {H : Type u_3} [CategoryTheory.Category.{v_3, u_3} H] [∀ (F : CategoryTheory.Functor C H), L.HasLeftKanExtension F] [CategoryTheory.Limits.HasColimitsOfShape C H] [CategoryTheory.Limits.HasColimitsOfShape D H] : L.lan.comp CategoryTheory.Limits.colim ≅ CategoryTheory.Limits.colim
• CategoryTheory.Functor.lanCompColimIso_hom_app 📋 Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D) {H : Type u_3} [CategoryTheory.Category.{v_3, u_3} H] [∀ (F : CategoryTheory.Functor C H), L.HasLeftKanExtension F] [CategoryTheory.Limits.HasColimitsOfShape C H] [CategoryTheory.Limits.HasColimitsOfShape D H] (X : CategoryTheory.Functor C H) : L.lanCompColimIso.hom.app X = ((L.lan.obj X).colimitIsoOfIsLeftKanExtension (L.lanUnit.app X)).hom
• CategoryTheory.Functor.lanCompColimIso_inv_app 📋 Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D) {H : Type u_3} [CategoryTheory.Category.{v_3, u_3} H] [∀ (F : CategoryTheory.Functor C H), L.HasLeftKanExtension F] [CategoryTheory.Limits.HasColimitsOfShape C H] [CategoryTheory.Limits.HasColimitsOfShape D H] (X : CategoryTheory.Functor C H) : L.lanCompColimIso.inv.app X = ((L.lan.obj X).colimitIsoOfIsLeftKanExtension (L.lanUnit.app X)).inv
• CategoryTheory.Functor.Elements.shrinkYonedaCompWhiskeringLeftObjπCompColimIso 📋 Mathlib.CategoryTheory.Limits.Presheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.LocallySmall.{w, v₁, u₁} C] (F : CategoryTheory.Functor C (Type w)) [CategoryTheory.Limits.HasColimitsOfShape F.Elementsᵒᵖ (Type w)] : CategoryTheory.shrinkYoneda.{w, v₁, u₁}.comp (((CategoryTheory.Functor.whiskeringLeft F.Elementsᵒᵖ Cᵒᵖ (Type w)).obj (CategoryTheory.CategoryOfElements.π F).op).comp CategoryTheory.Limits.colim) ≅ F
• CategoryTheory.Functor.Elements.shrinkYonedaCompWhiskeringLeftObjπCompColimIso_inv_app_apply 📋 Mathlib.CategoryTheory.Limits.Presheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.LocallySmall.{w, v₁, u₁} C] (F : CategoryTheory.Functor C (Type w)) [CategoryTheory.Limits.HasColimitsOfShape F.Elementsᵒᵖ (Type w)] (u : F.Elements) : (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Functor.Elements.shrinkYonedaCompWhiskeringLeftObjπCompColimIso F).inv.app u.fst)) u.snd = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimit.ι ((CategoryTheory.CategoryOfElements.π F).op.comp (CategoryTheory.shrinkYoneda.{w, v₁, u₁}.obj u.fst)) (Opposite.op u))) (CategoryTheory.shrinkYonedaObjObjEquiv.symm (CategoryTheory.CategoryStruct.id (Opposite.unop ((CategoryTheory.CategoryOfElements.π F).op.obj (Opposite.op u)))))
• CategoryTheory.instPreservesLimitsOfShapeFunctorColim 📋 Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] [CategoryTheory.Limits.HasLimitsOfShape J C] [CategoryTheory.Limits.HasColimitsOfShape K C] [CategoryTheory.Limits.PreservesLimitsOfShape J CategoryTheory.Limits.colim] : CategoryTheory.Limits.PreservesLimitsOfShape J CategoryTheory.Limits.colim
• CategoryTheory.HasExactColimitsOfShape.mk 📋 Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
  {J : Type u'} [CategoryTheory.Category.{v', u'} J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimitsOfShape J C] (preservesFiniteLimits : CategoryTheory.Limits.PreservesFiniteLimits CategoryTheory.Limits.colim) : CategoryTheory.HasExactColimitsOfShape J C
• CategoryTheory.HasExactColimitsOfShape.preservesFiniteLimits 📋 Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
  {J : Type u'} {inst✝ : CategoryTheory.Category.{v', u'} J} {C : Type u} {inst✝¹ : CategoryTheory.Category.{v, u} C} {inst✝² : CategoryTheory.Limits.HasColimitsOfShape J C} [self : CategoryTheory.HasExactColimitsOfShape J C] : CategoryTheory.Limits.PreservesFiniteLimits CategoryTheory.Limits.colim
• CategoryTheory.hasExactColimitsOfShape_of_preservesMono 📋 Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (J : Type u') [CategoryTheory.Category.{v', u'} J] [CategoryTheory.Limits.HasColimitsOfShape J C] [CategoryTheory.Limits.colim.PreservesMonomorphisms] : CategoryTheory.HasExactColimitsOfShape J C
• instPreservesFiniteLimitsFunctorAddCommGrpCatColim 📋 Mathlib.Algebra.Category.Grp.AB
  {J : Type u} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] : CategoryTheory.Limits.PreservesFiniteLimits CategoryTheory.Limits.colim
• instAdditiveFunctorColim 📋 Mathlib.Algebra.Category.Grp.AB
  {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{v_1, u_1} J] [CategoryTheory.Category.{v_2, u_2} C] [CategoryTheory.Limits.HasColimitsOfShape J C] [CategoryTheory.Preadditive C] : CategoryTheory.Limits.colim.Additive
• instPreservesHomologyFunctorAddCommGrpCatColim 📋 Mathlib.Algebra.Category.Grp.AB
  {J : Type u} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] : CategoryTheory.Limits.colim.PreservesHomology
• CategoryTheory.Limits.DiagramOfCocones.mkOfHasColimits_coconePoints 📋 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)) [CategoryTheory.Limits.HasColimitsOfShape K C] : (CategoryTheory.Limits.DiagramOfCocones.mkOfHasColimits F).coconePoints = F.comp CategoryTheory.Limits.colim
• CategoryTheory.Limits.coconeOfHasColimitCurryCompColim 📋 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) [CategoryTheory.Limits.HasColimitsOfShape K C] [CategoryTheory.Limits.HasColimit ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.colim)] : CategoryTheory.Limits.Cocone G
• CategoryTheory.Limits.instHasColimitProd 📋 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) [CategoryTheory.Limits.HasColimitsOfShape K C] [CategoryTheory.Limits.HasColimit ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.colim)] : CategoryTheory.Limits.HasColimit G
• CategoryTheory.Limits.isColimitCoconeOfHasColimitCurryCompColim 📋 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) [CategoryTheory.Limits.HasColimitsOfShape K C] [CategoryTheory.Limits.HasColimit ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.colim)] : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.coconeOfHasColimitCurryCompColim G)
• CategoryTheory.Limits.colimitFlipCompColimIsoColimitCompColim 📋 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)) [CategoryTheory.Limits.HasColimitsOfShape J C] [CategoryTheory.Limits.HasColimitsOfShape K C] : CategoryTheory.Limits.colimit (F.flip.comp CategoryTheory.Limits.colim) ≅ CategoryTheory.Limits.colimit (F.comp CategoryTheory.Limits.colim)
• CategoryTheory.Limits.colimitIsoColimitCurryCompColim 📋 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) [CategoryTheory.Limits.HasColimitsOfShape K C] [CategoryTheory.Limits.HasColimit ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.colim)] : CategoryTheory.Limits.colimit G ≅ CategoryTheory.Limits.colimit ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.colim)
• CategoryTheory.Limits.colimitUncurryIsoColimitCompColim 📋 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)) [CategoryTheory.Limits.HasColimitsOfShape K C] [CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.uncurry.obj F)] [CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.Limits.colim)] : CategoryTheory.Limits.colimit (CategoryTheory.Functor.uncurry.obj F) ≅ CategoryTheory.Limits.colimit (F.comp CategoryTheory.Limits.colim)
• CategoryTheory.Limits.DiagramOfCocones.mkOfHasColimits_map_hom 📋 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)) [CategoryTheory.Limits.HasColimitsOfShape K C] {j✝ j'✝ : J} (f : j✝ ⟶ j'✝) : ((CategoryTheory.Limits.DiagramOfCocones.mkOfHasColimits F).map f).hom = CategoryTheory.Limits.colim.map (F.map f)
• CategoryTheory.Limits.colimitCurrySwapCompColimIsoColimitCurryCompColim 📋 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) [CategoryTheory.Limits.HasColimitsOfShape K C] [CategoryTheory.Limits.HasColimitsOfShape J C] [CategoryTheory.Limits.HasColimit ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.colim)] : CategoryTheory.Limits.colimit ((CategoryTheory.Functor.curry.obj ((CategoryTheory.Prod.swap K J).comp G)).comp CategoryTheory.Limits.colim) ≅ CategoryTheory.Limits.colimit ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.colim)
• CategoryTheory.Limits.colimitUncurryIsoColimitCompColim_ι_ι_inv 📋 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)) [CategoryTheory.Limits.HasColimitsOfShape K C] [CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.uncurry.obj F)] [CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.Limits.colim)] {j : J} {k : K} : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (F.obj j) k) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (F.comp CategoryTheory.Limits.colim) j) (CategoryTheory.Limits.colimitUncurryIsoColimitCompColim F).inv) = CategoryTheory.Limits.colimit.ι (CategoryTheory.Functor.uncurry.obj F) (j, k)
• CategoryTheory.Limits.colimitUncurryIsoColimitCompColim_ι_hom 📋 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)) [CategoryTheory.Limits.HasColimitsOfShape K C] [CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.uncurry.obj F)] [CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.Limits.colim)] {j : J} {k : K} : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (CategoryTheory.Functor.uncurry.obj F) (j, k)) (CategoryTheory.Limits.colimitUncurryIsoColimitCompColim F).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (F.obj j) k) (CategoryTheory.Limits.colimit.ι (F.comp CategoryTheory.Limits.colim) j)
• CategoryTheory.Limits.colimitUncurryIsoColimitCompColim_ι_ι_inv_assoc 📋 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)) [CategoryTheory.Limits.HasColimitsOfShape K C] [CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.uncurry.obj F)] [CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.Limits.colim)] {j : J} {k : K} {Z : C} (h : CategoryTheory.Limits.colimit (CategoryTheory.Functor.uncurry.obj F) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (F.obj j) k) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (F.comp CategoryTheory.Limits.colim) j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitUncurryIsoColimitCompColim F).inv h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (CategoryTheory.Functor.uncurry.obj F) (j, k)) h
• CategoryTheory.Limits.colimitFlipCompColimIsoColimitCompColim_ι_ι_hom 📋 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)) [CategoryTheory.Limits.HasColimitsOfShape J C] [CategoryTheory.Limits.HasColimitsOfShape K C] (j : J) (k : K) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (F.flip.obj k) j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (F.flip.comp CategoryTheory.Limits.colim) k) (CategoryTheory.Limits.colimitFlipCompColimIsoColimitCompColim F).hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (F.obj j) k) (CategoryTheory.Limits.colimit.ι (F.comp CategoryTheory.Limits.colim) j)
• CategoryTheory.Limits.colimitUncurryIsoColimitCompColim_ι_hom_assoc 📋 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)) [CategoryTheory.Limits.HasColimitsOfShape K C] [CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.uncurry.obj F)] [CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.Limits.colim)] {j : J} {k : K} {Z : C} (h : CategoryTheory.Limits.colimit (F.comp CategoryTheory.Limits.colim) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (CategoryTheory.Functor.uncurry.obj F) (j, k)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitUncurryIsoColimitCompColim F).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (F.obj j) k) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (F.comp CategoryTheory.Limits.colim) j) h)
• CategoryTheory.Limits.colimitFlipCompColimIsoColimitCompColim_ι_ι_inv 📋 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)) [CategoryTheory.Limits.HasColimitsOfShape J C] [CategoryTheory.Limits.HasColimitsOfShape K C] (k : K) (j : J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (F.obj j) k) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (F.comp CategoryTheory.Limits.colim) j) (CategoryTheory.Limits.colimitFlipCompColimIsoColimitCompColim F).inv) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (F.flip.obj k) j) (CategoryTheory.Limits.colimit.ι (F.flip.comp CategoryTheory.Limits.colim) k)
• CategoryTheory.Limits.colimitFlipCompColimIsoColimitCompColim_ι_ι_inv_assoc 📋 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)) [CategoryTheory.Limits.HasColimitsOfShape J C] [CategoryTheory.Limits.HasColimitsOfShape K C] (k : K) (j : J) {Z : C} (h : CategoryTheory.Limits.colimit (F.flip.comp CategoryTheory.Limits.colim) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (F.obj j) k) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (F.comp CategoryTheory.Limits.colim) j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitFlipCompColimIsoColimitCompColim F).inv h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (F.flip.obj k) j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (F.flip.comp CategoryTheory.Limits.colim) k) h)
• CategoryTheory.Limits.colimitFlipCompColimIsoColimitCompColim_ι_ι_hom_assoc 📋 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)) [CategoryTheory.Limits.HasColimitsOfShape J C] [CategoryTheory.Limits.HasColimitsOfShape K C] (j : J) (k : K) {Z : C} (h : CategoryTheory.Limits.colimit (F.comp CategoryTheory.Limits.colim) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (F.flip.obj k) j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (F.flip.comp CategoryTheory.Limits.colim) k) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitFlipCompColimIsoColimitCompColim F).hom h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (F.obj j) k) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (F.comp CategoryTheory.Limits.colim) j) h)
• CategoryTheory.Limits.colimitIsoColimitCurryCompColim_ι_hom 📋 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) [CategoryTheory.Limits.HasColimitsOfShape K C] [CategoryTheory.Limits.HasColimit ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.colim)] {j : J} {k : K} : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι G (j, k)) (CategoryTheory.Limits.colimitIsoColimitCurryCompColim G).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((CategoryTheory.Functor.curry.obj G).obj j) k) (CategoryTheory.Limits.colimit.ι ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.colim) j)
• CategoryTheory.Limits.colimitIsoColimitCurryCompColim_ι_ι_inv 📋 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) [CategoryTheory.Limits.HasColimitsOfShape K C] [CategoryTheory.Limits.HasColimit ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.colim)] {j : J} {k : K} : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((CategoryTheory.Functor.curry.obj G).obj j) k) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.colim) j) (CategoryTheory.Limits.colimitIsoColimitCurryCompColim G).inv) = CategoryTheory.Limits.colimit.ι G (j, k)
• CategoryTheory.Limits.colimitIsoColimitCurryCompColim_ι_hom_assoc 📋 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) [CategoryTheory.Limits.HasColimitsOfShape K C] [CategoryTheory.Limits.HasColimit ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.colim)] {j : J} {k : K} {Z : C} (h : CategoryTheory.Limits.colimit ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.colim) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι G (j, k)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitIsoColimitCurryCompColim G).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((CategoryTheory.Functor.curry.obj G).obj j) k) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.colim) j) h)
• CategoryTheory.Limits.colimitIsoColimitCurryCompColim_ι_ι_inv_assoc 📋 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) [CategoryTheory.Limits.HasColimitsOfShape K C] [CategoryTheory.Limits.HasColimit ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.colim)] {j : J} {k : K} {Z : C} (h : CategoryTheory.Limits.colimit G ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((CategoryTheory.Functor.curry.obj G).obj j) k) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.colim) j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitIsoColimitCurryCompColim G).inv h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι G (j, k)) h
• CategoryTheory.Limits.colimitCurrySwapCompColimIsoColimitCurryCompColim_ι_ι_hom 📋 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) [CategoryTheory.Limits.HasColimitsOfShape K C] [CategoryTheory.Limits.HasColimitsOfShape J C] [CategoryTheory.Limits.HasColimit ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.colim)] {j : J} {k : K} : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((CategoryTheory.Functor.curry.obj ((CategoryTheory.Prod.swap K J).comp G)).obj k) j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((CategoryTheory.Functor.curry.obj ((CategoryTheory.Prod.swap K J).comp G)).comp CategoryTheory.Limits.colim) k) (CategoryTheory.Limits.colimitCurrySwapCompColimIsoColimitCurryCompColim G).hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((CategoryTheory.Functor.curry.obj G).obj j) k) (CategoryTheory.Limits.colimit.ι ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.colim) j)
• CategoryTheory.Limits.colimitCurrySwapCompColimIsoColimitCurryCompColim_ι_ι_inv 📋 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) [CategoryTheory.Limits.HasColimitsOfShape K C] [CategoryTheory.Limits.HasColimitsOfShape J C] [CategoryTheory.Limits.HasColimit ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.colim)] {j : J} {k : K} : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((CategoryTheory.Functor.curry.obj G).obj j) k) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.colim) j) (CategoryTheory.Limits.colimitCurrySwapCompColimIsoColimitCurryCompColim G).inv) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((CategoryTheory.Functor.curry.obj ((CategoryTheory.Prod.swap K J).comp G)).obj k) j) (CategoryTheory.Limits.colimit.ι ((CategoryTheory.Functor.curry.obj ((CategoryTheory.Prod.swap K J).comp G)).comp CategoryTheory.Limits.colim) k)
• CategoryTheory.IsSifted.colim_preservesFiniteProducts_of_isSifted 📋 Mathlib.CategoryTheory.Limits.Sifted
  {C : Type u} [CategoryTheory.SmallCategory C] [CategoryTheory.IsSifted C] : CategoryTheory.Limits.PreservesFiniteProducts CategoryTheory.Limits.colim
• CategoryTheory.IsSifted.isSiftedOrEmpty_of_colim_preservesFiniteProducts 📋 Mathlib.CategoryTheory.Limits.Sifted
  (C : Type u) [CategoryTheory.SmallCategory C] [h : CategoryTheory.Limits.PreservesFiniteProducts CategoryTheory.Limits.colim] : CategoryTheory.IsSiftedOrEmpty C
• CategoryTheory.IsSifted.of_colim_preservesFiniteProducts 📋 Mathlib.CategoryTheory.Limits.Sifted
  (C : Type u) [CategoryTheory.SmallCategory C] [h : CategoryTheory.Limits.PreservesFiniteProducts CategoryTheory.Limits.colim] : CategoryTheory.IsSifted C
• CategoryTheory.IsSifted.colim_preservesBinaryProducts_of_isSifted 📋 Mathlib.CategoryTheory.Limits.Sifted
  {C : Type u} [CategoryTheory.SmallCategory C] [CategoryTheory.IsSifted C] : CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) CategoryTheory.Limits.colim
• CategoryTheory.IsSifted.colim_preservesLimitsOfShape_pempty_of_isSifted 📋 Mathlib.CategoryTheory.Limits.Sifted
  {C : Type u} [CategoryTheory.SmallCategory C] [CategoryTheory.IsSifted C] : CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) CategoryTheory.Limits.colim
• CategoryTheory.IsSifted.isSiftedOrEmpty_of_colim_preservesBinaryProducts 📋 Mathlib.CategoryTheory.Limits.Sifted
  (C : Type u) [CategoryTheory.SmallCategory C] [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) CategoryTheory.Limits.colim] : CategoryTheory.IsSiftedOrEmpty C
• CategoryTheory.IsSifted.nonempty_of_colim_preservesLimitsOfShapeFinZero 📋 Mathlib.CategoryTheory.Limits.Sifted
  (C : Type u) [CategoryTheory.SmallCategory C] [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete (Fin 0)) CategoryTheory.Limits.colim] : Nonempty C
• CategoryTheory.IsSifted.colim_preservesTerminal_of_isSifted 📋 Mathlib.CategoryTheory.Limits.Sifted
  {C : Type u} [CategoryTheory.SmallCategory C] [CategoryTheory.IsSifted C] : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty (CategoryTheory.Functor C (Type u))) CategoryTheory.Limits.colim
• CategoryTheory.IsSifted.colim_preservesLimits_pair_of_sSifted 📋 Mathlib.CategoryTheory.Limits.Sifted
  {C : Type u} [CategoryTheory.SmallCategory C] [CategoryTheory.IsSifted C] {X Y : CategoryTheory.Functor C (Type u)} : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair X Y) CategoryTheory.Limits.colim
• CategoryTheory.IsSifted.instIsIsoObjFunctorTypeColimTensorObjProdComparison 📋 Mathlib.CategoryTheory.Limits.Sifted
  {C : Type u} [CategoryTheory.SmallCategory C] (X Y : CategoryTheory.Functor C (Type u)) [CategoryTheory.IsSifted C] : CategoryTheory.IsIso (CategoryTheory.CartesianMonoidalCategory.prodComparison CategoryTheory.Limits.colim X Y)
• CategoryTheory.IsSifted.factorization_prodComparison_colim 📋 Mathlib.CategoryTheory.Limits.Sifted
  {C : Type u} [CategoryTheory.SmallCategory C] (X Y : CategoryTheory.Functor C (Type u)) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.HasColimit.isoOfNatIso ((CategoryTheory.MonoidalCategory.externalProductCompDiagIso C (Type u)).app (X, Y)).symm).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.pre (CategoryTheory.MonoidalCategory.externalProduct X Y) (CategoryTheory.Functor.diag C)) (CategoryTheory.Limits.PreservesColimit₂.isoColimitUncurryWhiskeringLeft₂ X Y (CategoryTheory.MonoidalCategory.curriedTensor (Type u))).hom) = CategoryTheory.CartesianMonoidalCategory.prodComparison CategoryTheory.Limits.colim X Y
• CategoryTheory.Limits.colimitLimitToLimitColimitCone 📋 Mathlib.CategoryTheory.Limits.ColimitLimit
  {J : Type u₁} {K : Type u₂} [CategoryTheory.Category.{v₁, u₁} J] [CategoryTheory.Category.{v₂, u₂} K] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimitsOfShape J C] [CategoryTheory.Limits.HasColimitsOfShape K C] (G : CategoryTheory.Functor J (CategoryTheory.Functor K C)) [CategoryTheory.Limits.HasLimit G] : CategoryTheory.Limits.colim.mapCone (CategoryTheory.Limits.limit.cone G) ⟶ CategoryTheory.Limits.limit.cone (G.comp CategoryTheory.Limits.colim)
• CategoryTheory.Limits.colimitLimitToLimitColimit 📋 Mathlib.CategoryTheory.Limits.ColimitLimit
  {J : Type u₁} {K : Type u₂} [CategoryTheory.Category.{v₁, u₁} J] [CategoryTheory.Category.{v₂, u₂} K] {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor (J × K) C) [CategoryTheory.Limits.HasLimitsOfShape J C] [CategoryTheory.Limits.HasColimitsOfShape K C] : CategoryTheory.Limits.colimit ((CategoryTheory.Functor.curry.obj ((CategoryTheory.Prod.swap K J).comp F)).comp CategoryTheory.Limits.lim) ⟶ CategoryTheory.Limits.limit ((CategoryTheory.Functor.curry.obj F).comp CategoryTheory.Limits.colim)
• CategoryTheory.Limits.ι_colimitLimitToLimitColimit_π 📋 Mathlib.CategoryTheory.Limits.ColimitLimit
  {J : Type u₁} {K : Type u₂} [CategoryTheory.Category.{v₁, u₁} J] [CategoryTheory.Category.{v₂, u₂} K] {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor (J × K) C) [CategoryTheory.Limits.HasLimitsOfShape J C] [CategoryTheory.Limits.HasColimitsOfShape K C] (j : J) (k : K) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((CategoryTheory.Functor.curry.obj ((CategoryTheory.Prod.swap K J).comp F)).comp CategoryTheory.Limits.lim) k) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitLimitToLimitColimit F) (CategoryTheory.Limits.limit.π ((CategoryTheory.Functor.curry.obj F).comp CategoryTheory.Limits.colim) j)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π ((CategoryTheory.Functor.curry.obj ((CategoryTheory.Prod.swap K J).comp F)).obj k) j) (CategoryTheory.Limits.colimit.ι ((CategoryTheory.Functor.curry.obj F).obj j) k)
• CategoryTheory.Limits.ι_colimitLimitToLimitColimit_π_assoc 📋 Mathlib.CategoryTheory.Limits.ColimitLimit
  {J : Type u₁} {K : Type u₂} [CategoryTheory.Category.{v₁, u₁} J] [CategoryTheory.Category.{v₂, u₂} K] {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor (J × K) C) [CategoryTheory.Limits.HasLimitsOfShape J C] [CategoryTheory.Limits.HasColimitsOfShape K C] (j : J) (k : K) {Z : C} (h : CategoryTheory.Limits.colim.obj ((CategoryTheory.Functor.curry.obj F).obj j) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((CategoryTheory.Functor.curry.obj ((CategoryTheory.Prod.swap K J).comp F)).comp CategoryTheory.Limits.lim) k) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitLimitToLimitColimit F) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π ((CategoryTheory.Functor.curry.obj F).comp CategoryTheory.Limits.colim) j) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π ((CategoryTheory.Functor.curry.obj ((CategoryTheory.Prod.swap K J).comp F)).obj k) j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((CategoryTheory.Functor.curry.obj F).obj j) k) h)
• CategoryTheory.Limits.colimitLimitToLimitColimitCone_hom 📋 Mathlib.CategoryTheory.Limits.ColimitLimit
  {J : Type u₁} {K : Type u₂} [CategoryTheory.Category.{v₁, u₁} J] [CategoryTheory.Category.{v₂, u₂} K] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimitsOfShape J C] [CategoryTheory.Limits.HasColimitsOfShape K C] (G : CategoryTheory.Functor J (CategoryTheory.Functor K C)) [CategoryTheory.Limits.HasLimit G] : (CategoryTheory.Limits.colimitLimitToLimitColimitCone G).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colim.map (CategoryTheory.Limits.limitIsoSwapCompLim G).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitLimitToLimitColimit (CategoryTheory.Functor.uncurry.obj G)) (CategoryTheory.Limits.lim.map (CategoryTheory.Functor.whiskerRight (CategoryTheory.Functor.currying.unitIso.app G).inv CategoryTheory.Limits.colim)))
• CategoryTheory.Limits.ι_colimitLimitToLimitColimit_π_apply 📋 Mathlib.CategoryTheory.Limits.ColimitLimit
  {J : Type u₁} {K : Type u₂} [CategoryTheory.Category.{v₁, u₁} J] [CategoryTheory.Category.{v₂, u₂} K] {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor (J × K) C) [CategoryTheory.Limits.HasLimitsOfShape J C] [CategoryTheory.Limits.HasColimitsOfShape K C] (j : J) (k : K) {F✝ : C → C → Type uF} {carrier : C → Type w} {instFunLike : (X Y : C) → FunLike (F✝ X Y) (carrier X) (carrier Y)} [inst : CategoryTheory.ConcreteCategory C F✝] (x : carrier (((CategoryTheory.Functor.curry.obj ((CategoryTheory.Prod.swap K J).comp F)).comp CategoryTheory.Limits.lim).obj k)) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.π ((CategoryTheory.Functor.curry.obj F).comp CategoryTheory.Limits.colim) j)) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimitLimitToLimitColimit F)) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimit.ι ((CategoryTheory.Functor.curry.obj ((CategoryTheory.Prod.swap K J).comp F)).comp CategoryTheory.Limits.lim) k)) x)) = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimit.ι ((CategoryTheory.Functor.curry.obj F).obj j) k)) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.π ((CategoryTheory.Functor.curry.obj ((CategoryTheory.Prod.swap K J).comp F)).obj k) j)) x)
• CategoryTheory.Limits.filtered_colim_preservesFiniteLimits_of_types 📋 Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit
  {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] [Small.{v, u₂} K] [CategoryTheory.IsFiltered K] : CategoryTheory.Limits.PreservesFiniteLimits CategoryTheory.Limits.colim
• CategoryTheory.Limits.instPreservesFiniteLimitsFunctorColimOfPreservesColimitsOfShapeOfHasFiniteLimitsOfReflectsIsomorphismsForget 📋 Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit
  {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] [Small.{v, u₂} K] [CategoryTheory.IsFiltered K] {C : Type u} [CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type v} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] [CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.forget C)] [CategoryTheory.Limits.PreservesColimitsOfShape K (CategoryTheory.forget C)] [CategoryTheory.Limits.HasFiniteLimits C] [CategoryTheory.Limits.HasColimitsOfShape K C] [(CategoryTheory.forget C).ReflectsIsomorphisms] : CategoryTheory.Limits.PreservesFiniteLimits CategoryTheory.Limits.colim
• CategoryTheory.Limits.filtered_colim_preservesFiniteLimits 📋 Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit
  {J : Type u₁} {K : Type u₂} [CategoryTheory.SmallCategory J] [CategoryTheory.Category.{v₂, u₂} K] [Small.{v, u₂} K] [CategoryTheory.FinCategory J] [CategoryTheory.IsFiltered K] {C : Type u} [CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type v} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] [CategoryTheory.Limits.HasLimitsOfShape J C] [CategoryTheory.Limits.HasColimitsOfShape K C] [CategoryTheory.Limits.ReflectsLimitsOfShape J (CategoryTheory.forget C)] [CategoryTheory.Limits.PreservesColimitsOfShape K (CategoryTheory.forget C)] [CategoryTheory.Limits.PreservesLimitsOfShape J (CategoryTheory.forget C)] : CategoryTheory.Limits.PreservesLimitsOfShape J CategoryTheory.Limits.colim
• CategoryTheory.Limits.colimitLimitToLimitColimitCone_iso 📋 Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit
  {J : Type u₁} {K : Type u₂} [CategoryTheory.SmallCategory J] [CategoryTheory.Category.{v₂, u₂} K] [Small.{v, u₂} K] [CategoryTheory.FinCategory J] [CategoryTheory.IsFiltered K] (F : CategoryTheory.Functor J (CategoryTheory.Functor K (Type v))) : CategoryTheory.IsIso (CategoryTheory.Limits.colimitLimitToLimitColimitCone F)
• CategoryTheory.Limits.colimitLimitIso 📋 Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] [CategoryTheory.Limits.HasLimitsOfShape J C] [CategoryTheory.Limits.HasColimitsOfShape K C] [CategoryTheory.Limits.PreservesLimitsOfShape J CategoryTheory.Limits.colim] (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) : CategoryTheory.Limits.colimit (CategoryTheory.Limits.limit F) ≅ CategoryTheory.Limits.limit (CategoryTheory.Limits.colimit F.flip)
• CategoryTheory.Limits.colimitLimitToLimitColimit_isIso 📋 Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit
  {J : Type u₁} {K : Type u₂} [CategoryTheory.SmallCategory J] [CategoryTheory.Category.{v₂, u₂} K] [Small.{v, u₂} K] [CategoryTheory.FinCategory J] (F : CategoryTheory.Functor (J × K) (Type v)) [CategoryTheory.IsFiltered K] : CategoryTheory.IsIso (CategoryTheory.Limits.colimitLimitToLimitColimit F)
• CategoryTheory.Limits.ι_colimitLimitIso_limit_π 📋 Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] [CategoryTheory.Limits.HasLimitsOfShape J C] [CategoryTheory.Limits.HasColimitsOfShape K C] [CategoryTheory.Limits.PreservesLimitsOfShape J CategoryTheory.Limits.colim] (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) (a : K) (b : J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (CategoryTheory.Limits.limit F) a) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitLimitIso F).hom (CategoryTheory.Limits.limit.π (CategoryTheory.Limits.colimit F.flip) b)) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.limit.π F b).app a) ((CategoryTheory.Limits.colimit.ι F.flip a).app b)
• CategoryTheory.Limits.ι_colimitLimitIso_limit_π_assoc 📋 Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] [CategoryTheory.Limits.HasLimitsOfShape J C] [CategoryTheory.Limits.HasColimitsOfShape K C] [CategoryTheory.Limits.PreservesLimitsOfShape J CategoryTheory.Limits.colim] (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) (a : K) (b : J) {Z : C} (h : (CategoryTheory.Limits.colimit F.flip).obj b ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (CategoryTheory.Limits.limit F) a) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitLimitIso F).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (CategoryTheory.Limits.colimit F.flip) b) h)) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.limit.π F b).app a) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.colimit.ι F.flip a).app b) h)
• CategoryTheory.Limits.colimitLimitToLimitColimit_injective 📋 Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit
  {J : Type u₁} {K : Type u₂} [CategoryTheory.Category.{v₁, u₁} J] [CategoryTheory.Category.{v₂, u₂} K] [Small.{v, u₂} K] (F : CategoryTheory.Functor (J × K) (Type v)) [CategoryTheory.IsFiltered K] [Finite J] : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimitLimitToLimitColimit F))
• CategoryTheory.Limits.colimitLimitToLimitColimit_surjective 📋 Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit
  {J : Type u₁} {K : Type u₂} [CategoryTheory.SmallCategory J] [CategoryTheory.Category.{v₂, u₂} K] [Small.{v, u₂} K] [CategoryTheory.FinCategory J] (F : CategoryTheory.Functor (J × K) (Type v)) [CategoryTheory.IsFiltered K] : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimitLimitToLimitColimit F))
• CategoryTheory.lanEvaluationIsoColim 📋 Mathlib.CategoryTheory.Functor.Flat
  {C D : Type u₁} [CategoryTheory.SmallCategory C] [CategoryTheory.SmallCategory D] (E : Type u₂) [CategoryTheory.Category.{u₁, u₂} E] (F : CategoryTheory.Functor C D) (X : D) [∀ (X : D), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.CostructuredArrow F X) E] : F.lan.comp ((CategoryTheory.evaluation D E).obj X) ≅ ((CategoryTheory.Functor.whiskeringLeft (CategoryTheory.CostructuredArrow F X) C E).obj (CategoryTheory.CostructuredArrow.proj F X)).comp CategoryTheory.Limits.colim
• CategoryTheory.MorphismProperty.isStableUnderColimitsOfShape_monomorphisms 📋 Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim
  (C : Type u) [CategoryTheory.Category.{v, u} C] (J : Type u') [CategoryTheory.Category.{v', u'} J] [CategoryTheory.Limits.HasColimitsOfShape J C] [CategoryTheory.Limits.colim.PreservesMonomorphisms] : (CategoryTheory.MorphismProperty.monomorphisms C).IsStableUnderColimitsOfShape J
• CategoryTheory.Limits.IsColimit.mono_ι_app_of_isFiltered 📋 Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u'} [CategoryTheory.Category.{v', u'} J] {X : CategoryTheory.Functor J C} [∀ (j j' : J) (φ : j ⟶ j'), CategoryTheory.Mono (X.map φ)] {c : CategoryTheory.Limits.Cocone X} (hc : CategoryTheory.Limits.IsColimit c) [CategoryTheory.IsFiltered J] (j₀ : J) [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Under j₀) C] [CategoryTheory.Limits.colim.PreservesMonomorphisms] : CategoryTheory.Mono (c.ι.app j₀)
• CategoryTheory.Limits.colim.map_mono' 📋 Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u'} [CategoryTheory.Category.{v', u'} J] [CategoryTheory.Limits.HasColimitsOfShape J C] [CategoryTheory.Limits.colim.PreservesMonomorphisms] {X₁ X₂ : CategoryTheory.Functor J C} (φ : X₁ ⟶ X₂) [CategoryTheory.Mono φ] {c₁ : CategoryTheory.Limits.Cocone X₁} (hc₁ : CategoryTheory.Limits.IsColimit c₁) {c₂ : CategoryTheory.Limits.Cocone X₂} (hc₂ : CategoryTheory.Limits.IsColimit c₂) (f : c₁.pt ⟶ c₂.pt) (hf : ∀ (j : J), CategoryTheory.CategoryStruct.comp (c₁.ι.app j) f = CategoryTheory.CategoryStruct.comp (φ.app j) (c₂.ι.app j)) : CategoryTheory.Mono f
• CategoryTheory.IndParallelPairPresentation.parallelPairIsoParallelPairCompYoneda 📋 Mathlib.CategoryTheory.Limits.Indization.ParallelPair
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A B : CategoryTheory.Functor Cᵒᵖ (Type v₁)} {f g : A ⟶ B} (P : CategoryTheory.IndParallelPairPresentation f g) : CategoryTheory.Limits.parallelPair f g ≅ (CategoryTheory.Limits.parallelPair P.φ P.ψ).comp (((CategoryTheory.Functor.whiskeringRight P.I C (CategoryTheory.Functor Cᵒᵖ (Type v₁))).obj CategoryTheory.yoneda).comp CategoryTheory.Limits.colim)
• CategoryTheory.Limits.isIndObject_limit_comp_yoneda_comp_colim 📋 Mathlib.CategoryTheory.Limits.Indization.Equalizers
  {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type v} [CategoryTheory.SmallCategory I] [CategoryTheory.IsFiltered I] {J : Type} [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] (F : CategoryTheory.Functor J (CategoryTheory.Functor I C)) (hF : ∀ (i : I), CategoryTheory.Limits.IsIndObject (CategoryTheory.Limits.limit ((F.flip.obj i).comp CategoryTheory.yoneda))) : CategoryTheory.Limits.IsIndObject (CategoryTheory.Limits.limit (F.comp (((CategoryTheory.Functor.whiskeringRight I C (CategoryTheory.Functor Cᵒᵖ (Type v))).obj CategoryTheory.yoneda).comp CategoryTheory.Limits.colim)))
• CategoryTheory.Ind.limCompInclusion 📋 Mathlib.CategoryTheory.Limits.Indization.Category
  {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type v} [CategoryTheory.SmallCategory I] [CategoryTheory.IsFiltered I] : (CategoryTheory.Ind.lim I).comp (CategoryTheory.Ind.inclusion C) ≅ ((CategoryTheory.Functor.whiskeringRight I C (CategoryTheory.Functor Cᵒᵖ (Type v))).obj CategoryTheory.yoneda).comp CategoryTheory.Limits.colim
• CategoryTheory.Limits.preservesLimitsOfShape_colim_grothendieck 📋 Mathlib.CategoryTheory.Limits.Preserves.Grothendieck
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] {H : Type u₂} [CategoryTheory.Category.{v₂, u₂} H] {J : Type u₃} [CategoryTheory.Category.{v₃, u₃} J] (F : CategoryTheory.Functor C CategoryTheory.Cat) [CategoryTheory.Limits.HasColimitsOfShape C H] [CategoryTheory.Limits.HasLimitsOfShape J H] [∀ (c : C), CategoryTheory.Limits.HasColimitsOfShape (↑(F.obj c)) H] [CategoryTheory.Limits.PreservesLimitsOfShape J CategoryTheory.Limits.colim] [∀ (c : C), CategoryTheory.Limits.PreservesLimitsOfShape J CategoryTheory.Limits.colim] : CategoryTheory.Limits.PreservesLimitsOfShape J CategoryTheory.Limits.colim
• CategoryTheory.Limits.fiberwiseColimitLimitIso 📋 Mathlib.CategoryTheory.Limits.Preserves.Grothendieck
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {H : Type u₂} [CategoryTheory.Category.{v₂, u₂} H] {J : Type u₃} [CategoryTheory.Category.{v₃, u₃} J] {F : CategoryTheory.Functor C CategoryTheory.Cat} (K : CategoryTheory.Functor J (CategoryTheory.Functor (CategoryTheory.Grothendieck F) H)) [∀ (c : C), CategoryTheory.Limits.HasColimitsOfShape (↑(F.obj c)) H] [CategoryTheory.Limits.HasLimitsOfShape J H] [∀ (c : C), CategoryTheory.Limits.PreservesLimitsOfShape J CategoryTheory.Limits.colim] : CategoryTheory.Limits.fiberwiseColimit (CategoryTheory.Limits.limit K) ≅ CategoryTheory.Limits.limit (K.comp (CategoryTheory.Limits.fiberwiseColim F H))
• CategoryTheory.Limits.fiberwiseColimitLimitIso_inv_app 📋 Mathlib.CategoryTheory.Limits.Preserves.Grothendieck
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {H : Type u₂} [CategoryTheory.Category.{v₂, u₂} H] {J : Type u₃} [CategoryTheory.Category.{v₃, u₃} J] {F : CategoryTheory.Functor C CategoryTheory.Cat} (K : CategoryTheory.Functor J (CategoryTheory.Functor (CategoryTheory.Grothendieck F) H)) [∀ (c : C), CategoryTheory.Limits.HasColimitsOfShape (↑(F.obj c)) H] [CategoryTheory.Limits.HasLimitsOfShape J H] [∀ (c : C), CategoryTheory.Limits.PreservesLimitsOfShape J CategoryTheory.Limits.colim] (X : C) : (CategoryTheory.Limits.fiberwiseColimitLimitIso K).inv.app X = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitObjIsoLimitCompEvaluation (K.comp (CategoryTheory.Limits.fiberwiseColim F H)) X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.HasLimit.isoOfNatIso (K.associator ((CategoryTheory.Functor.whiskeringLeft (↑(F.obj X)) (CategoryTheory.Grothendieck F) H).obj (CategoryTheory.Grothendieck.ι F X)) CategoryTheory.Limits.colim ≪≫ K.isoWhiskerLeft (CategoryTheory.Limits.fiberwiseColimCompEvaluationIso X).symm ≪≫ (K.associator (CategoryTheory.Limits.fiberwiseColim F H) ((CategoryTheory.evaluation C H).obj X)).symm)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.preservesLimitIso CategoryTheory.Limits.colim (K.comp ((CategoryTheory.Functor.whiskeringLeft (↑(F.obj X)) (CategoryTheory.Grothendieck F) H).obj (CategoryTheory.Grothendieck.ι F X)))).inv (CategoryTheory.Limits.HasColimit.isoOfNatIso (CategoryTheory.Limits.limitCompWhiskeringLeftIsoCompLimit K (CategoryTheory.Grothendieck.ι F X)).symm).inv))
• CategoryTheory.Limits.fiberwiseColimitLimitIso_hom_app 📋 Mathlib.CategoryTheory.Limits.Preserves.Grothendieck
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {H : Type u₂} [CategoryTheory.Category.{v₂, u₂} H] {J : Type u₃} [CategoryTheory.Category.{v₃, u₃} J] {F : CategoryTheory.Functor C CategoryTheory.Cat} (K : CategoryTheory.Functor J (CategoryTheory.Functor (CategoryTheory.Grothendieck F) H)) [∀ (c : C), CategoryTheory.Limits.HasColimitsOfShape (↑(F.obj c)) H] [CategoryTheory.Limits.HasLimitsOfShape J H] [∀ (c : C), CategoryTheory.Limits.PreservesLimitsOfShape J CategoryTheory.Limits.colim] (X : C) : (CategoryTheory.Limits.fiberwiseColimitLimitIso K).hom.app X = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.HasColimit.isoOfNatIso (CategoryTheory.Limits.limitCompWhiskeringLeftIsoCompLimit K (CategoryTheory.Grothendieck.ι F X)).symm).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.preservesLimitIso CategoryTheory.Limits.colim (K.comp ((CategoryTheory.Functor.whiskeringLeft (↑(F.obj X)) (CategoryTheory.Grothendieck F) H).obj (CategoryTheory.Grothendieck.ι F X)))).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.HasLimit.isoOfNatIso (K.associator ((CategoryTheory.Functor.whiskeringLeft (↑(F.obj X)) (CategoryTheory.Grothendieck F) H).obj (CategoryTheory.Grothendieck.ι F X)) CategoryTheory.Limits.colim ≪≫ K.isoWhiskerLeft (CategoryTheory.Limits.fiberwiseColimCompEvaluationIso X).symm ≪≫ (K.associator (CategoryTheory.Limits.fiberwiseColim F H) ((CategoryTheory.evaluation C H).obj X)).symm)).hom (CategoryTheory.Limits.limitObjIsoLimitCompEvaluation (K.comp (CategoryTheory.Limits.fiberwiseColim F H)) X).inv))
• CategoryTheory.ObjectProperty.instIsClosedUnderColimitsOfShapeFunctorPreservesLimitsOfShapeOfPreservesLimitsOfShapeColim 📋 Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits
  {J : Type u_1} {C : Type u_2} (K : Type u_3) (K' : Type u_4) [CategoryTheory.Category.{v_1, u_3} K] [CategoryTheory.Category.{v_2, u_4} K'] [CategoryTheory.Category.{v_3, u_1} J] [CategoryTheory.Category.{v_4, u_2} C] [CategoryTheory.Limits.HasColimitsOfShape K' C] [CategoryTheory.Limits.PreservesLimitsOfShape K CategoryTheory.Limits.colim] : (CategoryTheory.ObjectProperty.preservesLimitsOfShape K).IsClosedUnderColimitsOfShape K'
• CategoryTheory.instPreservesFiniteProductsFunctorColimOfPreadditive 📋 Mathlib.CategoryTheory.Sites.Coherent.ExtensiveColimits
  {A : Type u_1} {J : Type u_3} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_3, u_3} J] [CategoryTheory.Limits.HasColimitsOfShape J A] [CategoryTheory.Preadditive A] : CategoryTheory.Limits.PreservesFiniteProducts CategoryTheory.Limits.colim
• CategoryTheory.instPreservesColimitsOfShapeSheafExtensiveTopologyFunctorOppositeSheafToPresheafOfPreservesFiniteProductsColim 📋 Mathlib.CategoryTheory.Sites.Coherent.ExtensiveColimits
  {A : Type u_1} {C : Type u_2} {J : Type u_3} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} C] [CategoryTheory.Category.{v_3, u_3} J] [CategoryTheory.FinitaryExtensive C] [CategoryTheory.Limits.HasColimitsOfShape J A] [CategoryTheory.Limits.PreservesFiniteProducts CategoryTheory.Limits.colim] : CategoryTheory.Limits.PreservesColimitsOfShape J (CategoryTheory.sheafToPresheaf (CategoryTheory.extensiveTopology C) A)
• CategoryTheory.isSheaf_pointwiseColimit 📋 Mathlib.CategoryTheory.Sites.Coherent.ExtensiveColimits
  {A : Type u_1} {C : Type u_2} {J : Type u_3} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} C] [CategoryTheory.Category.{v_3, u_3} J] [CategoryTheory.FinitaryExtensive C] [CategoryTheory.Limits.HasColimitsOfShape J A] [CategoryTheory.Limits.PreservesFiniteProducts CategoryTheory.Limits.colim] (G : CategoryTheory.Functor J (CategoryTheory.Sheaf (CategoryTheory.extensiveTopology C) A)) : CategoryTheory.Presheaf.IsSheaf (CategoryTheory.extensiveTopology C) (CategoryTheory.Limits.pointwiseCocone (G.comp (CategoryTheory.sheafToPresheaf (CategoryTheory.extensiveTopology C) A))).pt

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 69fae59