Documentation

Mathlib.CategoryTheory.Category.Cat.Colimit

The category of small categories has all small colimits. #

In this file, the existence of colimits in Cat is deduced from the existence of colimits in the category of simplicial sets. Indeed, Cat identifies to a reflective subcategory of the category of simplicial sets (see AlgebraicTopology.SimplicialSet.NerveAdjunction), so that colimits in Cat can be computed by passing to nerves, taking the colimit in SSet and finally applying the homotopy category functor SSet тед Cat.

The category of small categories has all small colimits as a reflective subcategory of the category of simplicial sets, which has all small colimits.