Essentially small categories.

A category given by (C : Type u) [Category.{v} C] is w-essentially small if there exists a SmallModel C : Type w equipped with [SmallCategory (SmallModel C)] and an equivalence C ≌ SmallModel 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 CategoryTheory.EssentiallySmall (C : Type u) [CategoryTheory.Category.{v, u} C] : Prop

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

• equiv_smallCategory : ∃ (S : Type w) (x : CategoryTheory.SmallCategory S), Nonempty (C ≌ S)

  An essentially small category is equivalent to some small category.

theorem CategoryTheory.EssentiallySmall.mk' {C : Type u} [CategoryTheory.Category.{v, u} C] {S : Type w} [CategoryTheory.SmallCategory S] (e : C ≌ S) : CategoryTheory.EssentiallySmall.{w, v, u} C

Constructor for EssentiallySmall C from an explicit small category witness.

def CategoryTheory.SmallModel (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.EssentiallySmall.{w, v, u} C] : Type w

An arbitrarily chosen small model for an essentially small category.

Equations

• CategoryTheory.SmallModel.{?u.24, ?u.23, ?u.22} C = Classical.choose ⋯

noncomputable instance CategoryTheory.smallCategorySmallModel (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.EssentiallySmall.{w, v, u} C] : CategoryTheory.SmallCategory (CategoryTheory.SmallModel.{w, v, u} C)

Equations

• CategoryTheory.smallCategorySmallModel C = Classical.choose ⋯

noncomputable def CategoryTheory.equivSmallModel (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.EssentiallySmall.{w, v, u} C] : C ≌ CategoryTheory.SmallModel.{w, v, u} C

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

Equations

• CategoryTheory.equivSmallModel C = ⋯.some

instance CategoryTheory.instEssentiallySmallOpposite (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.EssentiallySmall.{w, v, u} C] : CategoryTheory.EssentiallySmall.{w, v, u} Cᵒᵖ

Equations

• ⋯ = ⋯

theorem CategoryTheory.essentiallySmall_congr {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (e : C ≌ D) : CategoryTheory.EssentiallySmall.{w, v, u} C ↔ CategoryTheory.EssentiallySmall.{w, v', u'} D

theorem CategoryTheory.Discrete.essentiallySmallOfSmall {α : Type u} [Small.{w, u} α] : CategoryTheory.EssentiallySmall.{w, u, u} (CategoryTheory.Discrete α)

theorem CategoryTheory.essentiallySmallSelf (C : Type u) [CategoryTheory.Category.{v, u} C] : CategoryTheory.EssentiallySmall.{max w v u, v, u} C

class CategoryTheory.LocallySmall (C : Type u) [CategoryTheory.Category.{v, u} C] : Prop

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

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

• hom_small : ∀ (X Y : C), Small.{w, v} (X ⟶ Y)

  A locally small category has small hom-types.

instance CategoryTheory.instSmallHomOfLocallySmall (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] (X Y : C) : Small.{w, v} (X ⟶ Y)

Equations

• ⋯ = ⋯

theorem CategoryTheory.locallySmall_of_faithful {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (F : CategoryTheory.Functor C D) [F.Faithful] [CategoryTheory.LocallySmall.{w, v', u'} D] : CategoryTheory.LocallySmall.{w, v, u} C

theorem CategoryTheory.locallySmall_congr {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (e : C ≌ D) : CategoryTheory.LocallySmall.{w, v, u} C ↔ CategoryTheory.LocallySmall.{w, v', u'} D

@[instance 100]

instance CategoryTheory.locallySmall_self (C : Type u) [CategoryTheory.Category.{v, u} C] : CategoryTheory.LocallySmall.{v, v, u} C

Equations

• ⋯ = ⋯

@[instance 100]

instance CategoryTheory.locallySmall_of_univLE (C : Type u) [CategoryTheory.Category.{v, u} C] [UnivLE.{v, w} ] : CategoryTheory.LocallySmall.{w, v, u} C

Equations

• ⋯ = ⋯

theorem CategoryTheory.locallySmall_max {C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.LocallySmall.{max v w, v, u} C

@[instance 100]

instance CategoryTheory.locallySmall_of_essentiallySmall (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.EssentiallySmall.{w, v, u} C] : CategoryTheory.LocallySmall.{w, v, u} C

Equations

• ⋯ = ⋯

def CategoryTheory.ShrinkHoms (C : Type u) : Type u

We define a type alias ShrinkHoms C for C. When we have LocallySmall.{w} C, we'll put a Category.{w} instance on ShrinkHoms C.

Equations

• CategoryTheory.ShrinkHoms.{?u.10} C = C

def CategoryTheory.ShrinkHoms.toShrinkHoms {C' : Type u_2} (X : C') : CategoryTheory.ShrinkHoms.{u_2} C'

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

Equations

• CategoryTheory.ShrinkHoms.toShrinkHoms X = X

def CategoryTheory.ShrinkHoms.fromShrinkHoms {C' : Type u_2} (X : CategoryTheory.ShrinkHoms.{u_2} C') : C'

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

Equations

• X.fromShrinkHoms = X

@[simp]

theorem CategoryTheory.ShrinkHoms.to_from {C' : Type u_1} (X : C') : (CategoryTheory.ShrinkHoms.toShrinkHoms X).fromShrinkHoms = X

@[simp]

theorem CategoryTheory.ShrinkHoms.from_to {C' : Type u_1} (X : CategoryTheory.ShrinkHoms.{u_1} C') : CategoryTheory.ShrinkHoms.toShrinkHoms X.fromShrinkHoms = X

noncomputable instance CategoryTheory.ShrinkHoms.instCategory (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] : CategoryTheory.Category.{w, u} (CategoryTheory.ShrinkHoms.{u} C)

Equations

• CategoryTheory.ShrinkHoms.instCategory C = CategoryTheory.Category.mk ⋯ ⋯ ⋯

@[simp]

theorem CategoryTheory.ShrinkHoms.instCategory_comp (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] {X✝ Y✝ Z✝ : CategoryTheory.ShrinkHoms.{u} C} (f : X✝ ⟶ Y✝) (g : Y✝ ⟶ Z✝) : CategoryTheory.CategoryStruct.comp f g = (equivShrink (X✝.fromShrinkHoms ⟶ Z✝.fromShrinkHoms)) (CategoryTheory.CategoryStruct.comp ((equivShrink (X✝.fromShrinkHoms ⟶ Y✝.fromShrinkHoms)).symm f) ((equivShrink (Y✝.fromShrinkHoms ⟶ Z✝.fromShrinkHoms)).symm g))

@[simp]

theorem CategoryTheory.ShrinkHoms.instCategory_id (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] (X : CategoryTheory.ShrinkHoms.{u} C) : CategoryTheory.CategoryStruct.id X = (equivShrink (X.fromShrinkHoms ⟶ X.fromShrinkHoms)) (CategoryTheory.CategoryStruct.id X.fromShrinkHoms)

noncomputable def CategoryTheory.ShrinkHoms.functor (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] : CategoryTheory.Functor C (CategoryTheory.ShrinkHoms.{u} C)

Implementation of ShrinkHoms.equivalence.

Equations

• CategoryTheory.ShrinkHoms.functor C = { obj := fun (X : C) => CategoryTheory.ShrinkHoms.toShrinkHoms X, map := fun {X Y : C} (f : X ⟶ Y) => (equivShrink (X ⟶ Y)) f, map_id := ⋯, map_comp := ⋯ }

@[simp]

theorem CategoryTheory.ShrinkHoms.functor_obj (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] (X : C) : (CategoryTheory.ShrinkHoms.functor C).obj X = CategoryTheory.ShrinkHoms.toShrinkHoms X

@[simp]

theorem CategoryTheory.ShrinkHoms.functor_map (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] {X Y : C} (f : X ⟶ Y) : (CategoryTheory.ShrinkHoms.functor C).map f = (equivShrink (X ⟶ Y)) f

noncomputable def CategoryTheory.ShrinkHoms.inverse (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] : CategoryTheory.Functor (CategoryTheory.ShrinkHoms.{u} C) C

Implementation of ShrinkHoms.equivalence.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.ShrinkHoms.inverse_map (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] {X Y : CategoryTheory.ShrinkHoms.{u} C} (f : X ⟶ Y) : (CategoryTheory.ShrinkHoms.inverse C).map f = (equivShrink (X.fromShrinkHoms ⟶ Y.fromShrinkHoms)).symm f

@[simp]

theorem CategoryTheory.ShrinkHoms.inverse_obj (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] (X : CategoryTheory.ShrinkHoms.{u} C) : (CategoryTheory.ShrinkHoms.inverse C).obj X = X.fromShrinkHoms

noncomputable def CategoryTheory.ShrinkHoms.equivalence (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] : C ≌ CategoryTheory.ShrinkHoms.{u} C

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.ShrinkHoms.equivalence_functor (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] : (CategoryTheory.ShrinkHoms.equivalence C).functor = CategoryTheory.ShrinkHoms.functor C

@[simp]

theorem CategoryTheory.ShrinkHoms.equivalence_inverse (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] : (CategoryTheory.ShrinkHoms.equivalence C).inverse = CategoryTheory.ShrinkHoms.inverse C

@[simp]

theorem CategoryTheory.ShrinkHoms.equivalence_counitIso (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] : (CategoryTheory.ShrinkHoms.equivalence C).counitIso = CategoryTheory.NatIso.ofComponents (fun (x : CategoryTheory.ShrinkHoms.{u} C) => CategoryTheory.Iso.refl (((CategoryTheory.ShrinkHoms.inverse C).comp (CategoryTheory.ShrinkHoms.functor C)).obj x)) ⋯

@[simp]

theorem CategoryTheory.ShrinkHoms.equivalence_unitIso (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] : (CategoryTheory.ShrinkHoms.equivalence C).unitIso = CategoryTheory.NatIso.ofComponents (fun (x : C) => CategoryTheory.Iso.refl ((CategoryTheory.Functor.id C).obj x)) ⋯

noncomputable instance CategoryTheory.Shrink.instCategoryShrink (C : Type u) [CategoryTheory.Category.{v, u} C] [Small.{w, u} C] : CategoryTheory.Category.{v, w} (Shrink.{w, u} C)

Equations

• CategoryTheory.Shrink.instCategoryShrink C = CategoryTheory.InducedCategory.category ⇑(equivShrink C).symm

noncomputable def CategoryTheory.Shrink.equivalence (C : Type u) [CategoryTheory.Category.{v, u} C] [Small.{w, u} C] : C ≌ Shrink.{w, u} C

The categorical equivalence between C and Shrink C, when C is small.

Equations

• CategoryTheory.Shrink.equivalence C = (CategoryTheory.inducedFunctor ⇑(equivShrink C).symm).asEquivalence.symm

theorem CategoryTheory.essentiallySmall_iff (C : Type u) [CategoryTheory.Category.{v, u} C] : CategoryTheory.EssentiallySmall.{w, v, u} C ↔ Small.{w, u} (CategoryTheory.Skeleton C) ∧ CategoryTheory.LocallySmall.{w, v, u} C

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.

theorem CategoryTheory.essentiallySmall_of_small_of_locallySmall (C : Type u) [CategoryTheory.Category.{v, u} C] [Small.{w, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] : CategoryTheory.EssentiallySmall.{w, v, u} C

instance CategoryTheory.locallySmall_fullSubcategory (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] (P : C → Prop) : CategoryTheory.LocallySmall.{w, v, u} (CategoryTheory.FullSubcategory P)

Equations

• ⋯ = ⋯

instance CategoryTheory.essentiallySmall_fullSubcategory_mem (C : Type u) [CategoryTheory.Category.{v, u} C] (s : Set C) [Small.{w, u} ↑s] [CategoryTheory.LocallySmall.{w, v, u} C] : CategoryTheory.EssentiallySmall.{w, v, u} (CategoryTheory.FullSubcategory fun (x : C) => x ∈ s)

Equations

• ⋯ = ⋯

@[instance 100]

instance CategoryTheory.locallySmall_of_thin {C : Type u} [CategoryTheory.Category.{v, u} C] [Quiver.IsThin C] : CategoryTheory.LocallySmall.{w, v, u} C

Any thin category is locally small.

Equations

• ⋯ = ⋯

theorem CategoryTheory.essentiallySmall_iff_of_thin {C : Type u} [CategoryTheory.Category.{v, u} C] [Quiver.IsThin C] : CategoryTheory.EssentiallySmall.{w, v, u} C ↔ Small.{w, u} (CategoryTheory.Skeleton C)

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

instance CategoryTheory.instSmallDiscrete (C : Type u) [Small.{w, u} C] : Small.{w, u} (CategoryTheory.Discrete C)

Equations

• ⋯ = ⋯