Documentation

Mathlib.CategoryTheory.Limits.FinallySmall

Finally small categories #

A category given by (J : Type u) [Category.{v} J] is w-finally small if there exists a FinalModel J : Type w equipped with [SmallCategory (FinalModel J)] and a final functor FinalModel J ⥤ J.

This means that if a category C has colimits of size w and J is w-finally small, then C has colimits of shape J. In this way, the notion of "finally small" can be seen of a generalization of the notion of "essentially small" for indexing categories of colimits.

Dually, we have a notion of initially small category.

We show that a finally small category admits a small weakly terminal set, i.e., a small set s of objects such that from every object there a morphism to a member of s. We also show that the converse holds if J is filtered.

A category is FinallySmall.{w} if there is a final functor from a w-small category.

Instances

    There is a final functor from a small category.

    Constructor for FinallySmall C from an explicit small category witness.

    An arbitrarily chosen small model for a finally small category.

    Equations
    Instances For

      A category is InitiallySmall.{w} if there is an initial functor from a w-small category.

      Instances

        There is an initial functor from a small category.

        Constructor for InitialSmall C from an explicit small category witness.

        An arbitrarily chosen small model for an initially small category.

        Equations
        Instances For

          The converse is true if J is filtered, see finallySmall_of_small_weakly_terminal_set.

          The converse is true if J is cofiltered, see intiallySmall_of_small_weakly_initial_set.