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.

class CategoryTheory.EssentiallySmall (C : Type u) [CategoryTheory.Category.{v, u} C] : Prop

• 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].

theorem CategoryTheory.EssentiallySmall.mk' {C : Type u} [CategoryTheory.Category.{v, u} C] {S : Type w} [CategoryTheory.SmallCategory S] (e : C ≌ S) : CategoryTheory.EssentiallySmall C

Constructor for EssentiallySmall C from an explicit small category witness.

def CategoryTheory.SmallModel (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.EssentiallySmall C] : Type w

An arbitrarily chosen small model for an essentially small category.

noncomputable instance CategoryTheory.smallCategorySmallModel (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.EssentiallySmall C] : CategoryTheory.SmallCategory (CategoryTheory.SmallModel C)

noncomputable def CategoryTheory.equivSmallModel (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.EssentiallySmall C] : C ≌ CategoryTheory.SmallModel C

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

theorem CategoryTheory.essentiallySmall_congr {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (e : C ≌ D) : CategoryTheory.EssentiallySmall C ↔ CategoryTheory.EssentiallySmall D

theorem CategoryTheory.Discrete.essentiallySmallOfSmall {α : Type u} [Small.{w, u} α] : CategoryTheory.EssentiallySmall (CategoryTheory.Discrete α)

theorem CategoryTheory.essentiallySmallSelf (C : Type u) [CategoryTheory.Category.{v, u} C] : CategoryTheory.EssentiallySmall C

class CategoryTheory.LocallySmall (C : Type u) [CategoryTheory.Category.{v, u} C] : Prop

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

instance CategoryTheory.instSmallHomToQuiverToCategoryStruct (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall C] (X : C) (Y : C) : Small.{w, v} (X ⟶ Y)

theorem CategoryTheory.locallySmall_congr {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (e : C ≌ D) : CategoryTheory.LocallySmall C ↔ CategoryTheory.LocallySmall D

instance CategoryTheory.locallySmall_self (C : Type u) [CategoryTheory.Category.{v, u} C] : CategoryTheory.LocallySmall C

theorem CategoryTheory.locallySmall_max {C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.LocallySmall C

instance CategoryTheory.locallySmall_of_essentiallySmall (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.EssentiallySmall C] : CategoryTheory.LocallySmall C

def CategoryTheory.ShrinkHoms (C : Type u) : Type u

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.

def CategoryTheory.ShrinkHoms.toShrinkHoms {C' : Type u_2} (X : C') : CategoryTheory.ShrinkHoms C'

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

def CategoryTheory.ShrinkHoms.fromShrinkHoms {C' : Type u_2} (X : CategoryTheory.ShrinkHoms C') : C'

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

@[simp]

theorem CategoryTheory.ShrinkHoms.to_from {C' : Type u_1} (X : C') : CategoryTheory.ShrinkHoms.fromShrinkHoms (CategoryTheory.ShrinkHoms.toShrinkHoms X) = X

@[simp]

theorem CategoryTheory.ShrinkHoms.from_to {C' : Type u_1} (X : CategoryTheory.ShrinkHoms C') : CategoryTheory.ShrinkHoms.toShrinkHoms (CategoryTheory.ShrinkHoms.fromShrinkHoms X) = X

@[simp]

theorem CategoryTheory.ShrinkHoms.instCategoryShrinkHoms_comp (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall C] : ∀ {X Y Z : CategoryTheory.ShrinkHoms C} (f : X ⟶ Y) (g : Y ⟶ Z), CategoryTheory.CategoryStruct.comp f g = ↑(equivShrink (CategoryTheory.ShrinkHoms.fromShrinkHoms X ⟶ CategoryTheory.ShrinkHoms.fromShrinkHoms Z)) (CategoryTheory.CategoryStruct.comp (↑(equivShrink (CategoryTheory.ShrinkHoms.fromShrinkHoms X ⟶ CategoryTheory.ShrinkHoms.fromShrinkHoms Y)).symm f) (↑(equivShrink (CategoryTheory.ShrinkHoms.fromShrinkHoms Y ⟶ CategoryTheory.ShrinkHoms.fromShrinkHoms Z)).symm g))

@[simp]

theorem CategoryTheory.ShrinkHoms.instCategoryShrinkHoms_id (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall C] (X : CategoryTheory.ShrinkHoms C) : CategoryTheory.CategoryStruct.id X = ↑(equivShrink (CategoryTheory.ShrinkHoms.fromShrinkHoms X ⟶ CategoryTheory.ShrinkHoms.fromShrinkHoms X)) (CategoryTheory.CategoryStruct.id (CategoryTheory.ShrinkHoms.fromShrinkHoms X))

noncomputable instance CategoryTheory.ShrinkHoms.instCategoryShrinkHoms (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall C] : CategoryTheory.Category.{w, u} (CategoryTheory.ShrinkHoms C)

@[simp]

theorem CategoryTheory.ShrinkHoms.functor_obj (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall C] (X : C) : (CategoryTheory.ShrinkHoms.functor C).obj X = CategoryTheory.ShrinkHoms.toShrinkHoms X

@[simp]

theorem CategoryTheory.ShrinkHoms.functor_map (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall C] {X : C} {Y : C} (f : X ⟶ Y) : (CategoryTheory.ShrinkHoms.functor C).map f = ↑(equivShrink (X ⟶ Y)) f

noncomputable def CategoryTheory.ShrinkHoms.functor (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall C] : CategoryTheory.Functor C (CategoryTheory.ShrinkHoms C)

Implementation of ShrinkHoms.equivalence.

@[simp]

theorem CategoryTheory.ShrinkHoms.inverse_map (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall C] {X : CategoryTheory.ShrinkHoms C} {Y : CategoryTheory.ShrinkHoms C} (f : X ⟶ Y) : (CategoryTheory.ShrinkHoms.inverse C).map f = ↑(equivShrink (CategoryTheory.ShrinkHoms.fromShrinkHoms X ⟶ CategoryTheory.ShrinkHoms.fromShrinkHoms Y)).symm f

@[simp]

theorem CategoryTheory.ShrinkHoms.inverse_obj (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall C] (X : CategoryTheory.ShrinkHoms C) : (CategoryTheory.ShrinkHoms.inverse C).obj X = CategoryTheory.ShrinkHoms.fromShrinkHoms X

noncomputable def CategoryTheory.ShrinkHoms.inverse (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall C] : CategoryTheory.Functor (CategoryTheory.ShrinkHoms C) C

Implementation of ShrinkHoms.equivalence.

@[simp]

theorem CategoryTheory.ShrinkHoms.equivalence_unitIso_hom_app (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall C] (X : C) : (CategoryTheory.ShrinkHoms.equivalence C).unitIso.hom.app X = CategoryTheory.CategoryStruct.id X

@[simp]

theorem CategoryTheory.ShrinkHoms.equivalence_functor_obj (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall C] (X : C) : (CategoryTheory.ShrinkHoms.equivalence C).functor.obj X = CategoryTheory.ShrinkHoms.toShrinkHoms X

@[simp]

theorem CategoryTheory.ShrinkHoms.equivalence_functor_map (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall C] {X : C} {Y : C} (f : X ⟶ Y) : (CategoryTheory.ShrinkHoms.equivalence C).functor.map f = ↑(equivShrink (X ⟶ Y)) f

@[simp]

theorem CategoryTheory.ShrinkHoms.equivalence_counitIso_inv_app (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall C] (X : CategoryTheory.ShrinkHoms C) : (CategoryTheory.ShrinkHoms.equivalence C).counitIso.inv.app X = ↑(equivShrink (CategoryTheory.ShrinkHoms.fromShrinkHoms X ⟶ CategoryTheory.ShrinkHoms.fromShrinkHoms X)) (CategoryTheory.CategoryStruct.id (CategoryTheory.ShrinkHoms.fromShrinkHoms X))

@[simp]

theorem CategoryTheory.ShrinkHoms.equivalence_inverse_obj (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall C] (X : CategoryTheory.ShrinkHoms C) : (CategoryTheory.ShrinkHoms.equivalence C).inverse.obj X = CategoryTheory.ShrinkHoms.fromShrinkHoms X

@[simp]

theorem CategoryTheory.ShrinkHoms.equivalence_counitIso_hom_app (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall C] (X : CategoryTheory.ShrinkHoms C) : (CategoryTheory.ShrinkHoms.equivalence C).counitIso.hom.app X = ↑(equivShrink (CategoryTheory.ShrinkHoms.fromShrinkHoms X ⟶ CategoryTheory.ShrinkHoms.fromShrinkHoms X)) (CategoryTheory.CategoryStruct.id (CategoryTheory.ShrinkHoms.fromShrinkHoms X))

@[simp]

theorem CategoryTheory.ShrinkHoms.equivalence_inverse_map (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall C] {X : CategoryTheory.ShrinkHoms C} {Y : CategoryTheory.ShrinkHoms C} (f : X ⟶ Y) : (CategoryTheory.ShrinkHoms.equivalence C).inverse.map f = ↑(equivShrink (CategoryTheory.ShrinkHoms.fromShrinkHoms X ⟶ CategoryTheory.ShrinkHoms.fromShrinkHoms Y)).symm f

@[simp]

theorem CategoryTheory.ShrinkHoms.equivalence_unitIso_inv_app (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall C] (X : C) : (CategoryTheory.ShrinkHoms.equivalence C).unitIso.inv.app X = CategoryTheory.CategoryStruct.id X

noncomputable def CategoryTheory.ShrinkHoms.equivalence (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall C] : C ≌ CategoryTheory.ShrinkHoms C

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

theorem CategoryTheory.essentiallySmall_iff (C : Type u) [CategoryTheory.Category.{v, u} C] : CategoryTheory.EssentiallySmall C ↔ Small.{w, u} (CategoryTheory.Skeleton C) ∧ CategoryTheory.LocallySmall C

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.

theorem CategoryTheory.essentiallySmall_of_small_of_locallySmall (C : Type u) [CategoryTheory.Category.{v, u} C] [Small.{w, u} C] [CategoryTheory.LocallySmall C] : CategoryTheory.EssentiallySmall C

instance CategoryTheory.locallySmall_of_thin {C : Type u} [CategoryTheory.Category.{v, u} C] [Quiver.IsThin C] : CategoryTheory.LocallySmall C

Any thin category is locally small.

theorem CategoryTheory.essentiallySmall_iff_of_thin {C : Type u} [CategoryTheory.Category.{v, u} C] [Quiver.IsThin C] : CategoryTheory.EssentiallySmall C ↔ Small.{w, u} (CategoryTheory.Skeleton C)

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