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.

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

    Equations

    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

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

      Equations

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

      Equations
      • X.fromShrinkHoms = X
      @[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

      Implementation of ShrinkHoms.equivalence.

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

      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.

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

      Equations

      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.