Loogle!

Result

Found 66 declarations mentioning CategoryTheory.Limits.LimitCone.

• CategoryTheory.Limits.LimitCone 📋 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) : Type (max (max u u₁) v)
• CategoryTheory.Limits.getLimitCone 📋 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.HasLimit F] : CategoryTheory.Limits.LimitCone F
• CategoryTheory.Limits.HasLimit.mk 📋 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} (d : CategoryTheory.Limits.LimitCone F) : CategoryTheory.Limits.HasLimit F
• CategoryTheory.Limits.LimitCone.cone 📋 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} (self : CategoryTheory.Limits.LimitCone F) : CategoryTheory.Limits.Cone F
• CategoryTheory.Limits.HasLimit.exists_limit 📋 Mathlib.CategoryTheory.Limits.HasLimits
  {J : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} J} {C : Type u} {inst✝¹ : CategoryTheory.Category.{v, u} C} {F : CategoryTheory.Functor J C} [self : CategoryTheory.Limits.HasLimit F] : Nonempty (CategoryTheory.Limits.LimitCone F)
• CategoryTheory.Limits.HasLimit.mk' 📋 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} (exists_limit : Nonempty (CategoryTheory.Limits.LimitCone F)) : CategoryTheory.Limits.HasLimit F
• CategoryTheory.Limits.LimitCone.isLimit 📋 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} (self : CategoryTheory.Limits.LimitCone F) : CategoryTheory.Limits.IsLimit self.cone
• CategoryTheory.Limits.LimitCone.mk 📋 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} (cone : CategoryTheory.Limits.Cone F) (isLimit : CategoryTheory.Limits.IsLimit cone) : CategoryTheory.Limits.LimitCone F
• CategoryTheory.Limits.limit.isoLimitCone 📋 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.HasLimit F] (t : CategoryTheory.Limits.LimitCone F) : CategoryTheory.Limits.limit F ≅ t.cone.pt
• CategoryTheory.Limits.limit.isoLimitCone_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.HasLimit F] (t : CategoryTheory.Limits.LimitCone F) (j : J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.isoLimitCone t).hom (t.cone.π.app j) = CategoryTheory.Limits.limit.π F j
• CategoryTheory.Limits.limit.isoLimitCone_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.HasLimit F] (t : CategoryTheory.Limits.LimitCone F) (j : J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.isoLimitCone t).inv (CategoryTheory.Limits.limit.π F j) = t.cone.π.app j
• CategoryTheory.Limits.limit.isoLimitCone_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.HasLimit F] (t : CategoryTheory.Limits.LimitCone F) (j : J) {Z : C} (h : F.obj j ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.isoLimitCone t).hom (CategoryTheory.CategoryStruct.comp (t.cone.π.app j) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π F j) h
• CategoryTheory.Limits.limit.isoLimitCone_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.HasLimit F] (t : CategoryTheory.Limits.LimitCone F) (j : J) {Z : C} (h : F.obj j ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.isoLimitCone t).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π F j) h) = CategoryTheory.CategoryStruct.comp (t.cone.π.app j) h
• CategoryTheory.Limits.limit.pre_eq 📋 Mathlib.CategoryTheory.Limits.HasLimits
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor J C} [CategoryTheory.Limits.HasLimit F] {E : CategoryTheory.Functor K J} [CategoryTheory.Limits.HasLimit (E.comp F)] (s : CategoryTheory.Limits.LimitCone (E.comp F)) (t : CategoryTheory.Limits.LimitCone F) : CategoryTheory.Limits.limit.pre F E = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.isoLimitCone t).hom (CategoryTheory.CategoryStruct.comp (s.isLimit.lift (CategoryTheory.Limits.Cone.whisker E t.cone)) (CategoryTheory.Limits.limit.isoLimitCone s).inv)
• CategoryTheory.Limits.limitConeOfUnique 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [Unique β] (f : β → C) : CategoryTheory.Limits.LimitCone (CategoryTheory.Discrete.functor f)
• CategoryTheory.Limits.BinaryFan.associatorOfLimitCone 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] (L : (X Y : C) → CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.pair X Y)) (X Y Z : C) : (L (L X Y).cone.pt Z).cone.pt ≅ (L X (L Y Z).cone.pt).cone.pt
• CategoryTheory.Limits.kernelForkBiproductToSubtype 📋 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.LimitCone (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.biproduct.toSubtype f p) 0)
• CategoryTheory.Limits.combineCones 📋 Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) (c : (k : K) → CategoryTheory.Limits.LimitCone (F.flip.obj k)) : CategoryTheory.Limits.Cone F
• CategoryTheory.Limits.combinedIsLimit 📋 Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) (c : (k : K) → CategoryTheory.Limits.LimitCone (F.flip.obj k)) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.combineCones F c)
• CategoryTheory.Limits.combineCones_pt_obj 📋 Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) (c : (k : K) → CategoryTheory.Limits.LimitCone (F.flip.obj k)) (k : K) : (CategoryTheory.Limits.combineCones F c).pt.obj k = (c k).cone.pt
• CategoryTheory.Limits.evaluateCombinedCones 📋 Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) (c : (k : K) → CategoryTheory.Limits.LimitCone (F.flip.obj k)) (k : K) : ((CategoryTheory.evaluation K C).obj k).mapCone (CategoryTheory.Limits.combineCones F c) ≅ (c k).cone
• CategoryTheory.Limits.combineCones_pt_map 📋 Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) (c : (k : K) → CategoryTheory.Limits.LimitCone (F.flip.obj k)) {k₁ k₂ : K} (f : k₁ ⟶ k₂) : (CategoryTheory.Limits.combineCones F c).pt.map f = (c k₂).isLimit.lift { pt := (c k₁).cone.pt, π := CategoryTheory.CategoryStruct.comp (c k₁).cone.π (F.flip.map f) }
• CategoryTheory.Limits.combineCones_π_app_app 📋 Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) (c : (k : K) → CategoryTheory.Limits.LimitCone (F.flip.obj k)) (j : J) (k : K) : ((CategoryTheory.Limits.combineCones F c).π.app j).app k = (c k).cone.π.app j
• limitConeOfTerminalAndPullbacks 📋 Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasPullbacks C] (F : CategoryTheory.Functor (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) C) : CategoryTheory.Limits.LimitCone F
• CategoryTheory.Limits.Types.terminalLimitCone 📋 Mathlib.CategoryTheory.Limits.Types.Products
  : CategoryTheory.Limits.LimitCone (CategoryTheory.Functor.empty (Type u))
• CategoryTheory.Limits.Types.binaryProductLimitCone 📋 Mathlib.CategoryTheory.Limits.Types.Products
  (X Y : Type u) : CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.pair X Y)
• CategoryTheory.Limits.Types.productLimitCone 📋 Mathlib.CategoryTheory.Limits.Types.Products
  {J : Type v} (F : J → Type (max v u)) : CategoryTheory.Limits.LimitCone (CategoryTheory.Discrete.functor F)
• CategoryTheory.Limits.Types.Small.productLimitCone 📋 Mathlib.CategoryTheory.Limits.Types.Products
  {J : Type v} (F : J → Type u) [Small.{u, v} J] : CategoryTheory.Limits.LimitCone (CategoryTheory.Discrete.functor F)
• CategoryTheory.Functor.Initial.limitConeComp 📋 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.Initial] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {G : CategoryTheory.Functor D E} (t : CategoryTheory.Limits.LimitCone G) : CategoryTheory.Limits.LimitCone (F.comp G)
• CategoryTheory.Functor.Initial.limitConeOfComp 📋 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.Initial] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {G : CategoryTheory.Functor D E} (t : CategoryTheory.Limits.LimitCone (F.comp G)) : CategoryTheory.Limits.LimitCone G
• CategoryTheory.Functor.Initial.limitConeComp_cone 📋 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.Initial] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {G : CategoryTheory.Functor D E} (t : CategoryTheory.Limits.LimitCone G) : (CategoryTheory.Functor.Initial.limitConeComp F t).cone = CategoryTheory.Limits.Cone.whisker F t.cone
• CategoryTheory.Functor.Initial.limitConeOfComp_cone 📋 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.Initial] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {G : CategoryTheory.Functor D E} (t : CategoryTheory.Limits.LimitCone (F.comp G)) : (CategoryTheory.Functor.Initial.limitConeOfComp F t).cone = CategoryTheory.Functor.Initial.extendCone.obj t.cone
• CategoryTheory.Functor.Initial.limitConeComp_isLimit 📋 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.Initial] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {G : CategoryTheory.Functor D E} (t : CategoryTheory.Limits.LimitCone G) : (CategoryTheory.Functor.Initial.limitConeComp F t).isLimit = (CategoryTheory.Functor.Initial.isLimitWhiskerEquiv F t.cone).symm t.isLimit
• CategoryTheory.Functor.Initial.limitConeOfComp_isLimit 📋 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.Initial] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {G : CategoryTheory.Functor D E} (t : CategoryTheory.Limits.LimitCone (F.comp G)) : (CategoryTheory.Functor.Initial.limitConeOfComp F t).isLimit = (CategoryTheory.Functor.Initial.isLimitExtendConeEquiv F t.cone).symm t.isLimit
• CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.tensorObj 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (ℬ : (X Y : C) → CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.pair X Y)) (X Y : C) : C
• CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (𝒯 : CategoryTheory.Limits.LimitCone (CategoryTheory.Functor.empty C)) (ℬ : (X Y : C) → CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.pair X Y)) : CategoryTheory.CartesianMonoidalCategory C
• CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.tensorHom 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (ℬ : (X Y : C) → CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.pair X Y)) {X₁ X₂ Y₁ Y₂ : C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) : CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.tensorObj ℬ X₁ X₂ ⟶ CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.tensorObj ℬ Y₁ Y₂
• CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.id_tensorHom_id 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (ℬ : (X Y : C) → CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.pair X Y)) (X Y : C) : CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.tensorHom ℬ (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id Y) = CategoryTheory.CategoryStruct.id (CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.tensorObj ℬ X Y)
• CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.tensorHom_comp_tensorHom 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (ℬ : (X Y : C) → CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.pair X Y)) {X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.tensorHom ℬ f₁ f₂) (CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.tensorHom ℬ g₁ g₂) = CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.tensorHom ℬ (CategoryTheory.CategoryStruct.comp f₁ g₁) (CategoryTheory.CategoryStruct.comp f₂ g₂)
• CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.leftUnitor_naturality 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (𝒯 : CategoryTheory.Limits.LimitCone (CategoryTheory.Functor.empty C)) (ℬ : (X Y : C) → CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.pair X Y)) {X₁ X₂ : C} (f : X₁ ⟶ X₂) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.tensorHom ℬ (CategoryTheory.CategoryStruct.id 𝒯.cone.pt) f) (CategoryTheory.Limits.BinaryFan.leftUnitor 𝒯.isLimit (ℬ 𝒯.cone.pt X₂).isLimit).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryFan.leftUnitor 𝒯.isLimit (ℬ 𝒯.cone.pt X₁).isLimit).hom f
• CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.rightUnitor_naturality 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (𝒯 : CategoryTheory.Limits.LimitCone (CategoryTheory.Functor.empty C)) (ℬ : (X Y : C) → CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.pair X Y)) {X₁ X₂ : C} (f : X₁ ⟶ X₂) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.tensorHom ℬ f (CategoryTheory.CategoryStruct.id 𝒯.cone.pt)) (CategoryTheory.Limits.BinaryFan.rightUnitor 𝒯.isLimit (ℬ X₂ 𝒯.cone.pt).isLimit).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryFan.rightUnitor 𝒯.isLimit (ℬ X₁ 𝒯.cone.pt).isLimit).hom f
• CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.associator_naturality 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (ℬ : (X Y : C) → CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.pair X Y)) {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.tensorHom ℬ (CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.tensorHom ℬ f₁ f₂) f₃) (CategoryTheory.Limits.BinaryFan.associatorOfLimitCone ℬ Y₁ Y₂ Y₃).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryFan.associatorOfLimitCone ℬ X₁ X₂ X₃).hom (CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.tensorHom ℬ f₁ (CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.tensorHom ℬ f₂ f₃))
• CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.triangle 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (𝒯 : CategoryTheory.Limits.LimitCone (CategoryTheory.Functor.empty C)) (ℬ : (X Y : C) → CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.pair X Y)) (X Y : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryFan.associatorOfLimitCone ℬ X 𝒯.cone.pt Y).hom (CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.tensorHom ℬ (CategoryTheory.CategoryStruct.id X) (CategoryTheory.Limits.BinaryFan.leftUnitor 𝒯.isLimit (ℬ 𝒯.cone.pt Y).isLimit).hom) = CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.tensorHom ℬ (CategoryTheory.Limits.BinaryFan.rightUnitor 𝒯.isLimit (ℬ X 𝒯.cone.pt).isLimit).hom (CategoryTheory.CategoryStruct.id Y)
• CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.pentagon 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (ℬ : (X Y : C) → CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.pair X Y)) (W X Y Z : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.tensorHom ℬ (CategoryTheory.Limits.BinaryFan.associatorOfLimitCone ℬ W X Y).hom (CategoryTheory.CategoryStruct.id Z)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryFan.associatorOfLimitCone ℬ W (CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.tensorObj ℬ X Y) Z).hom (CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.tensorHom ℬ (CategoryTheory.CategoryStruct.id W) (CategoryTheory.Limits.BinaryFan.associatorOfLimitCone ℬ X Y Z).hom)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryFan.associatorOfLimitCone ℬ (CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.tensorObj ℬ W X) Y Z).hom (CategoryTheory.Limits.BinaryFan.associatorOfLimitCone ℬ W X (CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.tensorObj ℬ Y Z)).hom
• CategoryTheory.Limits.limitConeOfEqualizerAndProduct 📋 Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J C) [CategoryTheory.Limits.HasLimit (CategoryTheory.Discrete.functor F.obj)] [CategoryTheory.Limits.HasLimit (CategoryTheory.Discrete.functor fun f => F.obj f.fst.2)] [CategoryTheory.Limits.HasEqualizers C] : CategoryTheory.Limits.LimitCone F
• AddCommGrpCat.binaryProductLimitCone 📋 Mathlib.Algebra.Category.Grp.Biproducts
  (G H : AddCommGrpCat) : CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.pair G H)
• AddCommGrpCat.HasLimit.productLimitCone 📋 Mathlib.Algebra.Category.Grp.Biproducts
  {J : Type w} (f : J → AddCommGrpCat) : CategoryTheory.Limits.LimitCone (CategoryTheory.Discrete.functor f)
• CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetLimitCone 📋 Mathlib.CategoryTheory.Limits.Constructions.Filtered
  {C : Type u} [CategoryTheory.Category.{v, u} C] {α : Type w} [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasLimitsOfShape (Finset (CategoryTheory.Discrete α))ᵒᵖ C] (F : CategoryTheory.Functor (CategoryTheory.Discrete α) C) : CategoryTheory.Limits.LimitCone F
• AddGrpCat.binaryProductLimitCone 📋 Mathlib.Algebra.Category.Grp.CartesianMonoidal
  (G H : AddGrpCat) : CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.pair G H)
• CommGrpCat.binaryProductLimitCone 📋 Mathlib.Algebra.Category.Grp.CartesianMonoidal
  (G H : CommGrpCat) : CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.pair G H)
• GrpCat.binaryProductLimitCone 📋 Mathlib.Algebra.Category.Grp.CartesianMonoidal
  (G H : GrpCat) : CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.pair G H)
• CategoryTheory.Limits.Types.pullbackLimitCone 📋 Mathlib.CategoryTheory.Limits.Types.Pullbacks
  {X Y Z : Type u} (f : X ⟶ Z) (g : Y ⟶ Z) : CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.cospan f g)
• ModuleCat.HasLimit.productLimitCone 📋 Mathlib.Algebra.Category.ModuleCat.Biproducts
  {R : Type u} [Ring R] {J : Type w} (f : J → ModuleCat R) : CategoryTheory.Limits.LimitCone (CategoryTheory.Discrete.functor f)
• ModuleCat.binaryProductLimitCone 📋 Mathlib.Algebra.Category.ModuleCat.Biproducts
  {R : Type u} [Ring R] (M N : ModuleCat R) : CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.pair M N)
• CategoryTheory.Limits.Types.equalizerLimit 📋 Mathlib.CategoryTheory.Limits.Types.Equalizers
  {Y Z : Type u} {g h : Y ⟶ Z} : CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.parallelPair g h)
• Preorder.limitConeOfIsGLB 📋 Mathlib.CategoryTheory.Limits.Preorder
  {C : Type u} [Preorder C] {J : Type u'} [CategoryTheory.Category.{v, u'} J] (F : CategoryTheory.Functor J C) {pt : C} (h : IsGLB (Set.range F.obj) pt) : CategoryTheory.Limits.LimitCone F
• CategoryTheory.Limits.CompleteLattice.limitCone 📋 Mathlib.CategoryTheory.Limits.Lattice
  {α : Type u} [CompleteLattice α] {J : Type w} [CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor J α) : CategoryTheory.Limits.LimitCone F
• CategoryTheory.Limits.CompleteLattice.finiteLimitCone 📋 Mathlib.CategoryTheory.Limits.Lattice
  {α : Type u} {J : Type w} [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] [SemilatticeInf α] [OrderTop α] (F : CategoryTheory.Functor J α) : CategoryTheory.Limits.LimitCone F
• CategoryTheory.CechNerveTerminalFrom.wideCospan.limitCone 📋 Mathlib.AlgebraicTopology.CechNerve
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] (ι : Type w) [CategoryTheory.Limits.HasFiniteProducts C] [Finite ι] (X : C) : CategoryTheory.Limits.LimitCone (CategoryTheory.CechNerveTerminalFrom.wideCospan ι X)
• Action.ofMulActionLimitCone 📋 Mathlib.CategoryTheory.Action.Concrete
  {ι : Type v} (G : Type (max v u)) [Monoid G] (F : ι → Type (max v u)) [(i : ι) → MulAction G (F i)] : CategoryTheory.Limits.LimitCone (CategoryTheory.Discrete.functor fun i => Action.ofMulAction G (F i))
• CategoryTheory.FunctorToTypes.binaryProductLimitCone 📋 Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
  {C : Type u} [CategoryTheory.Category.{v, u} C] (F G : CategoryTheory.Functor C (Type w)) : CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.pair F G)
• CategoryTheory.Limits.WeakLimitCone.ofLimitCone 📋 Mathlib.CategoryTheory.Limits.WeakLimits.Basic
  {J : Type u_1} [CategoryTheory.Category.{v_1, u_1} J] {C : Type u_3} [CategoryTheory.Category.{v_3, u_3} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.LimitCone F) : CategoryTheory.Limits.WeakLimitCone F
• Profinite.lim 📋 Mathlib.Topology.Category.Profinite.AsLimit
  (X : Profinite) : CategoryTheory.Limits.LimitCone X.diagram
• LightProfinite.lim 📋 Mathlib.Topology.Category.LightProfinite.AsLimit
  (S : LightProfinite) : CategoryTheory.Limits.LimitCone S.diagram
• Profinite.lim' 📋 Mathlib.Topology.Category.Profinite.Extend
  (S : Profinite) : CategoryTheory.Limits.LimitCone S.diagram'
• LightProfinite.lim' 📋 Mathlib.Topology.Category.LightProfinite.Extend
  (S : LightProfinite) : CategoryTheory.Limits.LimitCone S.diagram'

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