Theorems · Definition · category theory
CategoryTheory.Limits.HasInitial
(C : Type u₁) → [CategoryTheory.Category.{v₁, u₁} C] → PropA category has an initial object if it has a colimit over the empty diagram.
Use hasInitial_of_unique to construct instances.
- Cited by
- 185 results in Mathlib
- Foundations
- Depth 11 from the axioms, rests on 61 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.Discreteproof · cited by 2,447
- CategoryTheory.Limits.HasColimitsOfShapeproof · cited by 308
Cited by256
Results whose statement or proof uses this declaration.
- CategoryTheory.Limits.initialstatement and proof · cited by 84
- CategoryTheory.Limits.initial.tostatement and proof · cited by 63
- HomotopicalAlgebra.IsCofibrantstatement and proof · cited by 56
- CategoryTheory.Functor.HasLeftKanExtensionproof · cited by 42
- HomotopicalAlgebra.BifibrantObjectstatement and proof · cited by 38
- HomotopicalAlgebra.bifibrantObjectsstatement and proof · cited by 37
- HomotopicalAlgebra.CofibrantObjectstatement and proof · cited by 35
- CategoryTheory.Limits.initialIsInitialstatement and proof · cited by 35
- HomotopicalAlgebra.cofibrantObjectsstatement and proof · cited by 34
- CategoryTheory.GradedObject.single₀statement and proof · cited by 30
- CategoryTheory.GradedObject.singlestatement and proof · cited by 22
- CategoryTheory.GradedObject.singleObjApplyIsostatement and proof · cited by 19
Showing the 200 most cited of 256.