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

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

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

Instances For
theorem CategoryTheory.essentiallySmall_congr {C : Type u} {D : Type u'} [] (e : C D) :
• 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
theorem CategoryTheory.locallySmall_congr {C : Type u} {D : Type u'} [] (e : C D) :

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.

Instances For

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

Instances For

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

Instances For
@[simp]
theorem CategoryTheory.ShrinkHoms.to_from {C' : Type u_1} (X : C') :
@[simp]
theorem CategoryTheory.ShrinkHoms.from_to {C' : Type u_1} (X : ) :
@[simp]
theorem CategoryTheory.ShrinkHoms.instCategoryShrinkHoms_comp (C : Type u) :
∀ {X Y Z : } (f : X Y) (g : Y Z), = ↑() (CategoryTheory.CategoryStruct.comp () ())
@[simp]
@[simp]
theorem CategoryTheory.ShrinkHoms.functor_map (C : Type u) {X : C} {Y : C} (f : X Y) :
().map f = ↑(equivShrink (X Y)) f
noncomputable def CategoryTheory.ShrinkHoms.functor (C : Type u) :

Implementation of ShrinkHoms.equivalence.

Instances For
@[simp]
theorem CategoryTheory.ShrinkHoms.inverse_map (C : Type u) {X : } {Y : } (f : X Y) :
@[simp]
noncomputable def CategoryTheory.ShrinkHoms.inverse (C : Type u) :

Implementation of ShrinkHoms.equivalence.

Instances For
@[simp]
theorem CategoryTheory.ShrinkHoms.equivalence_unitIso_hom_app (C : Type u) (X : C) :
().unitIso.hom.app X =
@[simp]
theorem CategoryTheory.ShrinkHoms.equivalence_functor_obj (C : Type u) (X : C) :
().functor.obj 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_inverse_obj (C : Type u) (X : ) :
().inverse.obj X =
@[simp]
theorem CategoryTheory.ShrinkHoms.equivalence_inverse_map (C : Type u) {X : } {Y : } (f : X Y) :
().inverse.map f =
@[simp]
theorem CategoryTheory.ShrinkHoms.equivalence_unitIso_inv_app (C : Type u) (X : C) :
().unitIso.inv.app X =
noncomputable def CategoryTheory.ShrinkHoms.equivalence (C : Type u) :

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

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.

Any thin category is locally small.

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