mathlib documentation

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) [category_theory.category C] :
Prop

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

Instances

Constructor for essentially_small C from an explicit small category witness.

@[nolint]

An arbitrarily chosen small model for an essentially small category.

Equations

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

Equations
@[class]
structure category_theory.locally_small (C : Type u) [category_theory.category C] :
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
@[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

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

Implementation of shrink_homs.equivalence.

Equations

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]

Any thin category is locally small.

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