Theorems · Definition · category theory
CategoryTheory.Limits.colimit
{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.HasColimit F] → CAn arbitrary choice of colimit object of a functor.
- Defined in
- Mathlib.CategoryTheory.Limits.HasLimits
- Cited by
- 453 results in Mathlib
- Foundations
- Depth 6 from the axioms, rests on 11 definitions · uses Classical.choice
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
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.Cocone.ptproof · cited by 1,354
- CategoryTheory.Limits.HasColimitstatement and proof · cited by 307
- CategoryTheory.Limits.colimit.coconeproof · cited by 136
Cited by573
Results whose statement or proof uses this declaration.
- CategoryTheory.Limits.colimit.ιstatement · cited by 397
- CategoryTheory.Limits.sigmaObjproof · cited by 302
- CategoryTheory.Limits.pushoutproof · cited by 284
- CategoryTheory.Limits.coprodproof · cited by 252
- CategoryTheory.Limits.colimit.ι_descstatement · cited by 170
- CategoryTheory.Limits.colimproof · cited by 89
- CategoryTheory.Limits.initialproof · cited by 84
- CategoryTheory.Limits.coequalizerproof · cited by 79
- CategoryTheory.Limits.colimMapstatement · cited by 69
- CategoryTheory.Limits.colimit.descstatement · cited by 63
- CategoryTheory.GrothendieckTopology.plusObjproof · cited by 56
- CategoryTheory.Limits.HasColimit.isoOfNatIsostatement · cited by 56
Showing the 200 most cited of 573.