Documentation

Mathlib.CategoryTheory.EssentiallySmall

Essentially small categories. #

A category given by (C : Type u) [Category.{v} C] is w-essentially small if there exists a SmallModel C : Type w equipped with [SmallCategory (SmallModel C)] and an equivalence C ≌ SmallModel C.

A category is w-locally small if every hom type is w-small.

The main theorem here is that a category is w-essentially small iff the type Skeleton C is w-small, and C is w-locally small.

  • equiv_smallCategory : S x, Nonempty (C S)

    An essentially small category is equivalent to some small category.

A category is EssentiallySmall.{w} if there exists an equivalence to some S : Type w with [SmallCategory S].

Instances

    Constructor for EssentiallySmall C from an explicit small category witness.

    An arbitrarily chosen small model for an essentially small category.

    Instances For

      The (noncomputable) categorical equivalence between an essentially small category and its small model.

      Instances For
        • hom_small : ∀ (X Y : C), Small.{w, v} (X Y)

          A locally small category has small hom-types.

        A category is w-locally small if every hom set is w-small.

        See ShrinkHoms C for a category instance where every hom set has been replaced by a small model.

        Instances

          We define a type alias ShrinkHoms C for C. When we have LocallySmall.{w} C, we'll put a Category.{w} instance on ShrinkHoms C.

          Instances For

            Help the typechecker by explicitly translating from C to ShrinkHoms C.

            Instances For

              Help the typechecker by explicitly translating from ShrinkHoms C to C.

              Instances For

                The categorical equivalence between C and ShrinkHoms C, when C is locally small.

                Instances For

                  A category is essentially small if and only if the underlying type of its skeleton (i.e. the "set" of isomorphism classes) is small, and it is locally small.

                  A thin category is essentially small if and only if the underlying type of its skeleton is small.