mathlib3 documentation

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]

A category is essentially_small.{w} if there exists an equivalence to some S : Type w with [small_category 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

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

Equations
@[class]
  • 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]
@[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

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.

@[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.