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

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

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem CategoryTheory.Cat.asSmallFunctor_map {X✝ Y✝ : CategoryTheory.Cat} (F : X✝ ⟶ Y✝) :
    CategoryTheory.Cat.asSmallFunctor.map F = CategoryTheory.AsSmall.down.comp (CategoryTheory.Functor.comp F CategoryTheory.AsSmall.up)
    source
    @[simp]
    theorem CategoryTheory.Cat.asSmallFunctor_obj (C : CategoryTheory.Cat) :
    CategoryTheory.Cat.asSmallFunctor.obj C = CategoryTheory.Cat.of (CategoryTheory.AsSmall ↑C)