Loogle!

Result

Found 39 declarations mentioning CategoryTheory.SmallObject.functorObjTop.

• CategoryTheory.SmallObject.functorObjTop 📋 Mathlib.CategoryTheory.SmallObject.Construction
  {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C} (πX : X ⟶ S) [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C] : ∐ CategoryTheory.SmallObject.functorObjSrcFamily f πX ⟶ X
• CategoryTheory.SmallObject.functorObj 📋 Mathlib.CategoryTheory.SmallObject.Construction
  {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C} (πX : X ⟶ S) [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C] [CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX) (CategoryTheory.SmallObject.functorObjLeft f πX)] : C
• CategoryTheory.SmallObject.ιFunctorObj 📋 Mathlib.CategoryTheory.SmallObject.Construction
  {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C} (πX : X ⟶ S) [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C] [CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX) (CategoryTheory.SmallObject.functorObjLeft f πX)] : X ⟶ CategoryTheory.SmallObject.functorObj f πX
• CategoryTheory.SmallObject.πFunctorObj 📋 Mathlib.CategoryTheory.SmallObject.Construction
  {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C} (πX : X ⟶ S) [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C] [CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX) (CategoryTheory.SmallObject.functorObjLeft f πX)] : CategoryTheory.SmallObject.functorObj f πX ⟶ S
• CategoryTheory.SmallObject.attachCellsιFunctorObj 📋 Mathlib.CategoryTheory.SmallObject.Construction
  {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C} (πX : X ⟶ S) [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C] [CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX) (CategoryTheory.SmallObject.functorObjLeft f πX)] : HomotopicalAlgebra.AttachCells f (CategoryTheory.SmallObject.ιFunctorObj f πX)
• CategoryTheory.SmallObject.attachCellsιFunctorObjOfSmall 📋 Mathlib.CategoryTheory.SmallObject.Construction
  {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C} (πX : X ⟶ S) [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C] [CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX) (CategoryTheory.SmallObject.functorObjLeft f πX)] [CategoryTheory.LocallySmall.{t, v, u} C] [Small.{t, w} I] : HomotopicalAlgebra.AttachCells f (CategoryTheory.SmallObject.ιFunctorObj f πX)
• CategoryTheory.SmallObject.instSmallιAttachCellsιFunctorObj 📋 Mathlib.CategoryTheory.SmallObject.Construction
  {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C} (πX : X ⟶ S) [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C] [CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX) (CategoryTheory.SmallObject.functorObjLeft f πX)] [CategoryTheory.LocallySmall.{t, v, u} C] [Small.{t, w} I] : Small.{t, max v w} (CategoryTheory.SmallObject.attachCellsιFunctorObj f πX).ι
• CategoryTheory.SmallObject.ιFunctorObj_πFunctorObj 📋 Mathlib.CategoryTheory.SmallObject.Construction
  {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C} (πX : X ⟶ S) [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C] [CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX) (CategoryTheory.SmallObject.functorObjLeft f πX)] : CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.ιFunctorObj f πX) (CategoryTheory.SmallObject.πFunctorObj f πX) = πX
• CategoryTheory.SmallObject.attachCellsιFunctorObj_ι 📋 Mathlib.CategoryTheory.SmallObject.Construction
  {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C} (πX : X ⟶ S) [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C] [CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX) (CategoryTheory.SmallObject.functorObjLeft f πX)] : (CategoryTheory.SmallObject.attachCellsιFunctorObj f πX).ι = CategoryTheory.SmallObject.FunctorObjIndex f πX
• CategoryTheory.SmallObject.attachCellsιFunctorObj_π 📋 Mathlib.CategoryTheory.SmallObject.Construction
  {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C} (πX : X ⟶ S) [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C] [CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX) (CategoryTheory.SmallObject.functorObjLeft f πX)] (x : CategoryTheory.SmallObject.FunctorObjIndex f πX) : (CategoryTheory.SmallObject.attachCellsιFunctorObj f πX).π x = x.i
• CategoryTheory.SmallObject.functorMap_id 📋 Mathlib.CategoryTheory.SmallObject.Construction
  {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S : C} (X : C) {πX : X ⟶ S} [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C] [CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX) (CategoryTheory.SmallObject.functorObjLeft f πX)] : CategoryTheory.SmallObject.functorMap f (CategoryTheory.CategoryStruct.id (CategoryTheory.Arrow.mk πX)) = CategoryTheory.CategoryStruct.id (CategoryTheory.SmallObject.functorObj f πX)
• CategoryTheory.SmallObject.ρFunctorObj 📋 Mathlib.CategoryTheory.SmallObject.Construction
  {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C} (πX : X ⟶ S) [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C] [CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX) (CategoryTheory.SmallObject.functorObjLeft f πX)] : ∐ CategoryTheory.SmallObject.functorObjTgtFamily f πX ⟶ CategoryTheory.SmallObject.functorObj f πX
• CategoryTheory.SmallObject.ιFunctorObj_πFunctorObj_assoc 📋 Mathlib.CategoryTheory.SmallObject.Construction
  {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C} (πX : X ⟶ S) [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C] [CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX) (CategoryTheory.SmallObject.functorObjLeft f πX)] {Z : C} (h : S ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.ιFunctorObj f πX) (CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.πFunctorObj f πX) h) = CategoryTheory.CategoryStruct.comp πX h
• CategoryTheory.SmallObject.attachCellsιFunctorObj_g₁ 📋 Mathlib.CategoryTheory.SmallObject.Construction
  {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C} (πX : X ⟶ S) [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C] [CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX) (CategoryTheory.SmallObject.functorObjLeft f πX)] : (CategoryTheory.SmallObject.attachCellsιFunctorObj f πX).g₁ = CategoryTheory.SmallObject.functorObjTop f πX
• CategoryTheory.SmallObject.attachCellsιFunctorObj_g₂ 📋 Mathlib.CategoryTheory.SmallObject.Construction
  {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C} (πX : X ⟶ S) [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C] [CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX) (CategoryTheory.SmallObject.functorObjLeft f πX)] : (CategoryTheory.SmallObject.attachCellsιFunctorObj f πX).g₂ = CategoryTheory.SmallObject.ρFunctorObj f πX
• CategoryTheory.SmallObject.ιFunctorObj_extension 📋 Mathlib.CategoryTheory.SmallObject.Construction
  {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C} {πX : X ⟶ S} [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C] [CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX) (CategoryTheory.SmallObject.functorObjLeft f πX)] {i : I} (t : A i ⟶ X) (b : B i ⟶ S) (sq : CategoryTheory.CommSq t (f i) πX b) : ∃ l, CategoryTheory.CategoryStruct.comp (f i) l = CategoryTheory.CategoryStruct.comp t (CategoryTheory.SmallObject.ιFunctorObj f πX) ∧ CategoryTheory.CategoryStruct.comp l (CategoryTheory.SmallObject.πFunctorObj f πX) = b
• CategoryTheory.SmallObject.functorObj_isPushout 📋 Mathlib.CategoryTheory.SmallObject.Construction
  {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C} (πX : X ⟶ S) [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C] [CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX) (CategoryTheory.SmallObject.functorObjLeft f πX)] : CategoryTheory.IsPushout (CategoryTheory.SmallObject.functorObjTop f πX) (CategoryTheory.SmallObject.functorObjLeft f πX) (CategoryTheory.SmallObject.ιFunctorObj f πX) (CategoryTheory.SmallObject.ρFunctorObj f πX)
• CategoryTheory.SmallObject.ρFunctorObj_π 📋 Mathlib.CategoryTheory.SmallObject.Construction
  {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C} (πX : X ⟶ S) [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C] [CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX) (CategoryTheory.SmallObject.functorObjLeft f πX)] : CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.ρFunctorObj f πX) (CategoryTheory.SmallObject.πFunctorObj f πX) = CategoryTheory.SmallObject.π'FunctorObj f πX
• CategoryTheory.SmallObject.attachCellsιFunctorObj_cofan₁ 📋 Mathlib.CategoryTheory.SmallObject.Construction
  {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C} (πX : X ⟶ S) [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C] [CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX) (CategoryTheory.SmallObject.functorObjLeft f πX)] : (CategoryTheory.SmallObject.attachCellsιFunctorObj f πX).cofan₁ = CategoryTheory.Limits.Cofan.mk (∐ fun i => A i.i) (CategoryTheory.Limits.Sigma.ι fun i => A i.i)
• CategoryTheory.SmallObject.attachCellsιFunctorObj_cofan₂ 📋 Mathlib.CategoryTheory.SmallObject.Construction
  {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C} (πX : X ⟶ S) [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C] [CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX) (CategoryTheory.SmallObject.functorObjLeft f πX)] : (CategoryTheory.SmallObject.attachCellsιFunctorObj f πX).cofan₂ = CategoryTheory.Limits.Cofan.mk (∐ fun i => B i.i) (CategoryTheory.Limits.Sigma.ι fun i => B i.i)
• CategoryTheory.SmallObject.attachCellsιFunctorObj_m 📋 Mathlib.CategoryTheory.SmallObject.Construction
  {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C} (πX : X ⟶ S) [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C] [CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX) (CategoryTheory.SmallObject.functorObjLeft f πX)] : (CategoryTheory.SmallObject.attachCellsιFunctorObj f πX).m = CategoryTheory.SmallObject.functorObjLeft f πX
• CategoryTheory.SmallObject.functorMap 📋 Mathlib.CategoryTheory.SmallObject.Construction
  {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S T X Y : C} {πX : X ⟶ S} {πY : Y ⟶ T} (τ : CategoryTheory.Arrow.mk πX ⟶ CategoryTheory.Arrow.mk πY) [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C] [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πY)) C] [CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX) (CategoryTheory.SmallObject.functorObjLeft f πX)] [CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πY) (CategoryTheory.SmallObject.functorObjLeft f πY)] : CategoryTheory.SmallObject.functorObj f πX ⟶ CategoryTheory.SmallObject.functorObj f πY
• CategoryTheory.SmallObject.functorMapSrc_functorObjTop 📋 Mathlib.CategoryTheory.SmallObject.Construction
  {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S T X Y : C} {πX : X ⟶ S} {πY : Y ⟶ T} (τ : CategoryTheory.Arrow.mk πX ⟶ CategoryTheory.Arrow.mk πY) [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C] [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πY)) C] : CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.functorMapSrc f τ) (CategoryTheory.SmallObject.functorObjTop f πY) = CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.functorObjTop f πX) (CategoryTheory.Arrow.Hom.left τ)
• CategoryTheory.SmallObject.attachCellsιFunctorObj_isColimit₁ 📋 Mathlib.CategoryTheory.SmallObject.Construction
  {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C} (πX : X ⟶ S) [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C] [CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX) (CategoryTheory.SmallObject.functorObjLeft f πX)] : (CategoryTheory.SmallObject.attachCellsιFunctorObj f πX).isColimit₁ = CategoryTheory.Limits.coproductIsCoproduct fun i => A i.i
• CategoryTheory.SmallObject.attachCellsιFunctorObj_isColimit₂ 📋 Mathlib.CategoryTheory.SmallObject.Construction
  {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C} (πX : X ⟶ S) [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C] [CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX) (CategoryTheory.SmallObject.functorObjLeft f πX)] : (CategoryTheory.SmallObject.attachCellsιFunctorObj f πX).isColimit₂ = CategoryTheory.Limits.coproductIsCoproduct fun i => B i.i
• CategoryTheory.SmallObject.ρFunctorObj_π_assoc 📋 Mathlib.CategoryTheory.SmallObject.Construction
  {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C} (πX : X ⟶ S) [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C] [CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX) (CategoryTheory.SmallObject.functorObjLeft f πX)] {Z : C} (h : S ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.ρFunctorObj f πX) (CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.πFunctorObj f πX) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.π'FunctorObj f πX) h
• CategoryTheory.SmallObject.FunctorObjIndex.comm 📋 Mathlib.CategoryTheory.SmallObject.Construction
  {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C} (πX : X ⟶ S) [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C] [CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX) (CategoryTheory.SmallObject.functorObjLeft f πX)] (x : CategoryTheory.SmallObject.FunctorObjIndex f πX) : CategoryTheory.CategoryStruct.comp (f x.i) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (CategoryTheory.SmallObject.functorObjTgtFamily f πX) x) (CategoryTheory.SmallObject.ρFunctorObj f πX)) = CategoryTheory.CategoryStruct.comp x.t (CategoryTheory.SmallObject.ιFunctorObj f πX)
• CategoryTheory.SmallObject.functorMapSrc_functorObjTop_assoc 📋 Mathlib.CategoryTheory.SmallObject.Construction
  {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S T X Y : C} {πX : X ⟶ S} {πY : Y ⟶ T} (τ : CategoryTheory.Arrow.mk πX ⟶ CategoryTheory.Arrow.mk πY) [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C] [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πY)) C] {Z : C} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.functorMapSrc f τ) (CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.functorObjTop f πY) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.functorObjTop f πX) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.left τ) h)
• CategoryTheory.SmallObject.functorMap_π 📋 Mathlib.CategoryTheory.SmallObject.Construction
  {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S T X Y : C} {πX : X ⟶ S} {πY : Y ⟶ T} (τ : CategoryTheory.Arrow.mk πX ⟶ CategoryTheory.Arrow.mk πY) [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C] [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πY)) C] [CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX) (CategoryTheory.SmallObject.functorObjLeft f πX)] [CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πY) (CategoryTheory.SmallObject.functorObjLeft f πY)] : CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.functorMap f τ) (CategoryTheory.SmallObject.πFunctorObj f πY) = CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.πFunctorObj f πX) (CategoryTheory.Arrow.Hom.right τ)
• CategoryTheory.SmallObject.ιFunctorObj_naturality 📋 Mathlib.CategoryTheory.SmallObject.Construction
  {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S T X Y : C} {πX : X ⟶ S} {πY : Y ⟶ T} (τ : CategoryTheory.Arrow.mk πX ⟶ CategoryTheory.Arrow.mk πY) [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C] [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πY)) C] [CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX) (CategoryTheory.SmallObject.functorObjLeft f πX)] [CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πY) (CategoryTheory.SmallObject.functorObjLeft f πY)] : CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.ιFunctorObj f πX) (CategoryTheory.SmallObject.functorMap f τ) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.left τ) (CategoryTheory.SmallObject.ιFunctorObj f πY)
• CategoryTheory.SmallObject.ιFunctorObj_extension' 📋 Mathlib.CategoryTheory.SmallObject.Construction
  {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C} {πX : X ⟶ S} [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C] [CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX) (CategoryTheory.SmallObject.functorObjLeft f πX)] {X' S' Z' : C} (πX' : X' ⟶ S') (ι' : X' ⟶ Z') (πZ' : Z' ⟶ S') (fac' : CategoryTheory.CategoryStruct.comp ι' πZ' = πX') (eX : X' ≅ X) (eS : S' ≅ S) (eZ : Z' ≅ CategoryTheory.SmallObject.functorObj f πX) (commι : CategoryTheory.CategoryStruct.comp ι' eZ.hom = CategoryTheory.CategoryStruct.comp eX.hom (CategoryTheory.SmallObject.ιFunctorObj f πX)) (commπ : CategoryTheory.CategoryStruct.comp πZ' eS.hom = CategoryTheory.CategoryStruct.comp eZ.hom (CategoryTheory.SmallObject.πFunctorObj f πX)) {i : I} (t : A i ⟶ X') (b : B i ⟶ S') (fac : CategoryTheory.CategoryStruct.comp t πX' = CategoryTheory.CategoryStruct.comp (f i) b) : ∃ l, CategoryTheory.CategoryStruct.comp (f i) l = CategoryTheory.CategoryStruct.comp t ι' ∧ CategoryTheory.CategoryStruct.comp l πZ' = b
• CategoryTheory.SmallObject.functorObj_comm 📋 Mathlib.CategoryTheory.SmallObject.Construction
  {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C} (πX : X ⟶ S) [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C] [CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX) (CategoryTheory.SmallObject.functorObjLeft f πX)] : CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.functorObjTop f πX) (CategoryTheory.SmallObject.ιFunctorObj f πX) = CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.functorObjLeft f πX) (CategoryTheory.SmallObject.ρFunctorObj f πX)
• CategoryTheory.SmallObject.functorMap_π_assoc 📋 Mathlib.CategoryTheory.SmallObject.Construction
  {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S T X Y : C} {πX : X ⟶ S} {πY : Y ⟶ T} (τ : CategoryTheory.Arrow.mk πX ⟶ CategoryTheory.Arrow.mk πY) [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C] [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πY)) C] [CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX) (CategoryTheory.SmallObject.functorObjLeft f πX)] [CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πY) (CategoryTheory.SmallObject.functorObjLeft f πY)] {Z : C} (h : T ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.functorMap f τ) (CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.πFunctorObj f πY) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.πFunctorObj f πX) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.right τ) h)
• CategoryTheory.SmallObject.ιFunctorObj_naturality_assoc 📋 Mathlib.CategoryTheory.SmallObject.Construction
  {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S T X Y : C} {πX : X ⟶ S} {πY : Y ⟶ T} (τ : CategoryTheory.Arrow.mk πX ⟶ CategoryTheory.Arrow.mk πY) [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C] [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πY)) C] [CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX) (CategoryTheory.SmallObject.functorObjLeft f πX)] [CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πY) (CategoryTheory.SmallObject.functorObjLeft f πY)] {Z : C} (h : CategoryTheory.SmallObject.functorObj f πY ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.ιFunctorObj f πX) (CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.functorMap f τ) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.left τ) (CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.ιFunctorObj f πY) h)
• CategoryTheory.SmallObject.FunctorObjIndex.comm_assoc 📋 Mathlib.CategoryTheory.SmallObject.Construction
  {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C} (πX : X ⟶ S) [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C] [CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX) (CategoryTheory.SmallObject.functorObjLeft f πX)] (x : CategoryTheory.SmallObject.FunctorObjIndex f πX) {Z : C} (h : CategoryTheory.SmallObject.functorObj f πX ⟶ Z) : CategoryTheory.CategoryStruct.comp (f x.i) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (CategoryTheory.SmallObject.functorObjTgtFamily f πX) x) (CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.ρFunctorObj f πX) h)) = CategoryTheory.CategoryStruct.comp x.t (CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.ιFunctorObj f πX) h)
• CategoryTheory.SmallObject.functorObj_comm_assoc 📋 Mathlib.CategoryTheory.SmallObject.Construction
  {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C} (πX : X ⟶ S) [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C] [CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX) (CategoryTheory.SmallObject.functorObjLeft f πX)] {Z : C} (h : CategoryTheory.SmallObject.functorObj f πX ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.functorObjTop f πX) (CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.ιFunctorObj f πX) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.functorObjLeft f πX) (CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.ρFunctorObj f πX) h)
• CategoryTheory.SmallObject.relativeCellComplexιObjFObjSuccIso 📋 Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
  {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.MorphismProperty C) (κ : Cardinal.{w}) [Fact κ.IsRegular] [OrderBot κ.ord.ToType] [I.IsCardinalForSmallObjectArgument κ] {X Y : C} (f : X ⟶ Y) (j : κ.ord.ToType) : (CategoryTheory.SmallObject.relativeCellComplexιObj I κ f).F.obj (Order.succ j) ≅ CategoryTheory.SmallObject.functorObj I.homFamily (((CategoryTheory.SmallObject.iterationFunctor I κ).obj j).obj (CategoryTheory.Arrow.mk f)).hom
• CategoryTheory.SmallObject.ιFunctorObj_eq 📋 Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
  {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.MorphismProperty C) (κ : Cardinal.{w}) [Fact κ.IsRegular] [OrderBot κ.ord.ToType] [I.IsCardinalForSmallObjectArgument κ] {X Y : C} (f : X ⟶ Y) (j : κ.ord.ToType) : CategoryTheory.SmallObject.ιFunctorObj I.homFamily (((CategoryTheory.SmallObject.iterationFunctor I κ).obj j).obj (CategoryTheory.Arrow.mk f)).hom = CategoryTheory.CategoryStruct.comp ((CategoryTheory.SmallObject.relativeCellComplexιObj I κ f).F.map (CategoryTheory.homOfLE ⋯)) (CategoryTheory.SmallObject.relativeCellComplexιObjFObjSuccIso I κ f j).hom
• CategoryTheory.SmallObject.πFunctorObj_eq 📋 Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
  {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.MorphismProperty C) (κ : Cardinal.{w}) [Fact κ.IsRegular] [OrderBot κ.ord.ToType] [I.IsCardinalForSmallObjectArgument κ] {X Y : C} (f : X ⟶ Y) (j : κ.ord.ToType) : CategoryTheory.SmallObject.πFunctorObj I.homFamily (((CategoryTheory.SmallObject.iterationFunctor I κ).obj j).obj (CategoryTheory.Arrow.mk f)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.relativeCellComplexιObjFObjSuccIso I κ f j).inv (CategoryTheory.CategoryStruct.comp ((CategoryTheory.SmallObject.relativeCellComplexιObj I κ f).incl.app (Order.succ j)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.πObj I κ f) (CategoryTheory.SmallObject.iterationFunctorObjObjRightIso I κ (CategoryTheory.Arrow.mk f) j).inv))

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