Theorems · Definition · category theory
CategoryTheory.Limits.colim
{J : Type u₁} →
[inst : CategoryTheory.Category.{v₁, u₁} J] →
{C : Type u} →
[inst_1 : CategoryTheory.Category.{v, u} C] →
[CategoryTheory.Limits.HasColimitsOfShape J C] → CategoryTheory.Functor (CategoryTheory.Functor J C) Ccolimit F is functorial in F, when C has all colimits of shape J.
- Defined in
- Mathlib.CategoryTheory.Limits.HasLimits
- Cited by
- 89 results in Mathlib
- Foundations
- Depth 35 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
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
- Quiver.Homproof · cited by 32,603
- CategoryTheory.Functorstatement and proof · cited by 16,252
- CategoryTheory.Limits.colimitproof · cited by 453
- CategoryTheory.Limits.HasColimitsOfShapestatement and proof · cited by 308
- CategoryTheory.Limits.colimMapproof · cited by 69
Cited by134
Results whose statement or proof uses this declaration.
- CategoryTheory.GrothendieckTopology.Point.presheafFiberproof · cited by 89
- TopCat.Presheaf.stalkFunctorproof · cited by 37
- TopCat.Presheaf.stalkPushforwardproof · cited by 12
- CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.fiberproof · cited by 9
- CategoryTheory.Limits.fiberwiseColimproof · cited by 9
- CategoryTheory.Limits.Sigma.mapIsoproof · cited by 8
- CategoryTheory.Limits.colimitLimitIsostatement and proof · cited by 7
- CategoryTheory.Limits.colimit.ι_mapstatement · cited by 6
- CategoryTheory.preservesColimitNatIsostatement · cited by 6
- CategoryTheory.Limits.colimitIsoColimitCurryCompColimstatement and proof · cited by 6
- CategoryTheory.Limits.colimitLimitToLimitColimitstatement and proof · cited by 6
- CategoryTheory.Limits.colimitUncurryIsoColimitCompColimstatement and proof · cited by 6