Loogle!

Result

Found 59 declarations mentioning CategoryTheory.Limits.LimitCone.cone.

• 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.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.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_cone_pt 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [Unique β] (f : β → C) : (CategoryTheory.Limits.limitConeOfUnique f).cone.pt = f default
• CategoryTheory.Limits.limitConeOfUnique_cone_π 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [Unique β] (f : β → C) : (CategoryTheory.Limits.limitConeOfUnique f).cone.π = CategoryTheory.Discrete.natTrans fun x => match x with | { as := j } => CategoryTheory.eqToHom ⋯
• 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.limitBiconeOfUnique_isBilimit_isLimit 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [Unique J] (f : J → C) : (CategoryTheory.Limits.limitBiconeOfUnique f).isBilimit.isLimit = (CategoryTheory.Limits.limitConeOfUnique f).isLimit
• CategoryTheory.Limits.kernelForkBiproductToSubtype_cone 📋 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.kernelForkBiproductToSubtype f p).cone = CategoryTheory.Limits.KernelFork.ofι (CategoryTheory.Limits.biproduct.fromSubtype f pᶜ) ⋯
• CategoryTheory.Limits.kernelBiproductπ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.kernelBiproductπIso f i).inv = CategoryTheory.Limits.limit.lift (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.biproduct.π f i) 0) (CategoryTheory.Limits.KernelFork.ofι (CategoryTheory.Limits.biproduct.fromSubtype f fun j => ¬j = i) ⋯)
• CategoryTheory.Limits.kernelBiproductπ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.kernelBiproductπIso f i).hom = (CategoryTheory.Limits.biproduct.isLimitFromSubtype f i).lift (CategoryTheory.Limits.limit.cone (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.biproduct.π f i) 0))
• CategoryTheory.Limits.kernelBiproductToSubtypeIso_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.kernelBiproductToSubtypeIso f p).inv = CategoryTheory.Limits.limit.lift (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.biproduct.toSubtype f p) 0) (CategoryTheory.Limits.KernelFork.ofι (CategoryTheory.Limits.biproduct.fromSubtype f pᶜ) ⋯)
• CategoryTheory.Limits.kernelBiproductToSubtypeIso_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.kernelBiproductToSubtypeIso f p).hom = (CategoryTheory.Limits.KernelFork.IsLimit.ofι (CategoryTheory.Limits.biproduct.fromSubtype f pᶜ) ⋯ (fun {x} g x_1 => CategoryTheory.CategoryStruct.comp g (CategoryTheory.Limits.biproduct.toSubtype f pᶜ)) ⋯ ⋯).lift (CategoryTheory.Limits.limit.cone (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.biproduct.toSubtype f p) 0))
• CategoryTheory.Limits.kernelBiprodFstIso_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.kernelBiprodFstIso.inv = CategoryTheory.Limits.limit.lift (CategoryTheory.Limits.parallelPair CategoryTheory.Limits.biprod.fst 0) (CategoryTheory.Limits.biprod.fstKernelFork X Y)
• CategoryTheory.Limits.kernelBiprodSndIso_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.kernelBiprodSndIso.inv = CategoryTheory.Limits.limit.lift (CategoryTheory.Limits.parallelPair CategoryTheory.Limits.biprod.snd 0) (CategoryTheory.Limits.biprod.sndKernelFork X Y)
• CategoryTheory.Limits.kernelBiprodFstIso_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.kernelBiprodFstIso.hom = (CategoryTheory.Limits.biprod.isKernelFstKernelFork X Y).lift (CategoryTheory.Limits.limit.cone (CategoryTheory.Limits.parallelPair CategoryTheory.Limits.biprod.fst 0))
• CategoryTheory.Limits.kernelBiprodSndIso_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.kernelBiprodSndIso.hom = (CategoryTheory.Limits.biprod.isKernelSndKernelFork X Y).lift (CategoryTheory.Limits.limit.cone (CategoryTheory.Limits.parallelPair CategoryTheory.Limits.biprod.snd 0))
• 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
• CategoryTheory.Limits.Types.binaryProductLimitCone_cone 📋 Mathlib.CategoryTheory.Limits.Types.Products
  (X Y : Type u) : (CategoryTheory.Limits.Types.binaryProductLimitCone X Y).cone = CategoryTheory.Limits.Types.binaryProductCone X Y
• 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.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
• AddCommGrpCat.HasLimit.productLimitCone_cone_pt_coe 📋 Mathlib.Algebra.Category.Grp.Biproducts
  {J : Type w} (f : J → AddCommGrpCat) : ↑(AddCommGrpCat.HasLimit.productLimitCone f).cone.pt = ((j : J) → ↑(f j))
• AddCommGrpCat.binaryProductLimitCone_cone_pt 📋 Mathlib.Algebra.Category.Grp.Biproducts
  (G H : AddCommGrpCat) : (G.binaryProductLimitCone H).cone.pt = AddCommGrpCat.of (↑G × ↑H)
• AddCommGrpCat.HasLimit.productLimitCone_cone_π 📋 Mathlib.Algebra.Category.Grp.Biproducts
  {J : Type w} (f : J → AddCommGrpCat) : (AddCommGrpCat.HasLimit.productLimitCone f).cone.π = CategoryTheory.Discrete.natTrans fun j => AddCommGrpCat.ofHom (Pi.evalAddMonoidHom (fun j => ↑(f j)) j.as)
• AddCommGrpCat.binaryProductLimitCone_cone_π_app_left 📋 Mathlib.Algebra.Category.Grp.Biproducts
  (G H : AddCommGrpCat) : (G.binaryProductLimitCone H).cone.π.app { as := CategoryTheory.Limits.WalkingPair.left } = AddCommGrpCat.ofHom (AddMonoidHom.fst ↑G ↑H)
• AddCommGrpCat.binaryProductLimitCone_cone_π_app_right 📋 Mathlib.Algebra.Category.Grp.Biproducts
  (G H : AddCommGrpCat) : (G.binaryProductLimitCone H).cone.π.app { as := CategoryTheory.Limits.WalkingPair.right } = AddCommGrpCat.ofHom (AddMonoidHom.snd ↑G ↑H)
• CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetLimitCone_cone_pt 📋 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.ProductsFromFiniteCofiltered.liftToFinsetLimitCone F).cone.pt = CategoryTheory.Limits.limit (CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetObj F)
• CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetLimitCone_cone_π_app 📋 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) (j : CategoryTheory.Discrete α) : (CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetLimitCone F).cone.π.app j = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetObj F) (Opposite.op {j})) (CategoryTheory.Limits.Pi.π (fun x => F.obj ↑x) ⟨j, ⋯⟩)
• AddGrpCat.binaryProductLimitCone_cone_pt 📋 Mathlib.Algebra.Category.Grp.CartesianMonoidal
  (G H : AddGrpCat) : (G.binaryProductLimitCone H).cone.pt = AddGrpCat.of (↑G × ↑H)
• CommGrpCat.binaryProductLimitCone_cone_pt 📋 Mathlib.Algebra.Category.Grp.CartesianMonoidal
  (G H : CommGrpCat) : (G.binaryProductLimitCone H).cone.pt = CommGrpCat.of (↑G × ↑H)
• GrpCat.binaryProductLimitCone_cone_pt 📋 Mathlib.Algebra.Category.Grp.CartesianMonoidal
  (G H : GrpCat) : (G.binaryProductLimitCone H).cone.pt = GrpCat.of (↑G × ↑H)
• CategoryTheory.Limits.Types.pullbackLimitCone_cone 📋 Mathlib.CategoryTheory.Limits.Types.Pullbacks
  {X Y Z : Type u} (f : X ⟶ Z) (g : Y ⟶ Z) : (CategoryTheory.Limits.Types.pullbackLimitCone f g).cone = CategoryTheory.Limits.Types.pullbackCone f g
• ModuleCat.HasLimit.productLimitCone_cone_pt_carrier 📋 Mathlib.Algebra.Category.ModuleCat.Biproducts
  {R : Type u} [Ring R] {J : Type w} (f : J → ModuleCat R) : ↑(ModuleCat.HasLimit.productLimitCone f).cone.pt = ((j : J) → ↑(f j))
• ModuleCat.binaryProductLimitCone_cone_pt 📋 Mathlib.Algebra.Category.ModuleCat.Biproducts
  {R : Type u} [Ring R] (M N : ModuleCat R) : (M.binaryProductLimitCone N).cone.pt = ModuleCat.of R (↑M × ↑N)
• ModuleCat.binaryProductLimitCone_cone_π_app_left 📋 Mathlib.Algebra.Category.ModuleCat.Biproducts
  {R : Type u} [Ring R] (M N : ModuleCat R) : (M.binaryProductLimitCone N).cone.π.app { as := CategoryTheory.Limits.WalkingPair.left } = ModuleCat.ofHom (LinearMap.fst R ↑M ↑N)
• ModuleCat.binaryProductLimitCone_cone_π_app_right 📋 Mathlib.Algebra.Category.ModuleCat.Biproducts
  {R : Type u} [Ring R] (M N : ModuleCat R) : (M.binaryProductLimitCone N).cone.π.app { as := CategoryTheory.Limits.WalkingPair.right } = ModuleCat.ofHom (LinearMap.snd R ↑M ↑N)
• ModuleCat.HasLimit.productLimitCone_cone_π 📋 Mathlib.Algebra.Category.ModuleCat.Biproducts
  {R : Type u} [Ring R] {J : Type w} (f : J → ModuleCat R) : (ModuleCat.HasLimit.productLimitCone f).cone.π = CategoryTheory.Discrete.natTrans fun j => ModuleCat.ofHom (LinearMap.proj j.as)
• Preorder.limitConeOfIsGLB_cone 📋 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) : (Preorder.limitConeOfIsGLB F h).cone = Preorder.coneOfLowerBound F ⋯
• CategoryTheory.Limits.CompleteLattice.limitCone_cone_pt 📋 Mathlib.CategoryTheory.Limits.Lattice
  {α : Type u} [CompleteLattice α] {J : Type w} [CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor J α) : (CategoryTheory.Limits.CompleteLattice.limitCone F).cone.pt = iInf F.obj
• CategoryTheory.Limits.CompleteLattice.finiteLimitCone_cone_pt 📋 Mathlib.CategoryTheory.Limits.Lattice
  {α : Type u} {J : Type w} [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] [SemilatticeInf α] [OrderTop α] (F : CategoryTheory.Functor J α) : (CategoryTheory.Limits.CompleteLattice.finiteLimitCone F).cone.pt = Finset.univ.inf F.obj
• CategoryTheory.Limits.CompleteLattice.finiteLimitCone_cone_π_app 📋 Mathlib.CategoryTheory.Limits.Lattice
  {α : Type u} {J : Type w} [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] [SemilatticeInf α] [OrderTop α] (F : CategoryTheory.Functor J α) (x✝ : J) : (CategoryTheory.Limits.CompleteLattice.finiteLimitCone F).cone.π.app x✝ = CategoryTheory.homOfLE ⋯
• CategoryTheory.Limits.CompleteLattice.limitCone_cone_π_app 📋 Mathlib.CategoryTheory.Limits.Lattice
  {α : Type u} [CompleteLattice α] {J : Type w} [CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor J α) (x✝ : J) : (CategoryTheory.Limits.CompleteLattice.limitCone F).cone.π.app x✝ = CategoryTheory.homOfLE ⋯
• AlgebraicGeometry.Scheme.Pullback.openCoverOfBase'_f 📋 Mathlib.AlgebraicGeometry.Pullbacks
  {X Y Z : AlgebraicGeometry.Scheme} (𝒰 : Z.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) (ij : (i : (AlgebraicGeometry.Scheme.Pullback.openCoverOfLeft (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰) f g).I₀) × ((fun i => ((fun i => AlgebraicGeometry.Scheme.coverOfIsIso (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry (CategoryTheory.Limits.pullback.snd f (𝒰.f i)) (CategoryTheory.Limits.pullback.snd g (𝒰.f i))).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.isoLimitCone { cone := ⋯.cone, isLimit := ⋯.isLimit }).inv (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f (𝒰.f i)) (𝒰.f i)) g (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰).f i) f) g (CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.pullback f (𝒰.f i))) (CategoryTheory.CategoryStruct.id Y) (CategoryTheory.CategoryStruct.id Z) ⋯ ⋯)))) i).toPreZeroHypercover) i).I₀) : (AlgebraicGeometry.Scheme.Pullback.openCoverOfBase' 𝒰 f g).f ij = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry (CategoryTheory.Limits.pullback.snd f (𝒰.f ij.fst)) (CategoryTheory.Limits.pullback.snd g (𝒰.f ij.fst))).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.isoLimitCone { cone := ⋯.cone, isLimit := ⋯.isLimit }).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f (𝒰.f ij.fst)) (𝒰.f ij.fst)) g (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f (𝒰.f ij.fst)) f) g (CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.pullback f (𝒰.f ij.fst))) (CategoryTheory.CategoryStruct.id Y) (CategoryTheory.CategoryStruct.id Z) ⋯ ⋯) (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f (𝒰.f ij.fst)) f) g f g (CategoryTheory.Limits.pullback.fst f (𝒰.f ij.fst)) (CategoryTheory.CategoryStruct.id Y) (CategoryTheory.CategoryStruct.id Z) ⋯ ⋯)))
• Condensed.isoFinYoneda_inv_app_hom_apply 📋 Mathlib.Condensed.Discrete.Colimit
  (F : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))) [CategoryTheory.Limits.PreservesFiniteProducts F] (X : FintypeCatᵒᵖ) (a✝ : (CategoryTheory.Limits.Types.productLimitCone fun x => F.obj (Opposite.op (Profinite.of PUnit.{u + 1}))).cone.pt) : (CategoryTheory.ConcreteCategory.hom ((Condensed.isoFinYoneda F).inv.app X)) a✝ = (CategoryTheory.CategoryStruct.id (F.obj (Opposite.op (Condensed.fintypeCatAsCofan (Profinite.of (Opposite.unop X).obj)).pt))).hom' ((((CategoryTheory.Limits.IsLimit.postcomposeHomEquiv (CategoryTheory.Discrete.natIso fun j => CategoryTheory.Iso.refl (F.obj (Opposite.op (Profinite.of PUnit.{u + 1})))) (F.mapCone (CategoryTheory.Limits.Fan.mk (Opposite.op (Condensed.fintypeCatAsCofan (Profinite.of (Opposite.unop X).obj)).pt) fun a => ((Condensed.fintypeCatAsCofan (Profinite.of (Opposite.unop X).obj)).inj a).op))).symm (CategoryTheory.Limits.isLimitOfPreserves F (CategoryTheory.Limits.Cofan.IsColimit.op (Condensed.fintypeCatAsCofanIsColimit (Profinite.of (Opposite.unop X).obj))))).lift (CategoryTheory.Limits.Types.productLimitCone fun x => F.obj (Opposite.op (Profinite.of PUnit.{u + 1}))).cone).hom' a✝)
• LightCondensed.isoFinYoneda_inv_app_hom_apply 📋 Mathlib.Condensed.Discrete.Colimit
  (F : CategoryTheory.Functor LightProfiniteᵒᵖ (Type u)) [CategoryTheory.Limits.PreservesFiniteProducts F] (X : FintypeCatᵒᵖ) (a✝ : (CategoryTheory.Limits.Types.productLimitCone fun x => F.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))).cone.pt) : (CategoryTheory.ConcreteCategory.hom ((LightCondensed.isoFinYoneda F).inv.app X)) a✝ = (CategoryTheory.CategoryStruct.id (F.obj (Opposite.op (LightCondensed.fintypeCatAsCofan (LightProfinite.of (Opposite.unop X).obj)).pt))).hom' ((((CategoryTheory.Limits.IsLimit.postcomposeHomEquiv (CategoryTheory.Discrete.natIso fun j => CategoryTheory.Iso.refl (F.obj (Opposite.op (LightProfinite.of PUnit.{u + 1})))) (F.mapCone (CategoryTheory.Limits.Fan.mk (Opposite.op (LightCondensed.fintypeCatAsCofan (LightProfinite.of (Opposite.unop X).obj)).pt) fun a => ((LightCondensed.fintypeCatAsCofan (LightProfinite.of (Opposite.unop X).obj)).inj a).op))).symm (CategoryTheory.Limits.isLimitOfPreserves F (CategoryTheory.Limits.Cofan.IsColimit.op (LightCondensed.fintypeCatAsCofanIsColimit (LightProfinite.of (Opposite.unop X).obj))))).lift (CategoryTheory.Limits.Types.productLimitCone fun x => F.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))).cone).hom' a✝)

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