Theorems · Definition · category theory
CategoryTheory.SmallCategory
Type u → Type (u + 1)
A SmallCategory has objects and morphisms in the same universe level.
- Defined in
- Mathlib.CategoryTheory.Category.Basic
- Cited by
- 480 results in Mathlib
- Foundations
- Depth 1 from the axioms, rests on 2 definitions · uses no axioms
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.Categoryproof · cited by 32,673
Cited by864
Results whose statement or proof uses this declaration.
- CategoryTheory.FinCategorystatement · cited by 107
- CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagramstatement · cited by 37
- CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.DiagramWithUniqueTerminalstatement · cited by 29
- CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.Pstatement and proof · cited by 28
- CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.Wstatement and proof · cited by 26
- ProfiniteGrp.limitstatement and proof · cited by 23
- CommRingCat.Colimits.Prequotientstatement · cited by 22
- RingCat.Colimits.Prequotientstatement · cited by 22
- CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.IsTerminalstatement · cited by 20
- ProfiniteGrp.limitConePtAuxstatement and proof · cited by 19
- CategoryTheory.isFiltered_of_isCardinalFilteredproof · cited by 18
- CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.DiagramWithUniqueTerminal.toDiagramstatement and proof · cited by 15
Showing the 200 most cited of 864.