Theorems · Definition · category theory
CategoryTheory.Limits.HasCoproducts
(C : Type u) → [CategoryTheory.Category.{v, u} C] → PropAn abbreviation for Π J, HasColimitsOfShape (Discrete J) C
- Cited by
- 119 results in Mathlib
- Foundations
- Depth 11 from the axioms, rests on 60 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 by183
Results whose statement or proof uses this declaration.
- SSet.chainComplexstatement and proof · cited by 46
- SSet.normalizedChainComplexstatement and proof · cited by 29
- SSet.toNormalizedChainComplexstatement and proof · cited by 20
- SSet.ιChainComplexstatement and proof · cited by 20
- CategoryTheory.Limits.sigmaConststatement and proof · cited by 18
- SSet.homologystatement and proof · cited by 13
- SSet.fromNormalizedChainComplexstatement and proof · cited by 12
- SSet.ιNormalizedChainComplexstatement and proof · cited by 11
- CategoryTheory.Presheaf.freeYonedastatement and proof · cited by 11
- SSet.homologyMapstatement and proof · cited by 9
- SSet.chainComplexMapstatement and proof · cited by 8
- SSet.homologyData₀statement and proof · cited by 8