Theorems · Definition · category theory
CategoryTheory.Limits.limit.cone
{J : Type u₁} →
[inst : CategoryTheory.Category.{v₁, u₁} J] →
{C : Type u} →
[inst_1 : CategoryTheory.Category.{v, u} C] →
(F : CategoryTheory.Functor J C) → [CategoryTheory.Limits.HasLimit F] → CategoryTheory.Limits.Cone FAn arbitrary choice of limit cone for a functor.
- Defined in
- Mathlib.CategoryTheory.Limits.HasLimits
- Cited by
- 97 results in Mathlib
- Foundations
- Depth 5 from the axioms, rests on 9 definitions · uses Classical.choice
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Categorystatement and proof · cited by 32,673
- CategoryTheory.Functorstatement and proof · cited by 16,252
- CategoryTheory.Limits.Conestatement · cited by 710
- CategoryTheory.Limits.HasLimitstatement and proof · cited by 226
- CategoryTheory.Limits.LimitCone.coneproof · cited by 72
- CategoryTheory.Limits.getLimitConeproof · cited by 3
Cited by144
Results whose statement or proof uses this declaration.
- CategoryTheory.Limits.limitproof · cited by 346
- CategoryTheory.Limits.limit.πproof · cited by 278
- CategoryTheory.Limits.limit.isLimitstatement · cited by 146
- CategoryTheory.Limits.pullback.conditionproof · cited by 122
- CategoryTheory.Limits.pullback.hom_extproof · cited by 63
- CategoryTheory.Limits.kernel.conditionproof · cited by 52
- CategoryTheory.Limits.limMapproof · cited by 29
- CategoryTheory.Limits.kernelIsKernelproof · cited by 24
- CategoryTheory.Limits.pullback.coneproof · cited by 18
- CategoryTheory.Limits.hasLimit_of_isoproof · cited by 16
- CategoryTheory.Limits.equalizer.conditionproof · cited by 16
- CategoryTheory.Limits.limit.wproof · cited by 15