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
def CategoryTheory.Cat.asSmallFunctor :
Functor Cat Cat

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

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