AsSmall

📁 Source: Mathlib/CategoryTheory/Category/Cat/AsSmall.lean

Statistics

Metric	Count
Definitions AsSmall, asSmallFunctor	2
Theorems asSmallFunctor_map, asSmallFunctor_obj	2
Total	4

CategoryTheory

Definitions

Name	Category	Theorems
AsSmall 📖	CompOp	27 math math: Cat.asSmallFunctor_obj, Abelian.FreydMitchell.instNonemptyAsSmall, down_comp_assoc, AsSmall.hasFiniteLimits, Grothendieck.compAsSmallFunctorEquivalenceFunctor_map_fiber, instIsCofilteredAsSmall, AsSmall.down_obj, AsSmall.instAdditiveDown, AsSmall.equiv_unitIso, AsSmall.equiv_counitIso, Grothendieck.compAsSmallFunctorEquivalenceFunctor_obj_fiber, Grothendieck.compAsSmallFunctorEquivalenceInverse_obj_fiber, AsSmall.equiv_inverse, AsSmall.up_obj_down, AsSmall.equiv_functor, instIsFilteredAsSmall, AsSmall.up_map_down, Grothendieck.compAsSmallFunctorEquivalenceFunctor_map_base, eqToHom_down, Grothendieck.compAsSmallFunctorEquivalenceInverse_map_fiber, IsSifted.isSifted_iff_asSmallIsSifted, Cat.asSmallFunctor_map, AsSmall.instAdditiveUp, Grothendieck.compAsSmallFunctorEquivalenceInverse_map_base, AsSmall.hasLimitsOfShape, AsSmall.down_map, down_comp

CategoryTheory.Cat

Definitions

Name	Category	Theorems
asSmallFunctor 📖	CompOp	14 math math: asSmallFunctor_obj, CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceFunctor_map_fiber, CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceFunctor_obj_fiber, CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceInverse_obj_fiber, CategoryTheory.Grothendieck.compAsSmallFunctorEquivalence_functor, CategoryTheory.Grothendieck.compAsSmallFunctorEquivalence_inverse, CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceFunctor_obj_base, CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceFunctor_map_base, CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceInverse_obj_base, CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceInverse_map_fiber, CategoryTheory.Grothendieck.compAsSmallFunctorEquivalence_unitIso, asSmallFunctor_map, CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceInverse_map_base, CategoryTheory.Grothendieck.compAsSmallFunctorEquivalence_counitIso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
asSmallFunctor_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Cat category asSmallFunctor CategoryTheory.Functor.toCatHom CategoryTheory.AsSmall CategoryTheory.Bundled.α CategoryTheory.Category str CategoryTheory.instSmallCategoryAsSmall CategoryTheory.Functor.comp CategoryTheory.AsSmall.down Hom.toFunctor CategoryTheory.AsSmall.up	—	—
asSmallFunctor_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Cat category asSmallFunctor of CategoryTheory.AsSmall CategoryTheory.Bundled.α CategoryTheory.Category str CategoryTheory.instSmallCategoryAsSmall	—	—

---

← Back to Index