Theorems · Inductive type · category theory
CategoryTheory.Limits.HasFiniteColimits
(C : Type u) → [CategoryTheory.Category.{v, u} C] → PropA category has all finite colimits if every functor J ⥤ C with a FinCategory J
instance and J : Type has a colimit.
This is often called 'finitely cocomplete'.
- Cited by
- 34 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
- Assumes
- CategoryTheory.Category
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Categorystatement · cited by 32,673
Cited by49
Results whose statement or proof uses this declaration.
- CategoryTheory.CostructuredArrow.projectQuotientstatement and proof · cited by 4
- CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.isoAuxstatement and proof · cited by 2
- CategoryTheory.Limits.preservesFiniteLimits_of_isFiltered_costructuredArrow_yonedastatement and proof · cited by 2
- CategoryTheory.Limits.isFiltered_costructuredArrow_yoneda_of_preservesFiniteLimitsstatement and proof · cited by 2
- CategoryTheory.hasExactLimitsOfShape_discrete_of_hasExactLimitsOfShape_finset_discrete_opstatement and proof · cited by 2
- CategoryTheory.hasExactLimitsOfShape_of_initialstatement and proof · cited by 2
- CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.isostatement and proof · cited by 1
- CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.isoAux_hom_appstatement and proof · cited by 1
- CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.iso_homstatement and proof · cited by 1
- CategoryTheory.CountableAB4Star.of_hasExactLimitsOfShape_nat_and_finitestatement and proof · cited by 1
- CategoryTheory.Limits.hasFiniteColimits_of_hasCoequalizers_and_finite_coproductsstatement · cited by 1
- CategoryTheory.Limits.hasFiniteColimits_of_hasInitial_and_pushoutsstatement · cited by 1