Theorems · Definition · category theory
TopCat.limitCone
{J : Type v} →
[inst : CategoryTheory.Category.{w, v} J] → (F : CategoryTheory.Functor J TopCat) → CategoryTheory.Limits.Cone FA choice of limit cone for a functor F : J ⥤ TopCat.
Generally you should just use limit.cone F, unless you need the actual definition
(which is in terms of Types.limitCone).
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 73 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CategoryTheory.Category
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites13
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- CategoryTheory.Categorystatement and proof · cited by 32,673
- Quiver.Homproof · cited by 32,603
- CategoryTheory.Functor.objproof · cited by 19,642
- CategoryTheory.Functorstatement and proof · cited by 16,252
- CategoryTheory.Functor.mapproof · cited by 8,698
- Set.Elemproof · cited by 7,166
- Set.ofPredproof · cited by 6,101
- CategoryTheory.ConcreteCategory.homproof · cited by 4,022
- TopCat.carrierproof · cited by 3,184
- TopCatstatement and proof · cited by 1,889
- CategoryTheory.Limits.Conestatement · cited by 710
Cited by5
Results whose statement or proof uses this declaration.
- TopCat.nonempty_limitCone_of_compact_t2_cofiltered_systemstatement · cited by 2
- Profinite.exists_locallyConstantproof · cited by 2
- nonempty_sections_of_finite_cofiltered_system.initproof · cited by 1
- TopCat.limitConeIsLimitstatement and proof · cited by 1
- CompHaus.limitConeproof · cited by 0