Loogle!

Result

Found 44 declarations mentioning CategoryTheory.Limits.limit.cone.

CategoryTheory.Limits.limit.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) [CategoryTheory.Limits.HasLimit F] : CategoryTheory.Limits.Cone F
CategoryTheory.Limits.limit.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) [CategoryTheory.Limits.HasLimit F] : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.limit.cone F)
CategoryTheory.Limits.limit.cone_x 📋 Mathlib.CategoryTheory.Limits.HasLimits
{J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor J C} [CategoryTheory.Limits.HasLimit F] : (CategoryTheory.Limits.limit.cone F).pt = CategoryTheory.Limits.limit F
CategoryTheory.Limits.limit.coneMorphism 📋 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] (c : CategoryTheory.Limits.Cone F) : c ⟶ CategoryTheory.Limits.limit.cone F
CategoryTheory.Limits.limit.lift_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} [CategoryTheory.Limits.HasLimit F] : CategoryTheory.Limits.limit.lift F (CategoryTheory.Limits.limit.cone F) = CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.limit F)
CategoryTheory.Limits.limit.isLimit_lift 📋 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] (c : CategoryTheory.Limits.Cone F) : (CategoryTheory.Limits.limit.isLimit F).lift c = CategoryTheory.Limits.limit.lift F c
CategoryTheory.Limits.limit.coneMorphism_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] (c : CategoryTheory.Limits.Cone F) : (CategoryTheory.Limits.limit.coneMorphism c).hom = CategoryTheory.Limits.limit.lift F c
CategoryTheory.Limits.limit.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} [CategoryTheory.Limits.HasLimit F] : (CategoryTheory.Limits.limit.cone F).π.app = CategoryTheory.Limits.limit.π F
CategoryTheory.Limits.limit.coneMorphism_π 📋 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] (c : CategoryTheory.Limits.Cone F) (j : J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.coneMorphism c).hom (CategoryTheory.Limits.limit.π F j) = c.π.app j
CategoryTheory.Limits.limit.conePointUniqueUpToIso_hom_comp 📋 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] {c : CategoryTheory.Limits.Cone F} (hc : CategoryTheory.Limits.IsLimit c) (j : J) : CategoryTheory.CategoryStruct.comp (hc.conePointUniqueUpToIso (CategoryTheory.Limits.limit.isLimit F)).hom (CategoryTheory.Limits.limit.π F j) = c.π.app j
CategoryTheory.Limits.limit.conePointUniqueUpToIso_inv_comp 📋 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] {c : CategoryTheory.Limits.Cone F} (hc : CategoryTheory.Limits.IsLimit c) (j : J) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.limit.isLimit F).conePointUniqueUpToIso hc).inv (CategoryTheory.Limits.limit.π F j) = c.π.app j
CategoryTheory.Limits.limit.conePointUniqueUpToIso_hom_comp_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] {c : CategoryTheory.Limits.Cone F} (hc : CategoryTheory.Limits.IsLimit c) (j : J) {Z : C} (h : F.obj j ⟶ Z) : CategoryTheory.CategoryStruct.comp (hc.conePointUniqueUpToIso (CategoryTheory.Limits.limit.isLimit F)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π F j) h) = CategoryTheory.CategoryStruct.comp (c.π.app j) h
CategoryTheory.Limits.limit.conePointUniqueUpToIso_inv_comp_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] {c : CategoryTheory.Limits.Cone F} (hc : CategoryTheory.Limits.IsLimit c) (j : J) {Z : C} (h : F.obj j ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.limit.isLimit F).conePointUniqueUpToIso hc).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π F j) h) = CategoryTheory.CategoryStruct.comp (c.π.app j) h
CategoryTheory.Limits.limit.homIso_hom 📋 Mathlib.CategoryTheory.Limits.HasLimits
{J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor J C) [CategoryTheory.Limits.HasLimit F] {W : C} : (CategoryTheory.Limits.limit.homIso F W).hom = TypeCat.ofHom fun f => CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.const J).map f.down) (CategoryTheory.Limits.limit.cone F).π
CategoryTheory.Limits.PullbackCone.fst_limit_cone 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.cospan f g)] : CategoryTheory.Limits.PullbackCone.fst (CategoryTheory.Limits.limit.cone (CategoryTheory.Limits.cospan f g)) = CategoryTheory.Limits.pullback.fst f g
CategoryTheory.Limits.PullbackCone.snd_limit_cone 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.cospan f g)] : CategoryTheory.Limits.PullbackCone.snd (CategoryTheory.Limits.limit.cone (CategoryTheory.Limits.cospan f g)) = CategoryTheory.Limits.pullback.snd f g
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.createsLimitOfFullyFaithfulOfLift 📋 Mathlib.CategoryTheory.Limits.Creates
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [CategoryTheory.Category.{w', w} J] {K : CategoryTheory.Functor J C} {F : CategoryTheory.Functor C D} [F.Full] [F.Faithful] [CategoryTheory.Limits.HasLimit (K.comp F)] (c : CategoryTheory.Limits.Cone K) (i : F.mapCone c ≅ CategoryTheory.Limits.limit.cone (K.comp F)) : CategoryTheory.CreatesLimit K F
CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_functor_obj_pt 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (K : CategoryTheory.Limits.Multifork I) : (I.multiforkEquivPiFork.functor.obj K).pt = K.pt
CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_inverse_obj_pt 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (a : CategoryTheory.Limits.Fork (I.fstPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right))) (I.sndPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right)))) : (I.multiforkEquivPiFork.inverse.obj a).pt = a.pt
CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_functor_map_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] {K₁ K₂ : CategoryTheory.Limits.Multifork I} (f : K₁ ⟶ K₂) : (I.multiforkEquivPiFork.functor.map f).hom = f.hom
CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_functor_obj_π_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (K : CategoryTheory.Limits.Multifork I) (X : CategoryTheory.Limits.WalkingParallelPair) : (I.multiforkEquivPiFork.functor.obj K).π.app X = CategoryTheory.Limits.WalkingParallelPair.rec (motive := fun t => X = t → (K.pt ⟶ (CategoryTheory.Limits.parallelPair (I.fstPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right))) (I.sndPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right)))).obj X)) (fun h => ⋯ ▸ CategoryTheory.Limits.Fan.IsLimit.lift (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.left)) K.ι) (fun h => ⋯ ▸ CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fan.IsLimit.lift (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.left)) K.ι) (I.sndPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right)))) X ⋯
CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_inverse_obj_π_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (a : CategoryTheory.Limits.Fork (I.fstPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right))) (I.sndPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right)))) (x✝ : CategoryTheory.Limits.WalkingMulticospan J) : (I.multiforkEquivPiFork.inverse.obj a).π.app x✝ = match x✝ with | CategoryTheory.Limits.WalkingMulticospan.left a_1 => CategoryTheory.CategoryStruct.comp a.ι (CategoryTheory.Limits.Fan.proj (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) a_1) | CategoryTheory.Limits.WalkingMulticospan.right a_1 => CategoryTheory.CategoryStruct.comp a.ι (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fan.proj (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (J.fst a_1)) (I.fst a_1))
CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_inverse_map_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] {K₁ K₂ : CategoryTheory.Limits.Fork (I.fstPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right))) (I.sndPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right)))} (f : K₁ ⟶ K₂) : (I.multiforkEquivPiFork.inverse.map f).hom = f.hom
CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_unitIso_hom_app_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (X : CategoryTheory.Limits.Multifork I) : (I.multiforkEquivPiFork.unitIso.hom.app X).hom = CategoryTheory.CategoryStruct.id X.pt
CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_unitIso_inv_app_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (X : CategoryTheory.Limits.Multifork I) : (I.multiforkEquivPiFork.unitIso.inv.app X).hom = CategoryTheory.CategoryStruct.id X.pt
CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_counitIso_hom_app_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (X : CategoryTheory.Limits.Fork (I.fstPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right))) (I.sndPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right)))) : (I.multiforkEquivPiFork.counitIso.hom.app X).hom = CategoryTheory.CategoryStruct.id X.pt
CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_counitIso_inv_app_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (X : CategoryTheory.Limits.Fork (I.fstPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right))) (I.sndPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right)))) : (I.multiforkEquivPiFork.counitIso.inv.app X).hom = CategoryTheory.CategoryStruct.id X.pt
CategoryTheory.Limits.DiagramOfCones.mkOfHasLimits_obj 📋 Mathlib.CategoryTheory.Limits.Fubini
{J : Type u_1} {K : Type u_2} [CategoryTheory.Category.{v_1, u_1} J] [CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [CategoryTheory.Category.{v_3, u_3} C] (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) [CategoryTheory.Limits.HasLimitsOfShape K C] (j : J) : (CategoryTheory.Limits.DiagramOfCones.mkOfHasLimits F).obj j = CategoryTheory.Limits.limit.cone (F.obj j)
CategoryTheory.Limits.DiagramOfCones.mkOfHasLimits_map_hom 📋 Mathlib.CategoryTheory.Limits.Fubini
{J : Type u_1} {K : Type u_2} [CategoryTheory.Category.{v_1, u_1} J] [CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [CategoryTheory.Category.{v_3, u_3} C] (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) [CategoryTheory.Limits.HasLimitsOfShape K C] {j✝ j'✝ : J} (f : j✝ ⟶ j'✝) : ((CategoryTheory.Limits.DiagramOfCones.mkOfHasLimits F).map f).hom = CategoryTheory.Limits.lim.map (F.map f)
CategoryTheory.Limits.colimitLimitToLimitColimitCone 📋 Mathlib.CategoryTheory.Limits.ColimitLimit
{J : Type u₁} {K : Type u₂} [CategoryTheory.Category.{v₁, u₁} J] [CategoryTheory.Category.{v₂, u₂} K] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimitsOfShape J C] [CategoryTheory.Limits.HasColimitsOfShape K C] (G : CategoryTheory.Functor J (CategoryTheory.Functor K C)) [CategoryTheory.Limits.HasLimit G] : CategoryTheory.Limits.colim.mapCone (CategoryTheory.Limits.limit.cone G) ⟶ CategoryTheory.Limits.limit.cone (G.comp CategoryTheory.Limits.colim)
CategoryTheory.Limits.colimitLimitToLimitColimitCone_hom 📋 Mathlib.CategoryTheory.Limits.ColimitLimit
{J : Type u₁} {K : Type u₂} [CategoryTheory.Category.{v₁, u₁} J] [CategoryTheory.Category.{v₂, u₂} K] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimitsOfShape J C] [CategoryTheory.Limits.HasColimitsOfShape K C] (G : CategoryTheory.Functor J (CategoryTheory.Functor K C)) [CategoryTheory.Limits.HasLimit G] : (CategoryTheory.Limits.colimitLimitToLimitColimitCone G).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colim.map (CategoryTheory.Limits.limitIsoSwapCompLim G).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitLimitToLimitColimit (CategoryTheory.Functor.uncurry.obj G)) (CategoryTheory.Limits.lim.map (CategoryTheory.Functor.whiskerRight (CategoryTheory.Functor.currying.unitIso.app G).inv CategoryTheory.Limits.colim)))
CategoryTheory.Limits.colimitLimitToLimitColimitCone_iso 📋 Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit
{J : Type u₁} {K : Type u₂} [CategoryTheory.SmallCategory J] [CategoryTheory.Category.{v₂, u₂} K] [Small.{v, u₂} K] [CategoryTheory.FinCategory J] [CategoryTheory.IsFiltered K] (F : CategoryTheory.Functor J (CategoryTheory.Functor K (Type v))) : CategoryTheory.IsIso (CategoryTheory.Limits.colimitLimitToLimitColimitCone F)
CategoryTheory.CategoryOfElements.CreatesLimitsAux.isValidLift 📋 Mathlib.CategoryTheory.Limits.Elements
{C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor C (Type w)} {I : Type u₁} [CategoryTheory.Category.{v₁, u₁} I] [Small.{w, u₁} I] (F : CategoryTheory.Functor I A.Elements) [CategoryTheory.Limits.HasLimitsOfShape I C] [CategoryTheory.Limits.PreservesLimitsOfShape I A] : (CategoryTheory.CategoryOfElements.π A).mapCone (CategoryTheory.CategoryOfElements.CreatesLimitsAux.liftedCone F) ≅ CategoryTheory.Limits.limit.cone (F.comp (CategoryTheory.CategoryOfElements.π A))
CategoryTheory.LiftRightAdjoint.constructRightAdjointEquiv_apply 📋 Mathlib.CategoryTheory.Adjunction.Lifting.Right
{A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {U : CategoryTheory.Functor A B} {F : CategoryTheory.Functor B A} (L : CategoryTheory.Functor C B) (U' : CategoryTheory.Functor A C) (adj₁ : F ⊣ U) (adj₂ : L.comp F ⊣ U') [CategoryTheory.Limits.HasCoreflexiveEqualizers C] (h : (X : B) → CategoryTheory.RegularMono (adj₁.unit.app X)) (Y : C) (X : B) (a✝ : Y ⟶ CategoryTheory.LiftRightAdjoint.constructRightAdjointObj L U' adj₁ adj₂ X) : (CategoryTheory.LiftRightAdjoint.constructRightAdjointEquiv L U' adj₁ adj₂ h Y X) a✝ = (CategoryTheory.Limits.Fork.IsLimit.homIso (CategoryTheory.LiftRightAdjoint.unitEqualises adj₁ h X) (L.obj Y)).symm ⟨(adj₁.homEquiv (L.obj Y) (F.obj X)) ((adj₂.homEquiv Y (F.obj X)).symm ↑((CategoryTheory.Limits.Fork.IsLimit.homIso (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Limits.parallelPair (U'.map (F.map (adj₁.unit.app X))) (CategoryTheory.LiftRightAdjoint.otherMap L U' adj₁ adj₂ X))) Y) a✝)), ⋯⟩
CategoryTheory.LiftRightAdjoint.constructRightAdjointEquiv_symm_apply 📋 Mathlib.CategoryTheory.Adjunction.Lifting.Right
{A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {U : CategoryTheory.Functor A B} {F : CategoryTheory.Functor B A} (L : CategoryTheory.Functor C B) (U' : CategoryTheory.Functor A C) (adj₁ : F ⊣ U) (adj₂ : L.comp F ⊣ U') [CategoryTheory.Limits.HasCoreflexiveEqualizers C] (h : (X : B) → CategoryTheory.RegularMono (adj₁.unit.app X)) (Y : C) (X : B) (a✝ : L.obj Y ⟶ X) : (CategoryTheory.LiftRightAdjoint.constructRightAdjointEquiv L U' adj₁ adj₂ h Y X).symm a✝ = (CategoryTheory.Limits.Fork.IsLimit.homIso (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Limits.parallelPair (U'.map (F.map (adj₁.unit.app X))) (CategoryTheory.LiftRightAdjoint.otherMap L U' adj₁ adj₂ X))) Y).symm ⟨(adj₂.homEquiv Y (F.obj X)) ((adj₁.homEquiv (L.obj Y) (F.obj X)).symm ↑((CategoryTheory.Limits.Fork.IsLimit.homIso (CategoryTheory.LiftRightAdjoint.unitEqualises adj₁ h X) (L.obj Y)) a✝)), ⋯⟩
CategoryTheory.Localization.HasProductsOfShapeAux.isLimitMapCone 📋 Mathlib.CategoryTheory.Localization.FiniteProducts
{C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W] (J : Type) [CategoryTheory.Limits.HasProductsOfShape J C] [W.IsStableUnderProductsOfShape J] [W.ContainsIdentities] [Finite J] (F : CategoryTheory.Functor (CategoryTheory.Discrete J) C) : CategoryTheory.Limits.IsLimit (L.mapCone (CategoryTheory.Limits.limit.cone F))

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:

By constant:
🔍 Real.sin
finds all lemmas whose statement somehow mentions the sine function.
By lemma name substring:
🔍 "differ"
finds all lemmas that have "differ" somewhere in their lemma name.
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
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.
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