Loogle!

Result

Found 44 declarations mentioning CategoryTheory.Limits.colimit.cocone.

• CategoryTheory.Limits.colimit.cocone 📋 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] : CategoryTheory.Limits.Cocone F
• CategoryTheory.Limits.colimit.isColimit 📋 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] : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.colimit.cocone F)
• CategoryTheory.Limits.colimit.cocone_x 📋 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] : (CategoryTheory.Limits.colimit.cocone F).pt = CategoryTheory.Limits.colimit F
• CategoryTheory.Limits.colimit.coconeMorphism 📋 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.cocone F ⟶ c
• CategoryTheory.Limits.colimit.desc_cocone 📋 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] : CategoryTheory.Limits.colimit.desc F (CategoryTheory.Limits.colimit.cocone F) = CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.colimit F)
• 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.coconeMorphism_hom 📋 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.coconeMorphism c).hom = CategoryTheory.Limits.colimit.desc F c
• CategoryTheory.Limits.colimit.cocone_ι 📋 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] : (CategoryTheory.Limits.colimit.cocone F).ι.app = CategoryTheory.Limits.colimit.ι F
• CategoryTheory.Limits.colimit.ι_coconeMorphism 📋 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) (j : J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F j) (CategoryTheory.Limits.colimit.coconeMorphism c).hom = c.ι.app j
• CategoryTheory.Limits.colimit.comp_coconePointUniqueUpToIso_hom 📋 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} (hc : CategoryTheory.Limits.IsColimit c) (j : J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F j) ((CategoryTheory.Limits.colimit.isColimit F).coconePointUniqueUpToIso hc).hom = c.ι.app j
• CategoryTheory.Limits.colimit.comp_coconePointUniqueUpToIso_inv 📋 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} (hc : CategoryTheory.Limits.IsColimit c) (j : J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F j) (hc.coconePointUniqueUpToIso (CategoryTheory.Limits.colimit.isColimit F)).inv = c.ι.app j
• CategoryTheory.Limits.colimit.comp_coconePointUniqueUpToIso_hom_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.HasColimit F] {c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.Limits.IsColimit c) (j : J) {Z : C} (h : c.pt ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F j) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.colimit.isColimit F).coconePointUniqueUpToIso hc).hom h) = CategoryTheory.CategoryStruct.comp (c.ι.app j) h
• CategoryTheory.Limits.colimit.comp_coconePointUniqueUpToIso_inv_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.HasColimit F] {c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.Limits.IsColimit c) (j : J) {Z : C} (h : c.pt ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F j) (CategoryTheory.CategoryStruct.comp (hc.coconePointUniqueUpToIso (CategoryTheory.Limits.colimit.isColimit F)).inv h) = CategoryTheory.CategoryStruct.comp (c.ι.app j) h
• CategoryTheory.Limits.colimit.homIso_hom 📋 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] {W : C} : (CategoryTheory.Limits.colimit.homIso F W).hom = TypeCat.ofHom fun f => CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.cocone F).ι ((CategoryTheory.Functor.const J).map f.down)
• CategoryTheory.Limits.PushoutCocone.inl_colimit_cocone 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : Z ⟶ X) (g : Z ⟶ Y) [CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.span f g)] : CategoryTheory.Limits.PushoutCocone.inl (CategoryTheory.Limits.colimit.cocone (CategoryTheory.Limits.span f g)) = CategoryTheory.Limits.pushout.inl f g
• CategoryTheory.Limits.PushoutCocone.inr_colimit_cocone 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : Z ⟶ X) (g : Z ⟶ Y) [CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.span f g)] : CategoryTheory.Limits.PushoutCocone.inr (CategoryTheory.Limits.colimit.cocone (CategoryTheory.Limits.span f g)) = CategoryTheory.Limits.pushout.inr f g
• CategoryTheory.Limits.cokernelBiproductιIso_hom 📋 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).hom = CategoryTheory.Limits.colimit.desc (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.biproduct.ι f i) 0) (CategoryTheory.Limits.CokernelCofork.ofπ (CategoryTheory.Limits.biproduct.toSubtype f fun j => ¬j = i) ⋯)
• 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_hom 📋 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).hom = CategoryTheory.Limits.colimit.desc (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.biproduct.fromSubtype f p) 0) (CategoryTheory.Limits.CokernelCofork.ofπ (CategoryTheory.Limits.biproduct.toSubtype f pᶜ) ⋯)
• 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_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} [CategoryTheory.Limits.HasBinaryBiproduct X Y] : CategoryTheory.Limits.cokernelBiprodInlIso.hom = CategoryTheory.Limits.colimit.desc (CategoryTheory.Limits.parallelPair CategoryTheory.Limits.biprod.inl 0) (CategoryTheory.Limits.biprod.inlCokernelCofork X Y)
• CategoryTheory.Limits.cokernelBiprodInrIso_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} [CategoryTheory.Limits.HasBinaryBiproduct X Y] : CategoryTheory.Limits.cokernelBiprodInrIso.hom = CategoryTheory.Limits.colimit.desc (CategoryTheory.Limits.parallelPair CategoryTheory.Limits.biprod.inr 0) (CategoryTheory.Limits.biprod.inrCokernelCofork X Y)
• 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.createsColimitOfFullyFaithfulOfLift 📋 Mathlib.CategoryTheory.Limits.Creates
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [CategoryTheory.Category.{w', w} J] {K : CategoryTheory.Functor J C} {F : CategoryTheory.Functor C D} [F.Full] [F.Faithful] [CategoryTheory.Limits.HasColimit (K.comp F)] (c : CategoryTheory.Limits.Cocone K) (i : F.mapCocone c ≅ CategoryTheory.Limits.colimit.cocone (K.comp F)) : CategoryTheory.CreatesColimit K F
• CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork_functor_obj_pt 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape} (I : CategoryTheory.Limits.MultispanIndex J C) [CategoryTheory.Limits.HasCoproduct I.left] [CategoryTheory.Limits.HasCoproduct I.right] (K : CategoryTheory.Limits.Multicofork I) : (I.multicoforkEquivSigmaCofork.functor.obj K).pt = K.pt
• CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork_inverse_obj_pt 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape} (I : CategoryTheory.Limits.MultispanIndex J C) [CategoryTheory.Limits.HasCoproduct I.left] [CategoryTheory.Limits.HasCoproduct I.right] (a : CategoryTheory.Limits.Cofork (I.fstSigmaMapOfIsColimit (CategoryTheory.Limits.colimit.cocone (CategoryTheory.Discrete.functor I.right)) (CategoryTheory.Limits.colimit.isColimit (CategoryTheory.Discrete.functor I.left))) (I.sndSigmaMapOfIsColimit (CategoryTheory.Limits.colimit.cocone (CategoryTheory.Discrete.functor I.right)) (CategoryTheory.Limits.colimit.isColimit (CategoryTheory.Discrete.functor I.left)))) : (I.multicoforkEquivSigmaCofork.inverse.obj a).pt = a.pt
• CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork_functor_map_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape} (I : CategoryTheory.Limits.MultispanIndex J C) [CategoryTheory.Limits.HasCoproduct I.left] [CategoryTheory.Limits.HasCoproduct I.right] {K₁ K₂ : CategoryTheory.Limits.Multicofork I} (f : K₁ ⟶ K₂) : (I.multicoforkEquivSigmaCofork.functor.map f).hom = f.hom
• CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork_functor_obj_ι_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape} (I : CategoryTheory.Limits.MultispanIndex J C) [CategoryTheory.Limits.HasCoproduct I.left] [CategoryTheory.Limits.HasCoproduct I.right] (K : CategoryTheory.Limits.Multicofork I) (X : CategoryTheory.Limits.WalkingParallelPair) : (I.multicoforkEquivSigmaCofork.functor.obj K).ι.app X = CategoryTheory.Limits.WalkingParallelPair.rec (CategoryTheory.CategoryStruct.comp (I.sndSigmaMapOfIsColimit (CategoryTheory.Limits.colimit.cocone (CategoryTheory.Discrete.functor I.right)) (CategoryTheory.Limits.colimit.isColimit (CategoryTheory.Discrete.functor I.left))) (CategoryTheory.Limits.Cofan.IsColimit.desc (CategoryTheory.Limits.colimit.isColimit (CategoryTheory.Discrete.functor I.right)) K.π)) (CategoryTheory.Limits.Cofan.IsColimit.desc (CategoryTheory.Limits.colimit.isColimit (CategoryTheory.Discrete.functor I.right)) K.π) X
• CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork_inverse_obj_ι_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape} (I : CategoryTheory.Limits.MultispanIndex J C) [CategoryTheory.Limits.HasCoproduct I.left] [CategoryTheory.Limits.HasCoproduct I.right] (a : CategoryTheory.Limits.Cofork (I.fstSigmaMapOfIsColimit (CategoryTheory.Limits.colimit.cocone (CategoryTheory.Discrete.functor I.right)) (CategoryTheory.Limits.colimit.isColimit (CategoryTheory.Discrete.functor I.left))) (I.sndSigmaMapOfIsColimit (CategoryTheory.Limits.colimit.cocone (CategoryTheory.Discrete.functor I.right)) (CategoryTheory.Limits.colimit.isColimit (CategoryTheory.Discrete.functor I.left)))) (x : CategoryTheory.Limits.WalkingMultispan J) : (I.multicoforkEquivSigmaCofork.inverse.obj a).ι.app x = match x with | CategoryTheory.Limits.WalkingMultispan.left a_1 => CategoryTheory.CategoryStruct.comp (I.fst a_1) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofan.inj (CategoryTheory.Limits.colimit.cocone (CategoryTheory.Discrete.functor I.right)) (J.fst a_1)) a.π) | CategoryTheory.Limits.WalkingMultispan.right a_1 => CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofan.inj (CategoryTheory.Limits.colimit.cocone (CategoryTheory.Discrete.functor I.right)) a_1) a.π
• CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork_inverse_map_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape} (I : CategoryTheory.Limits.MultispanIndex J C) [CategoryTheory.Limits.HasCoproduct I.left] [CategoryTheory.Limits.HasCoproduct I.right] {K₁ K₂ : CategoryTheory.Limits.Cofork (I.fstSigmaMapOfIsColimit (CategoryTheory.Limits.colimit.cocone (CategoryTheory.Discrete.functor I.right)) (CategoryTheory.Limits.colimit.isColimit (CategoryTheory.Discrete.functor I.left))) (I.sndSigmaMapOfIsColimit (CategoryTheory.Limits.colimit.cocone (CategoryTheory.Discrete.functor I.right)) (CategoryTheory.Limits.colimit.isColimit (CategoryTheory.Discrete.functor I.left)))} (f : K₁ ⟶ K₂) : (I.multicoforkEquivSigmaCofork.inverse.map f).hom = f.hom
• CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork_unitIso_hom_app_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape} (I : CategoryTheory.Limits.MultispanIndex J C) [CategoryTheory.Limits.HasCoproduct I.left] [CategoryTheory.Limits.HasCoproduct I.right] (X : CategoryTheory.Limits.Multicofork I) : (I.multicoforkEquivSigmaCofork.unitIso.hom.app X).hom = CategoryTheory.CategoryStruct.id X.pt
• CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork_unitIso_inv_app_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape} (I : CategoryTheory.Limits.MultispanIndex J C) [CategoryTheory.Limits.HasCoproduct I.left] [CategoryTheory.Limits.HasCoproduct I.right] (X : CategoryTheory.Limits.Multicofork I) : (I.multicoforkEquivSigmaCofork.unitIso.inv.app X).hom = CategoryTheory.CategoryStruct.id X.pt
• CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork_counitIso_hom_app_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape} (I : CategoryTheory.Limits.MultispanIndex J C) [CategoryTheory.Limits.HasCoproduct I.left] [CategoryTheory.Limits.HasCoproduct I.right] (X : CategoryTheory.Limits.Cofork (I.fstSigmaMapOfIsColimit (CategoryTheory.Limits.colimit.cocone (CategoryTheory.Discrete.functor I.right)) (CategoryTheory.Limits.colimit.isColimit (CategoryTheory.Discrete.functor I.left))) (I.sndSigmaMapOfIsColimit (CategoryTheory.Limits.colimit.cocone (CategoryTheory.Discrete.functor I.right)) (CategoryTheory.Limits.colimit.isColimit (CategoryTheory.Discrete.functor I.left)))) : (I.multicoforkEquivSigmaCofork.counitIso.hom.app X).hom = CategoryTheory.CategoryStruct.id X.pt
• CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork_counitIso_inv_app_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape} (I : CategoryTheory.Limits.MultispanIndex J C) [CategoryTheory.Limits.HasCoproduct I.left] [CategoryTheory.Limits.HasCoproduct I.right] (X : CategoryTheory.Limits.Cofork (I.fstSigmaMapOfIsColimit (CategoryTheory.Limits.colimit.cocone (CategoryTheory.Discrete.functor I.right)) (CategoryTheory.Limits.colimit.isColimit (CategoryTheory.Discrete.functor I.left))) (I.sndSigmaMapOfIsColimit (CategoryTheory.Limits.colimit.cocone (CategoryTheory.Discrete.functor I.right)) (CategoryTheory.Limits.colimit.isColimit (CategoryTheory.Discrete.functor I.left)))) : (I.multicoforkEquivSigmaCofork.counitIso.inv.app X).hom = CategoryTheory.CategoryStruct.id X.pt
• CategoryTheory.Limits.DiagramOfCocones.mkOfHasColimits_obj 📋 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) : (CategoryTheory.Limits.DiagramOfCocones.mkOfHasColimits F).obj j = CategoryTheory.Limits.colimit.cocone (F.obj j)
• 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)
• PresheafOfModules.colimitAdjunction_homEquiv 📋 Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.IsCofiltered C] [CategoryTheory.InitiallySmall C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {cR : CategoryTheory.Limits.Cocone R} (hcR : CategoryTheory.Limits.IsColimit cR) (F : PresheafOfModules R) (G : ModuleCat ↑cR.pt) : (PresheafOfModules.colimitAdjunction hcR).homEquiv F G = ↑(PresheafOfModules.ModuleColimit.homEquiv hcR (CategoryTheory.Limits.colimit.isColimit F.presheaf))
• PresheafOfModules.colimitAdjunction_homEquiv_symm_apply 📋 Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.IsCofiltered C] [CategoryTheory.InitiallySmall C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {cR : CategoryTheory.Limits.Cocone R} (hcR : CategoryTheory.Limits.IsColimit cR) {F : PresheafOfModules R} {G : ModuleCat ↑cR.pt} (β : F ⟶ (PresheafOfModules.constFunctor cR).obj G) {X : Cᵒᵖ} (m : ↑(F.obj X)) : (CategoryTheory.ConcreteCategory.hom (((PresheafOfModules.colimitAdjunction hcR).homEquiv F G).symm β)) (PresheafOfModules.ModuleColimit.ιM m) = (CategoryTheory.ConcreteCategory.hom (β.app X)) m
• CategoryTheory.LiftLeftAdjoint.constructLeftAdjointEquiv_apply 📋 Mathlib.CategoryTheory.Adjunction.Lifting.Left
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {U : CategoryTheory.Functor B C} {F : CategoryTheory.Functor C B} (R : CategoryTheory.Functor A B) (F' : CategoryTheory.Functor C A) (adj₁ : F ⊣ U) (adj₂ : F' ⊣ R.comp U) [CategoryTheory.Limits.HasReflexiveCoequalizers A] (h : (X : B) → CategoryTheory.RegularEpi (adj₁.counit.app X)) (Y : A) (X : B) (a✝ : CategoryTheory.LiftLeftAdjoint.constructLeftAdjointObj R F' adj₁ adj₂ X ⟶ Y) : (CategoryTheory.LiftLeftAdjoint.constructLeftAdjointEquiv R F' adj₁ adj₂ h Y X) a✝ = (CategoryTheory.Limits.Cofork.IsColimit.homIso (CategoryTheory.LiftLeftAdjoint.counitCoequalises adj₁ h X) (R.obj Y)).symm ⟨(adj₁.homEquiv (U.obj X) (R.obj Y)).symm ((adj₂.homEquiv (U.obj X) Y) ↑((CategoryTheory.Limits.Cofork.IsColimit.homIso (CategoryTheory.Limits.colimit.isColimit (CategoryTheory.Limits.parallelPair (F'.map (U.map (adj₁.counit.app X))) (CategoryTheory.LiftLeftAdjoint.otherMap R F' adj₁ adj₂ X))) Y) a✝)), ⋯⟩
• CategoryTheory.LiftLeftAdjoint.constructLeftAdjointEquiv_symm_apply 📋 Mathlib.CategoryTheory.Adjunction.Lifting.Left
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {U : CategoryTheory.Functor B C} {F : CategoryTheory.Functor C B} (R : CategoryTheory.Functor A B) (F' : CategoryTheory.Functor C A) (adj₁ : F ⊣ U) (adj₂ : F' ⊣ R.comp U) [CategoryTheory.Limits.HasReflexiveCoequalizers A] (h : (X : B) → CategoryTheory.RegularEpi (adj₁.counit.app X)) (Y : A) (X : B) (a✝ : X ⟶ R.obj Y) : (CategoryTheory.LiftLeftAdjoint.constructLeftAdjointEquiv R F' adj₁ adj₂ h Y X).symm a✝ = (CategoryTheory.Limits.Cofork.IsColimit.homIso (CategoryTheory.Limits.colimit.isColimit (CategoryTheory.Limits.parallelPair (F'.map (U.map (adj₁.counit.app X))) (CategoryTheory.LiftLeftAdjoint.otherMap R F' adj₁ adj₂ X))) Y).symm ⟨(adj₂.homEquiv (U.obj X) Y).symm ((adj₁.homEquiv (U.obj X) (R.obj Y)) ↑((CategoryTheory.Limits.Cofork.IsColimit.homIso (CategoryTheory.LiftLeftAdjoint.counitCoequalises adj₁ h X) (R.obj Y)) a✝)), ⋯⟩
• CategoryTheory.Monad.MonadicityInternal.comparisonLeftAdjointHomEquiv_apply_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) (B : D) [CategoryTheory.Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))] (a✝ : CategoryTheory.Monad.MonadicityInternal.comparisonLeftAdjointObj adj A ⟶ B) : ((CategoryTheory.Monad.MonadicityInternal.comparisonLeftAdjointHomEquiv adj A B) a✝).f = ↑(((CategoryTheory.Limits.Cofork.IsColimit.homIso (CategoryTheory.Limits.colimit.isColimit (CategoryTheory.Limits.parallelPair (F.map A.a) (adj.counit.app (F.obj A.A)))) B).trans ((adj.homEquiv A.A B).subtypeEquiv ⋯)) a✝)
• CategoryTheory.Monad.MonadicityInternal.comparisonLeftAdjointHomEquiv_symm_apply 📋 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) (B : D) [CategoryTheory.Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))] (a✝ : A ⟶ (CategoryTheory.Monad.comparison adj).obj B) : (CategoryTheory.Monad.MonadicityInternal.comparisonLeftAdjointHomEquiv adj A B).symm a✝ = (((adj.homEquiv A.A B).symm.subtypeEquiv ⋯).trans (CategoryTheory.Limits.Cofork.IsColimit.homIso (CategoryTheory.Limits.colimit.isColimit (CategoryTheory.Limits.parallelPair (F.map A.a) (adj.counit.app (F.obj A.A)))) B).symm) ({ toFun := fun f => ⟨f.f, ⋯⟩, invFun := fun g => { f := ↑g, h := ⋯ }, left_inv := ⋯, right_inv := ⋯ } a✝)
• CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction_counit 📋 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))] : (CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction adj).counit = { app := fun Y => (((adj.homEquiv (G.obj Y) Y).symm.subtypeEquiv ⋯).trans (CategoryTheory.Limits.Cofork.IsColimit.homIso (CategoryTheory.Limits.colimit.isColimit (CategoryTheory.Limits.parallelPair (F.map (G.map (adj.counit.app Y))) (adj.counit.app (F.obj (G.obj Y))))) Y).symm) ({ toFun := fun f => ⟨f.f, ⋯⟩, invFun := fun g => { f := ↑g, h := ⋯ }, left_inv := ⋯, right_inv := ⋯ } (CategoryTheory.CategoryStruct.id ((CategoryTheory.Monad.comparison adj).obj Y))), naturality := ⋯ }

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