Theorems · Definition · category theory
CategoryTheory.FunctorToTypes.Small
{C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Functor C (Type w') → PropA functor to types F : C ⥤ Type w' is w-small if for any X : C,
the type F.obj X is w-small.
- Defined in
- Mathlib.CategoryTheory.ShrinkYoneda
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 11 from the axioms · uses no axioms
- Assumes
- CategoryTheory.Category
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
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.Functor.objproof · cited by 19,642
- CategoryTheory.Functorstatement and proof · cited by 16,252
- Smallproof · cited by 369
Cited by10
Results whose statement or proof uses this declaration.
- CategoryTheory.FunctorToTypes.shrinkstatement and proof · cited by 9
- CategoryTheory.FunctorToTypes.shrinkMapstatement and proof · cited by 3
- CategoryTheory.FunctorToTypes.shrinkCompUliftFunctorIsostatement and proof · cited by 2
- CategoryTheory.Precoverage.small_subsheafify_of_smallstatement · cited by 1
- CategoryTheory.FunctorToTypes.shrink.congr_simpstatement and proof · cited by 0
- CategoryTheory.FunctorToTypes.shrinkCompUliftFunctorIso_hom_appstatement and proof · cited by 0
- CategoryTheory.FunctorToTypes.shrinkCompUliftFunctorIso_inv_appstatement and proof · cited by 0
- CategoryTheory.FunctorToTypes.shrinkMap_appstatement and proof · cited by 0
- CategoryTheory.FunctorToTypes.shrink_mapstatement and proof · cited by 0
- CategoryTheory.FunctorToTypes.shrink_objstatement and proof · cited by 0