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.

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

Instances

    An essentially small category is equivalent to some small category.

    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

        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.

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

          A locally small category has small hom-types.

        Instances

          A locally small category has small hom-types.

          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
              • X.fromShrinkHoms = X
              Instances For
                @[simp]
                theorem CategoryTheory.ShrinkHoms.to_from {C' : Type u_1} (X : C') :
                @[simp]
                theorem CategoryTheory.ShrinkHoms.instCategory_comp (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] :
                ∀ {X Y Z : CategoryTheory.ShrinkHoms.{u} C} (f : X Y) (g : Y Z), CategoryTheory.CategoryStruct.comp f g = (equivShrink (X.fromShrinkHoms Z.fromShrinkHoms)) (CategoryTheory.CategoryStruct.comp ((equivShrink (X.fromShrinkHoms Y.fromShrinkHoms)).symm f) ((equivShrink (Y.fromShrinkHoms Z.fromShrinkHoms)).symm g))

                Implementation of ShrinkHoms.equivalence.

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

                      The categorical equivalence between C and Shrink C, when C is small.

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

                        @[instance 100]

                        Any thin category is locally small.

                        Equations
                        • =

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