Loogle!

Result

Found 58 declarations mentioning CategoryTheory.Limits.ColimitPresentation.

• CategoryTheory.Limits.ColimitPresentation 📋 Mathlib.CategoryTheory.Limits.Presentation
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : Type w) [CategoryTheory.Category.{t, w} J] (X : C) : Type (max (max (max t u) v) w)
• CategoryTheory.Limits.ColimitPresentation.diag 📋 Mathlib.CategoryTheory.Limits.Presentation
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.Category.{t, w} J] {X : C} (self : CategoryTheory.Limits.ColimitPresentation J X) : CategoryTheory.Functor J C
• CategoryTheory.Limits.ColimitPresentation.self 📋 Mathlib.CategoryTheory.Limits.Presentation
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) : CategoryTheory.Limits.ColimitPresentation PUnit.{s + 1} X
• CategoryTheory.Limits.ColimitPresentation.cocone 📋 Mathlib.CategoryTheory.Limits.Presentation
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.Category.{t, w} J] {X : C} (pres : CategoryTheory.Limits.ColimitPresentation J X) : CategoryTheory.Limits.Cocone pres.diag
• CategoryTheory.Limits.ColimitPresentation.hasColimit 📋 Mathlib.CategoryTheory.Limits.Presentation
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.Category.{t, w} J] {X : C} (pres : CategoryTheory.Limits.ColimitPresentation J X) : CategoryTheory.Limits.HasColimit pres.diag
• CategoryTheory.Limits.ColimitPresentation.ofIso 📋 Mathlib.CategoryTheory.Limits.Presentation
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.Category.{t, w} J] {X : C} (P : CategoryTheory.Limits.ColimitPresentation J X) {Y : C} (e : X ≅ Y) : CategoryTheory.Limits.ColimitPresentation J Y
• CategoryTheory.Limits.ColimitPresentation.colimit 📋 Mathlib.CategoryTheory.Limits.Presentation
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.Category.{t, w} J] (F : CategoryTheory.Functor J C) [CategoryTheory.Limits.HasColimit F] : CategoryTheory.Limits.ColimitPresentation J (CategoryTheory.Limits.colimit F)
• CategoryTheory.Limits.ColimitPresentation.reindex 📋 Mathlib.CategoryTheory.Limits.Presentation
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.Category.{t, w} J] {X : C} (P : CategoryTheory.Limits.ColimitPresentation J X) {J' : Type u_1} [CategoryTheory.Category.{v_1, u_1} J'] (F : CategoryTheory.Functor J' J) [F.Final] : CategoryTheory.Limits.ColimitPresentation J' X
• CategoryTheory.Limits.ColimitPresentation.map 📋 Mathlib.CategoryTheory.Limits.Presentation
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.Category.{t, w} J] {X : C} (P : CategoryTheory.Limits.ColimitPresentation J X) {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesColimitsOfShape J F] : CategoryTheory.Limits.ColimitPresentation J (F.obj X)
• CategoryTheory.Limits.ColimitPresentation.changeDiag 📋 Mathlib.CategoryTheory.Limits.Presentation
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.Category.{t, w} J] {X : C} (P : CategoryTheory.Limits.ColimitPresentation J X) {F : CategoryTheory.Functor J C} (e : F ≅ P.diag) : CategoryTheory.Limits.ColimitPresentation J X
• CategoryTheory.Limits.ColimitPresentation.isColimit 📋 Mathlib.CategoryTheory.Limits.Presentation
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.Category.{t, w} J] {X : C} (self : CategoryTheory.Limits.ColimitPresentation J X) : CategoryTheory.Limits.IsColimit { pt := X, ι := self.ι }
• CategoryTheory.Limits.ColimitPresentation.ofIso_diag 📋 Mathlib.CategoryTheory.Limits.Presentation
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.Category.{t, w} J] {X : C} (P : CategoryTheory.Limits.ColimitPresentation J X) {Y : C} (e : X ≅ Y) : (P.ofIso e).diag = P.diag
• CategoryTheory.Limits.ColimitPresentation.changeDiag_diag 📋 Mathlib.CategoryTheory.Limits.Presentation
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.Category.{t, w} J] {X : C} (P : CategoryTheory.Limits.ColimitPresentation J X) {F : CategoryTheory.Functor J C} (e : F ≅ P.diag) : (P.changeDiag e).diag = F
• CategoryTheory.Limits.ColimitPresentation.ι 📋 Mathlib.CategoryTheory.Limits.Presentation
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.Category.{t, w} J] {X : C} (self : CategoryTheory.Limits.ColimitPresentation J X) : self.diag ⟶ (CategoryTheory.Functor.const J).obj X
• CategoryTheory.Limits.ColimitPresentation.reindex_diag 📋 Mathlib.CategoryTheory.Limits.Presentation
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.Category.{t, w} J] {X : C} (P : CategoryTheory.Limits.ColimitPresentation J X) {J' : Type u_1} [CategoryTheory.Category.{v_1, u_1} J'] (F : CategoryTheory.Functor J' J) [F.Final] : (P.reindex F).diag = F.comp P.diag
• CategoryTheory.Limits.ColimitPresentation.map_diag 📋 Mathlib.CategoryTheory.Limits.Presentation
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.Category.{t, w} J] {X : C} (P : CategoryTheory.Limits.ColimitPresentation J X) {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesColimitsOfShape J F] : (P.map F).diag = P.diag.comp F
• CategoryTheory.Limits.ColimitPresentation.mk 📋 Mathlib.CategoryTheory.Limits.Presentation
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.Category.{t, w} J] {X : C} (diag : CategoryTheory.Functor J C) (ι : diag ⟶ (CategoryTheory.Functor.const J).obj X) (isColimit : CategoryTheory.Limits.IsColimit { pt := X, ι := ι }) : CategoryTheory.Limits.ColimitPresentation J X
• CategoryTheory.Limits.ColimitPresentation.reindex_ι 📋 Mathlib.CategoryTheory.Limits.Presentation
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.Category.{t, w} J] {X : C} (P : CategoryTheory.Limits.ColimitPresentation J X) {J' : Type u_1} [CategoryTheory.Category.{v_1, u_1} J'] (F : CategoryTheory.Functor J' J) [F.Final] : (P.reindex F).ι = F.whiskerLeft P.ι
• CategoryTheory.Limits.ColimitPresentation.changeDiag_ι 📋 Mathlib.CategoryTheory.Limits.Presentation
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.Category.{t, w} J] {X : C} (P : CategoryTheory.Limits.ColimitPresentation J X) {F : CategoryTheory.Functor J C} (e : F ≅ P.diag) : (P.changeDiag e).ι = CategoryTheory.CategoryStruct.comp e.hom P.ι
• CategoryTheory.Limits.ColimitPresentation.ofIso_ι 📋 Mathlib.CategoryTheory.Limits.Presentation
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.Category.{t, w} J] {X : C} (P : CategoryTheory.Limits.ColimitPresentation J X) {Y : C} (e : X ≅ Y) : (P.ofIso e).ι = CategoryTheory.CategoryStruct.comp P.ι ((CategoryTheory.Functor.const J).map e.hom)
• CategoryTheory.Limits.ColimitPresentation.w 📋 Mathlib.CategoryTheory.Limits.Presentation
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.Category.{t, w} J] {X : C} (pres : CategoryTheory.Limits.ColimitPresentation J X) {i j : J} (f : i ⟶ j) : CategoryTheory.CategoryStruct.comp (pres.diag.map f) (pres.ι.app j) = pres.ι.app i
• CategoryTheory.Limits.ColimitPresentation.w_assoc 📋 Mathlib.CategoryTheory.Limits.Presentation
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.Category.{t, w} J] {X : C} (pres : CategoryTheory.Limits.ColimitPresentation J X) {i j : J} (f : i ⟶ j) {Z : C} (h : ((CategoryTheory.Functor.const J).obj X).obj j ⟶ Z) : CategoryTheory.CategoryStruct.comp (pres.diag.map f) (CategoryTheory.CategoryStruct.comp (pres.ι.app j) h) = CategoryTheory.CategoryStruct.comp (pres.ι.app i) h
• CategoryTheory.Limits.ColimitPresentation.map_ι 📋 Mathlib.CategoryTheory.Limits.Presentation
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.Category.{t, w} J] {X : C} (P : CategoryTheory.Limits.ColimitPresentation J X) {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesColimitsOfShape J F] : (P.map F).ι = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight P.ι F) (CategoryTheory.Functor.constComp J X F).hom
• CategoryTheory.ObjectProperty.ColimitOfShape.toColimitPresentation 📋 Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.ObjectProperty C} {J : Type u'} [CategoryTheory.Category.{v', u'} J] {X : C} (self : P.ColimitOfShape J X) : CategoryTheory.Limits.ColimitPresentation J X
• CategoryTheory.ObjectProperty.ColimitOfShape.mk 📋 Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.ObjectProperty C} {J : Type u'} [CategoryTheory.Category.{v', u'} J] {X : C} (toColimitPresentation : CategoryTheory.Limits.ColimitPresentation J X) (prop_diag_obj : ∀ (j : J), P (toColimitPresentation.diag.obj j)) : P.ColimitOfShape J X
• CategoryTheory.ObjectProperty.ColimitOfShape.ofIso_toColimitPresentation 📋 Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.ObjectProperty C} {J : Type u'} [CategoryTheory.Category.{v', u'} J] {X : C} (h : P.ColimitOfShape J X) {Y : C} (e : X ≅ Y) : (h.ofIso e).toColimitPresentation = h.ofIso e
• CategoryTheory.ObjectProperty.ColimitOfShape.ofLE_toColimitPresentation 📋 Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.ObjectProperty C} {J : Type u'} [CategoryTheory.Category.{v', u'} J] {X : C} (h : P.ColimitOfShape J X) {Q : CategoryTheory.ObjectProperty C} (hPQ : P ≤ Q) : (h.ofLE hPQ).toColimitPresentation = h.toColimitPresentation
• CategoryTheory.ObjectProperty.ColimitOfShape.colimit_toColimitPresentation 📋 Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.ObjectProperty C} {J : Type u'} [CategoryTheory.Category.{v', u'} J] (F : CategoryTheory.Functor J C) [CategoryTheory.Limits.HasColimit F] (hF : ∀ (j : J), P (F.obj j)) : (CategoryTheory.ObjectProperty.ColimitOfShape.colimit F hF).toColimitPresentation = CategoryTheory.Limits.ColimitPresentation.colimit F
• CategoryTheory.ObjectProperty.ColimitOfShape.reindex_toColimitPresentation 📋 Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.ObjectProperty C} {J : Type u'} [CategoryTheory.Category.{v', u'} J] {J' : Type u''} [CategoryTheory.Category.{v'', u''} J'] {X : C} (h : P.ColimitOfShape J X) (G : CategoryTheory.Functor J' J) [G.Final] : (h.reindex G).toColimitPresentation = h.reindex G
• CategoryTheory.ObjectProperty.colimitsClosure.of_colimitPresentation 📋 Mathlib.CategoryTheory.ObjectProperty.ColimitsClosure
  {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {α : Type t} {J : α → Type u'} [(a : α) → CategoryTheory.Category.{v', u'} (J a)] {X : C} {a : α} (pres : CategoryTheory.Limits.ColimitPresentation (J a) X) (h : ∀ (j : J a), P.colimitsClosure J (pres.diag.obj j)) : P.colimitsClosure J X
• CategoryTheory.Limits.ColimitPresentation.isCardinalPresentable 📋 Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {J : Type w} [CategoryTheory.SmallCategory J] (p : CategoryTheory.Limits.ColimitPresentation J X) (κ : Cardinal.{w}) [Fact κ.IsRegular] (h : ∀ (j : J), CategoryTheory.IsCardinalPresentable (p.diag.obj j) κ) [CategoryTheory.LocallySmall.{w, v, u} C] (κ' : Cardinal.{w}) [Fact κ'.IsRegular] : κ ≤ κ' → ∀ (hJ : HasCardinalLT (CategoryTheory.Arrow J) κ'), CategoryTheory.IsCardinalPresentable X κ'
• CategoryTheory.Limits.ColimitPresentation.Total 📋 Mathlib.CategoryTheory.Presentable.ColimitPresentation
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u_1} {I : J → Type u_2} [CategoryTheory.Category.{v_1, u_1} J] [(j : J) → CategoryTheory.Category.{u_3, u_2} (I j)] {D : CategoryTheory.Functor J C} (P : (j : J) → CategoryTheory.Limits.ColimitPresentation (I j) (D.obj j)) : Type (max u_2 u_1)
• CategoryTheory.Limits.ColimitPresentation.instCategoryTotal 📋 Mathlib.CategoryTheory.Presentable.ColimitPresentation
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u_1} {I : J → Type u_2} [CategoryTheory.Category.{v_1, u_1} J] [(j : J) → CategoryTheory.Category.{u_3, u_2} (I j)] {D : CategoryTheory.Functor J C} {P : (j : J) → CategoryTheory.Limits.ColimitPresentation (I j) (D.obj j)} : CategoryTheory.Category.{max v v_1, max u_2 u_1} (CategoryTheory.Limits.ColimitPresentation.Total P)
• CategoryTheory.Limits.ColimitPresentation.Total.mk 📋 Mathlib.CategoryTheory.Presentable.ColimitPresentation
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u_1} {I : J → Type u_2} [CategoryTheory.Category.{v_1, u_1} J] [(j : J) → CategoryTheory.Category.{u_3, u_2} (I j)] {D : CategoryTheory.Functor J C} (P : (j : J) → CategoryTheory.Limits.ColimitPresentation (I j) (D.obj j)) (i : J) (k : I i) : CategoryTheory.Limits.ColimitPresentation.Total P
• CategoryTheory.Limits.ColimitPresentation.instNonemptyTotalOfIsFiltered 📋 Mathlib.CategoryTheory.Presentable.ColimitPresentation
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} {I : J → Type w} [CategoryTheory.SmallCategory J] [(j : J) → CategoryTheory.SmallCategory (I j)] {D : CategoryTheory.Functor J C} {P : (j : J) → CategoryTheory.Limits.ColimitPresentation (I j) (D.obj j)} [CategoryTheory.IsFiltered J] [∀ (j : J), CategoryTheory.IsFiltered (I j)] : Nonempty (CategoryTheory.Limits.ColimitPresentation.Total P)
• CategoryTheory.Limits.ColimitPresentation.Total.Hom 📋 Mathlib.CategoryTheory.Presentable.ColimitPresentation
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u_1} {I : J → Type u_2} [CategoryTheory.Category.{v_1, u_1} J] [(j : J) → CategoryTheory.Category.{u_3, u_2} (I j)] {D : CategoryTheory.Functor J C} {P : (j : J) → CategoryTheory.Limits.ColimitPresentation (I j) (D.obj j)} (k l : CategoryTheory.Limits.ColimitPresentation.Total P) : Type (max v v_1)
• CategoryTheory.Limits.ColimitPresentation.instLocallySmallTotal 📋 Mathlib.CategoryTheory.Presentable.ColimitPresentation
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u_1} {I : J → Type u_2} [CategoryTheory.Category.{v_1, u_1} J] [(j : J) → CategoryTheory.Category.{u_3, u_2} (I j)] {D : CategoryTheory.Functor J C} {P : (j : J) → CategoryTheory.Limits.ColimitPresentation (I j) (D.obj j)} [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.LocallySmall.{w, v_1, u_1} J] : CategoryTheory.LocallySmall.{w, max v v_1, max u_2 u_1} (CategoryTheory.Limits.ColimitPresentation.Total P)
• CategoryTheory.Limits.ColimitPresentation.Total.Hom.base 📋 Mathlib.CategoryTheory.Presentable.ColimitPresentation
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u_1} {I : J → Type u_2} [CategoryTheory.Category.{v_1, u_1} J] [(j : J) → CategoryTheory.Category.{u_3, u_2} (I j)] {D : CategoryTheory.Functor J C} {P : (j : J) → CategoryTheory.Limits.ColimitPresentation (I j) (D.obj j)} {k l : CategoryTheory.Limits.ColimitPresentation.Total P} (self : k.Hom l) : k.fst ⟶ l.fst
• CategoryTheory.Limits.ColimitPresentation.instIsFilteredTotalOfIsFinitelyPresentableObjDiag 📋 Mathlib.CategoryTheory.Presentable.ColimitPresentation
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} {I : J → Type w} [CategoryTheory.SmallCategory J] [(j : J) → CategoryTheory.SmallCategory (I j)] {D : CategoryTheory.Functor J C} {P : (j : J) → CategoryTheory.Limits.ColimitPresentation (I j) (D.obj j)} [CategoryTheory.IsFiltered J] [∀ (j : J), CategoryTheory.IsFiltered (I j)] [∀ (j : J) (i : I j), CategoryTheory.IsFinitelyPresentable ((P j).diag.obj i)] : CategoryTheory.IsFiltered (CategoryTheory.Limits.ColimitPresentation.Total P)
• CategoryTheory.Limits.ColimitPresentation.Total.Hom.comp 📋 Mathlib.CategoryTheory.Presentable.ColimitPresentation
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u_1} {I : J → Type u_2} [CategoryTheory.Category.{v_1, u_1} J] [(j : J) → CategoryTheory.Category.{u_3, u_2} (I j)] {D : CategoryTheory.Functor J C} {P : (j : J) → CategoryTheory.Limits.ColimitPresentation (I j) (D.obj j)} {k l m : CategoryTheory.Limits.ColimitPresentation.Total P} (f : k.Hom l) (g : l.Hom m) : k.Hom m
• CategoryTheory.Limits.ColimitPresentation.id_base 📋 Mathlib.CategoryTheory.Presentable.ColimitPresentation
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u_1} {I : J → Type u_2} [CategoryTheory.Category.{v_1, u_1} J] [(j : J) → CategoryTheory.Category.{u_3, u_2} (I j)] {D : CategoryTheory.Functor J C} {P : (j : J) → CategoryTheory.Limits.ColimitPresentation (I j) (D.obj j)} (x✝ : CategoryTheory.Limits.ColimitPresentation.Total P) : (CategoryTheory.CategoryStruct.id x✝).base = CategoryTheory.CategoryStruct.id x✝.fst
• CategoryTheory.Limits.ColimitPresentation.bind 📋 Mathlib.CategoryTheory.Presentable.ColimitPresentation
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} {I : J → Type w} [CategoryTheory.SmallCategory J] [(j : J) → CategoryTheory.SmallCategory (I j)] {X : C} (P : CategoryTheory.Limits.ColimitPresentation J X) (Q : (j : J) → CategoryTheory.Limits.ColimitPresentation (I j) (P.diag.obj j)) [∀ (j : J), CategoryTheory.IsFiltered (I j)] [∀ (j : J) (i : I j), CategoryTheory.IsFinitelyPresentable ((Q j).diag.obj i)] : CategoryTheory.Limits.ColimitPresentation (CategoryTheory.Limits.ColimitPresentation.Total Q) X
• CategoryTheory.Limits.ColimitPresentation.Total.Hom.comp_base 📋 Mathlib.CategoryTheory.Presentable.ColimitPresentation
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u_1} {I : J → Type u_2} [CategoryTheory.Category.{v_1, u_1} J] [(j : J) → CategoryTheory.Category.{u_3, u_2} (I j)] {D : CategoryTheory.Functor J C} {P : (j : J) → CategoryTheory.Limits.ColimitPresentation (I j) (D.obj j)} {k l m : CategoryTheory.Limits.ColimitPresentation.Total P} (f : k.Hom l) (g : l.Hom m) : (f.comp g).base = CategoryTheory.CategoryStruct.comp f.base g.base
• CategoryTheory.Limits.ColimitPresentation.Total.Hom.hom 📋 Mathlib.CategoryTheory.Presentable.ColimitPresentation
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u_1} {I : J → Type u_2} [CategoryTheory.Category.{v_1, u_1} J] [(j : J) → CategoryTheory.Category.{u_3, u_2} (I j)] {D : CategoryTheory.Functor J C} {P : (j : J) → CategoryTheory.Limits.ColimitPresentation (I j) (D.obj j)} {k l : CategoryTheory.Limits.ColimitPresentation.Total P} (self : k.Hom l) : (P k.fst).diag.obj k.snd ⟶ (P l.fst).diag.obj l.snd
• CategoryTheory.Limits.ColimitPresentation.comp_base 📋 Mathlib.CategoryTheory.Presentable.ColimitPresentation
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u_1} {I : J → Type u_2} [CategoryTheory.Category.{v_1, u_1} J] [(j : J) → CategoryTheory.Category.{u_3, u_2} (I j)] {D : CategoryTheory.Functor J C} {P : (j : J) → CategoryTheory.Limits.ColimitPresentation (I j) (D.obj j)} {X✝ Y✝ Z✝ : CategoryTheory.Limits.ColimitPresentation.Total P} (f : X✝.Hom Y✝) (g : Y✝.Hom Z✝) : (CategoryTheory.CategoryStruct.comp f g).base = CategoryTheory.CategoryStruct.comp f.base g.base
• CategoryTheory.Limits.ColimitPresentation.bind_diag_obj 📋 Mathlib.CategoryTheory.Presentable.ColimitPresentation
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} {I : J → Type w} [CategoryTheory.SmallCategory J] [(j : J) → CategoryTheory.SmallCategory (I j)] {X : C} (P : CategoryTheory.Limits.ColimitPresentation J X) (Q : (j : J) → CategoryTheory.Limits.ColimitPresentation (I j) (P.diag.obj j)) [∀ (j : J), CategoryTheory.IsFiltered (I j)] [∀ (j : J) (i : I j), CategoryTheory.IsFinitelyPresentable ((Q j).diag.obj i)] (k : CategoryTheory.Limits.ColimitPresentation.Total Q) : (P.bind Q).diag.obj k = (Q k.fst).diag.obj k.snd
• CategoryTheory.Limits.ColimitPresentation.id_hom 📋 Mathlib.CategoryTheory.Presentable.ColimitPresentation
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u_1} {I : J → Type u_2} [CategoryTheory.Category.{v_1, u_1} J] [(j : J) → CategoryTheory.Category.{u_3, u_2} (I j)] {D : CategoryTheory.Functor J C} {P : (j : J) → CategoryTheory.Limits.ColimitPresentation (I j) (D.obj j)} (x✝ : CategoryTheory.Limits.ColimitPresentation.Total P) : (CategoryTheory.CategoryStruct.id x✝).hom = CategoryTheory.CategoryStruct.id ((P x✝.fst).diag.obj x✝.snd)
• CategoryTheory.Limits.ColimitPresentation.Total.exists_hom_of_hom 📋 Mathlib.CategoryTheory.Presentable.ColimitPresentation
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} {I : J → Type w} [CategoryTheory.SmallCategory J] [(j : J) → CategoryTheory.SmallCategory (I j)] {D : CategoryTheory.Functor J C} {P : (j : J) → CategoryTheory.Limits.ColimitPresentation (I j) (D.obj j)} {j j' : J} (i : I j) (u : j ⟶ j') [CategoryTheory.IsFiltered (I j')] [CategoryTheory.IsFinitelyPresentable ((P j).diag.obj i)] : ∃ i' f, f.base = u
• CategoryTheory.Limits.ColimitPresentation.Total.Hom.ext 📋 Mathlib.CategoryTheory.Presentable.ColimitPresentation
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {J : Type u_1} {I : J → Type u_2} {inst✝¹ : CategoryTheory.Category.{v_1, u_1} J} {inst✝² : (j : J) → CategoryTheory.Category.{u_3, u_2} (I j)} {D : CategoryTheory.Functor J C} {P : (j : J) → CategoryTheory.Limits.ColimitPresentation (I j) (D.obj j)} {k l : CategoryTheory.Limits.ColimitPresentation.Total P} {x y : k.Hom l} (base : x.base = y.base) (hom : x.hom = y.hom) : x = y
• CategoryTheory.Limits.ColimitPresentation.Total.Hom.ext_iff 📋 Mathlib.CategoryTheory.Presentable.ColimitPresentation
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {J : Type u_1} {I : J → Type u_2} {inst✝¹ : CategoryTheory.Category.{v_1, u_1} J} {inst✝² : (j : J) → CategoryTheory.Category.{u_3, u_2} (I j)} {D : CategoryTheory.Functor J C} {P : (j : J) → CategoryTheory.Limits.ColimitPresentation (I j) (D.obj j)} {k l : CategoryTheory.Limits.ColimitPresentation.Total P} {x y : k.Hom l} : x = y ↔ x.base = y.base ∧ x.hom = y.hom
• CategoryTheory.Limits.ColimitPresentation.bind_diag_map 📋 Mathlib.CategoryTheory.Presentable.ColimitPresentation
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} {I : J → Type w} [CategoryTheory.SmallCategory J] [(j : J) → CategoryTheory.SmallCategory (I j)] {X : C} (P : CategoryTheory.Limits.ColimitPresentation J X) (Q : (j : J) → CategoryTheory.Limits.ColimitPresentation (I j) (P.diag.obj j)) [∀ (j : J), CategoryTheory.IsFiltered (I j)] [∀ (j : J) (i : I j), CategoryTheory.IsFinitelyPresentable ((Q j).diag.obj i)] {k l : CategoryTheory.Limits.ColimitPresentation.Total Q} (f : k ⟶ l) : (P.bind Q).diag.map f = f.hom
• CategoryTheory.Limits.ColimitPresentation.Total.Hom.comp_hom 📋 Mathlib.CategoryTheory.Presentable.ColimitPresentation
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u_1} {I : J → Type u_2} [CategoryTheory.Category.{v_1, u_1} J] [(j : J) → CategoryTheory.Category.{u_3, u_2} (I j)] {D : CategoryTheory.Functor J C} {P : (j : J) → CategoryTheory.Limits.ColimitPresentation (I j) (D.obj j)} {k l m : CategoryTheory.Limits.ColimitPresentation.Total P} (f : k.Hom l) (g : l.Hom m) : (f.comp g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom
• CategoryTheory.Limits.ColimitPresentation.comp_hom 📋 Mathlib.CategoryTheory.Presentable.ColimitPresentation
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u_1} {I : J → Type u_2} [CategoryTheory.Category.{v_1, u_1} J] [(j : J) → CategoryTheory.Category.{u_3, u_2} (I j)] {D : CategoryTheory.Functor J C} {P : (j : J) → CategoryTheory.Limits.ColimitPresentation (I j) (D.obj j)} {X✝ Y✝ Z✝ : CategoryTheory.Limits.ColimitPresentation.Total P} (f : X✝.Hom Y✝) (g : Y✝.Hom Z✝) : (CategoryTheory.CategoryStruct.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom
• CategoryTheory.Limits.ColimitPresentation.Total.Hom.w 📋 Mathlib.CategoryTheory.Presentable.ColimitPresentation
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u_1} {I : J → Type u_2} [CategoryTheory.Category.{v_1, u_1} J] [(j : J) → CategoryTheory.Category.{u_3, u_2} (I j)] {D : CategoryTheory.Functor J C} {P : (j : J) → CategoryTheory.Limits.ColimitPresentation (I j) (D.obj j)} {k l : CategoryTheory.Limits.ColimitPresentation.Total P} (self : k.Hom l) : CategoryTheory.CategoryStruct.comp ((P k.fst).ι.app k.snd) (D.map self.base) = CategoryTheory.CategoryStruct.comp self.hom ((P l.fst).ι.app l.snd)
• CategoryTheory.Limits.ColimitPresentation.Total.Hom.w_assoc 📋 Mathlib.CategoryTheory.Presentable.ColimitPresentation
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u_1} {I : J → Type u_2} [CategoryTheory.Category.{v_1, u_1} J] [(j : J) → CategoryTheory.Category.{u_3, u_2} (I j)] {D : CategoryTheory.Functor J C} {P : (j : J) → CategoryTheory.Limits.ColimitPresentation (I j) (D.obj j)} {k l : CategoryTheory.Limits.ColimitPresentation.Total P} (self : k.Hom l) {Z : C} (h : D.obj l.fst ⟶ Z) : CategoryTheory.CategoryStruct.comp ((P k.fst).ι.app k.snd) (CategoryTheory.CategoryStruct.comp (D.map self.base) h) = CategoryTheory.CategoryStruct.comp self.hom (CategoryTheory.CategoryStruct.comp ((P l.fst).ι.app l.snd) h)
• CategoryTheory.Limits.ColimitPresentation.Total.Hom.mk 📋 Mathlib.CategoryTheory.Presentable.ColimitPresentation
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u_1} {I : J → Type u_2} [CategoryTheory.Category.{v_1, u_1} J] [(j : J) → CategoryTheory.Category.{u_3, u_2} (I j)] {D : CategoryTheory.Functor J C} {P : (j : J) → CategoryTheory.Limits.ColimitPresentation (I j) (D.obj j)} {k l : CategoryTheory.Limits.ColimitPresentation.Total P} (base : k.fst ⟶ l.fst) (hom : (P k.fst).diag.obj k.snd ⟶ (P l.fst).diag.obj l.snd) (w : CategoryTheory.CategoryStruct.comp ((P k.fst).ι.app k.snd) (D.map base) = CategoryTheory.CategoryStruct.comp hom ((P l.fst).ι.app l.snd) := by cat_disch) : k.Hom l
• CategoryTheory.Limits.ColimitPresentation.bind_ι_app 📋 Mathlib.CategoryTheory.Presentable.ColimitPresentation
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} {I : J → Type w} [CategoryTheory.SmallCategory J] [(j : J) → CategoryTheory.SmallCategory (I j)] {X : C} (P : CategoryTheory.Limits.ColimitPresentation J X) (Q : (j : J) → CategoryTheory.Limits.ColimitPresentation (I j) (P.diag.obj j)) [∀ (j : J), CategoryTheory.IsFiltered (I j)] [∀ (j : J) (i : I j), CategoryTheory.IsFinitelyPresentable ((Q j).diag.obj i)] (k : CategoryTheory.Limits.ColimitPresentation.Total Q) : (P.bind Q).ι.app k = CategoryTheory.CategoryStruct.comp ((Q k.fst).ι.app k.snd) (P.ι.app k.fst)
• CategoryTheory.ObjectProperty.of_essentiallySmall_index 📋 Mathlib.CategoryTheory.ObjectProperty.Ind
  {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {X : C} {J : Type u_1} [CategoryTheory.Category.{v_1, u_1} J] [CategoryTheory.EssentiallySmall.{w, v_1, u_1} J] [CategoryTheory.IsFiltered J] (pres : CategoryTheory.Limits.ColimitPresentation J X) (h : ∀ (i : J), P (pres.diag.obj i)) : P.ind X

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