Theorems · Definition · category theory
CategoryTheory.Limits.HasPullbacks
(C : Type u) → [CategoryTheory.Category.{v, u} C] → PropA category HasPullbacks if it has all limits of shape WalkingCospan, i.e. if it has a
pullback for every pair of morphisms with the same codomain.
- Cited by
- 439 results in Mathlib
- Foundations
- Depth 14 from the axioms, rests on 79 definitions · uses no axioms
- Assumes
- CategoryTheory.Category
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
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.Limits.WalkingCospanproof · cited by 496
- CategoryTheory.Limits.HasLimitsOfShapeproof · cited by 223
Cited by562
Results whose statement or proof uses this declaration.
- CategoryTheory.Over.cartesianMonoidalCategorystatement and proof · cited by 68
- CategoryTheory.Subobject.pullbackstatement and proof · cited by 54
- CategoryTheory.Dial.Hom.fstatement and proof · cited by 35
- CategoryTheory.Dial.tensorObjImplstatement and proof · cited by 35
- CategoryTheory.Pretopology.toPrecoveragestatement and proof · cited by 34
- CategoryTheory.Dial.Hom.Fstatement and proof · cited by 34
- CategoryTheory.Pretopologystatement · cited by 32
- CategoryTheory.SubobjectRepresentableBystatement and proof · cited by 19
- CategoryTheory.Pretopology.toGrothendieckstatement and proof · cited by 18
- CategoryTheory.PreOneHypercover.cylinderstatement and proof · cited by 17
- CategoryTheory.Over.braidedCategorystatement and proof · cited by 16
- CategoryTheory.Limits.pullbackDiagonalMapIdIsostatement and proof · cited by 16
Showing the 200 most cited of 562.