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.
- equiv_small_category : ∃ (S : Type ?) (_x : category_theory.small_category S), nonempty (C ≌ S)
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.
An arbitrarily chosen small model for an essentially small category.
Equations
Instances for category_theory.small_model
Equations
The (noncomputable) categorical equivalence between an essentially small category and its small model.
Equations
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.
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
- X.from_shrink_homs = X
Equations
- category_theory.shrink_homs.category_theory.category C = {to_category_struct := {to_quiver := {hom := λ (X Y : category_theory.shrink_homs C), shrink (X.from_shrink_homs ⟶ Y.from_shrink_homs)}, id := λ (X : category_theory.shrink_homs C), ⇑(equiv_shrink (X.from_shrink_homs ⟶ X.from_shrink_homs)) (𝟙 X.from_shrink_homs), comp := λ (X Y Z : category_theory.shrink_homs C) (f : X ⟶ Y) (g : Y ⟶ Z), ⇑(equiv_shrink (X.from_shrink_homs ⟶ Z.from_shrink_homs)) (⇑((equiv_shrink (X.from_shrink_homs ⟶ Y.from_shrink_homs)).symm) f ≫ ⇑((equiv_shrink (Y.from_shrink_homs ⟶ Z.from_shrink_homs)).symm) g)}, id_comp' := _, comp_id' := _, assoc' := _}
Implementation of shrink_homs.equivalence
.
Equations
- category_theory.shrink_homs.functor C = {obj := λ (X : C), category_theory.shrink_homs.to_shrink_homs X, map := λ (X Y : C) (f : X ⟶ Y), ⇑(equiv_shrink (X ⟶ Y)) f, map_id' := _, map_comp' := _}
Implementation of shrink_homs.equivalence
.
Equations
- category_theory.shrink_homs.inverse C = {obj := λ (X : category_theory.shrink_homs C), X.from_shrink_homs, map := λ (X Y : category_theory.shrink_homs C) (f : X ⟶ Y), ⇑((equiv_shrink (X.from_shrink_homs ⟶ Y.from_shrink_homs)).symm) f, map_id' := _, map_comp' := _}
The categorical equivalence between C
and shrink_homs C
, when C
is locally small.
Equations
- category_theory.shrink_homs.equivalence C = category_theory.equivalence.mk (category_theory.shrink_homs.functor C) (category_theory.shrink_homs.inverse C) (category_theory.nat_iso.of_components (λ (X : C), category_theory.iso.refl X) _) (category_theory.nat_iso.of_components (λ (X : category_theory.shrink_homs C), category_theory.iso.refl X) _)
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.