# mathlib3documentation

category_theory.essentially_small

# Essentially small categories. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

A category given by (C : Type u) [category.{v} C] is w-essentially small if there exists a small_model C : Type w equipped with [small_category (small_model 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]
structure category_theory.essentially_small (C : Type u)  :
Prop

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

Instances of this typeclass
theorem category_theory.essentially_small.mk' {C : Type u} {S : Type w} (e : C S) :

Constructor for essentially_small C from an explicit small category witness.

@[nolint]

An arbitrarily chosen small model for an essentially small category.

Equations
Instances for category_theory.small_model
@[protected, instance]
Equations
noncomputable def category_theory.equiv_small_model (C : Type u)  :

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

Equations
theorem category_theory.essentially_small_congr {C : Type u} {D : Type u'} (e : C D) :
@[class]
structure category_theory.locally_small (C : Type u)  :
Prop
• hom_small : ( (X Y : C), small (X Y)) . "apply_instance"

A category is w-locally small if every hom set is w-small.

See shrink_homs C for a category instance where every hom set has been replaced by a small model.

Instances of this typeclass
@[protected, instance]
def category_theory.quiver.hom.small (C : Type u) (X Y : C) :
small (X Y)
theorem category_theory.locally_small_congr {C : Type u} {D : Type u'} (e : C D) :
@[protected, instance]
@[protected, instance]
@[nolint]

We define a type alias shrink_homs C for C. When we have locally_small.{w} C, we'll put a category.{w} instance on shrink_homs C.

Equations
Instances for category_theory.shrink_homs

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

Equations

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

Equations
@[simp]
theorem category_theory.shrink_homs.to_from {C' : Type u_1} (X : C') :
@[protected, instance]
Equations
@[simp]
@[simp]
noncomputable def category_theory.shrink_homs.functor (C : Type u)  :

Implementation of shrink_homs.equivalence.

Equations
@[simp]
theorem category_theory.shrink_homs.functor_map (C : Type u) (X Y : C) (f : X Y) :
= (equiv_shrink (X Y)) f
@[simp]
@[simp]
noncomputable def category_theory.shrink_homs.inverse (C : Type u)  :

Implementation of shrink_homs.equivalence.

Equations
@[simp]
noncomputable def category_theory.shrink_homs.equivalence (C : Type u)  :

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

Equations
@[simp]
@[simp]
@[simp]
theorem category_theory.shrink_homs.equivalence_functor_map (C : Type u) (X Y : C) (f : X Y) :
= (equiv_shrink (X Y)) f
@[simp]

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.

@[protected, instance]

Any thin category is locally small.

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