Documentation

Mathlib.CategoryTheory.Category.Cat.AsSmall

Functorially embedding Cat into the category of small categories #

There is a canonical functor asSmallFunctor between the category of categories of any size and any larger category of small categories.

Future Work #

Show that asSmallFunctor is faithful.

source
🔸 coverage
def CategoryTheory.Cat.asSmallFunctor :
Functor Cat Cat

Assigning to each category C the small category AsSmall C induces a functor Cat ⥤ Cat.

Instances For
    source
    📐 coverage
    @[simp]
    theorem CategoryTheory.Cat.asSmallFunctor_map {X✝ Y✝ : Cat} (F : X✝ ⟶ Y✝) :
    asSmallFunctor.map F = (AsSmall.down.comp (F.toFunctor.comp AsSmall.up)).toCatHom
    source
    📐 coverage
    @[simp]
    theorem CategoryTheory.Cat.asSmallFunctor_obj (C : Cat) :
    asSmallFunctor.obj C = of (AsSmall ↑C)