mathlibdocumentation

category_theory.essentially_small

Essentially small categories. #

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
• equiv_small_category : ∃ (S : Type ?) [_inst_2_1 : , nonempty (C S)

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

Instances
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]
def category_theory.small_model (C : Type u)  :
Type w

An arbitrarily chosen small model for an essentially small category.

Equations
@[instance]
Equations

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
@[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) :
@[instance]
def category_theory.locally_small_self (C : Type u)  :
@[instance]
@[nolint]
def category_theory.shrink_homs (C : Type u) :
Type u

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
def category_theory.shrink_homs.to_shrink_homs {C' : Type u_1} (X : C') :

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') :
@[simp]
@[instance]
Equations
@[simp]
theorem category_theory.shrink_homs.category_theory.category_comp (C : Type u) (X Y Z : category_theory.shrink_homs C) (f : X Y) (g : Y Z) :
f g = (.symm) f .symm) g)
@[simp]
theorem category_theory.shrink_homs.functor_obj (C : Type u) (X : C) :

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]
theorem category_theory.shrink_homs.inverse_map (C : Type u) (X Y : category_theory.shrink_homs C) (f : X Y) :
= .symm) f
@[simp]
theorem category_theory.shrink_homs.inverse_obj (C : Type u)  :

Implementation of shrink_homs.equivalence.

Equations
@[simp]

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

Equations
@[simp]
@[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]
@[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.

@[instance]
def category_theory.locally_small_of_thin {C : Type u} [∀ (X Y : C), subsingleton (X Y)] :

Any thin category is locally small.

theorem category_theory.essentially_small_iff_of_thin {C : Type u} [∀ (X Y : C), subsingleton (X Y)] :

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