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.

    Equations
    Instances For

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

      Equations
      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.

          Equations
          Instances For

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

            Equations
            Instances For

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

              Equations
              Instances For

                Implementation of ShrinkHoms.equivalence.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For

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

                  Equations
                  • One or more equations did not get rendered due to their size.
                  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.