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

• equiv_smallCategory : ∃ (S : Type w) (x : ), Nonempty (C S)

An essentially small category is equivalent to some small category.

Instances
theorem CategoryTheory.EssentiallySmall.equiv_smallCategory {C : Type u} [self : ] :
∃ (S : Type w) (x : ), Nonempty (C S)

An essentially small category is equivalent to some small category.

theorem CategoryTheory.EssentiallySmall.mk' {C : Type u} {S : Type w} (e : C S) :

Constructor for EssentiallySmall C from an explicit small category witness.

An arbitrarily chosen small model for an essentially small category.

Equations
Instances For
noncomputable instance CategoryTheory.smallCategorySmallModel (C : Type u) :
Equations
noncomputable def CategoryTheory.equivSmallModel (C : Type u) :
C

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

Equations
• = .some
Instances For
theorem CategoryTheory.essentiallySmall_congr {C : Type u} {D : Type u'} [] (e : C D) :

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
theorem CategoryTheory.LocallySmall.hom_small {C : Type u} [self : ] (X : C) (Y : C) :

A locally small category has small hom-types.

instance CategoryTheory.instSmallHomOfLocallySmall (C : Type u) [] (X : C) (Y : C) :
Equations
• =
theorem CategoryTheory.locallySmall_of_faithful {C : Type u} {D : Type u'} [] (F : ) [F.Faithful] [] :
theorem CategoryTheory.locallySmall_congr {C : Type u} {D : Type u'} [] (e : C D) :
@[instance 100]
Equations
• =
@[instance 100]
Equations
• =
@[instance 100]
Equations
• =

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') :
.fromShrinkHoms = X
@[simp]
@[simp]
theorem CategoryTheory.ShrinkHoms.instCategory_id (C : Type u) [] :
= (equivShrink (X.fromShrinkHoms X.fromShrinkHoms)) (CategoryTheory.CategoryStruct.id X.fromShrinkHoms)
@[simp]
theorem CategoryTheory.ShrinkHoms.instCategory_comp (C : Type u) [] :
∀ {X Y Z : } (f : X Y) (g : Y Z), = (equivShrink (X.fromShrinkHoms Z.fromShrinkHoms)) (CategoryTheory.CategoryStruct.comp ((equivShrink (X.fromShrinkHoms Y.fromShrinkHoms)).symm f) ((equivShrink (Y.fromShrinkHoms Z.fromShrinkHoms)).symm g))
noncomputable instance CategoryTheory.ShrinkHoms.instCategory (C : Type u) [] :
Equations
@[simp]
theorem CategoryTheory.ShrinkHoms.functor_obj (C : Type u) [] (X : C) :
@[simp]
theorem CategoryTheory.ShrinkHoms.functor_map (C : Type u) [] {X : C} {Y : C} (f : X Y) :
f = (equivShrink (X Y)) f
noncomputable def CategoryTheory.ShrinkHoms.functor (C : Type u) [] :

Implementation of ShrinkHoms.equivalence.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.ShrinkHoms.inverse_obj (C : Type u) [] :
X = X.fromShrinkHoms
@[simp]
theorem CategoryTheory.ShrinkHoms.inverse_map (C : Type u) [] (f : X Y) :
f = (equivShrink (X.fromShrinkHoms Y.fromShrinkHoms)).symm f
noncomputable def CategoryTheory.ShrinkHoms.inverse (C : Type u) [] :

Implementation of ShrinkHoms.equivalence.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.ShrinkHoms.equivalence_counitIso_inv_app (C : Type u) [] :
.counitIso.inv.app X = (equivShrink (X.fromShrinkHoms X.fromShrinkHoms)) (CategoryTheory.CategoryStruct.id X.fromShrinkHoms)
@[simp]
theorem CategoryTheory.ShrinkHoms.equivalence_unitIso_inv_app (C : Type u) [] (X : C) :
.unitIso.inv.app X =
@[simp]
theorem CategoryTheory.ShrinkHoms.equivalence_functor_map (C : Type u) [] {X : C} {Y : C} (f : X Y) :
.functor.map f = (equivShrink (X Y)) f
@[simp]
theorem CategoryTheory.ShrinkHoms.equivalence_counitIso_hom_app (C : Type u) [] :
.counitIso.hom.app X = (equivShrink (X.fromShrinkHoms X.fromShrinkHoms)) (CategoryTheory.CategoryStruct.id X.fromShrinkHoms)
@[simp]
theorem CategoryTheory.ShrinkHoms.equivalence_unitIso_hom_app (C : Type u) [] (X : C) :
.unitIso.hom.app X =
@[simp]
theorem CategoryTheory.ShrinkHoms.equivalence_inverse_map (C : Type u) [] (f : X Y) :
.inverse.map f = (equivShrink (X.fromShrinkHoms Y.fromShrinkHoms)).symm f
@[simp]
theorem CategoryTheory.ShrinkHoms.equivalence_inverse_obj (C : Type u) [] :
.inverse.obj X = X.fromShrinkHoms
@[simp]
theorem CategoryTheory.ShrinkHoms.equivalence_functor_obj (C : Type u) [] (X : C) :
.functor.obj X =
noncomputable def CategoryTheory.ShrinkHoms.equivalence (C : Type u) [] :

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
noncomputable instance CategoryTheory.Shrink.instCategoryShrink (C : Type u) [] :
Equations
noncomputable def CategoryTheory.Shrink.equivalence (C : Type u) [] :
C

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 CategoryTheory.locallySmall_fullSubcategory (C : Type u) [] (P : CProp) :
Equations
• =
@[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.

Equations
• =