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) [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 : SmallCategory S), Nonempty (C ≌ S)

  An essentially small category is equivalent to some small category.

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

Constructor for EssentiallySmall C from an explicit small category witness.

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

An arbitrarily chosen small model for an essentially small category.

Equations

• CategoryTheory.SmallModel.{?u.18, ?u.17, ?u.16} C = Classical.choose ⋯

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

Equations

• CategoryTheory.smallCategorySmallModel C = Classical.choose ⋯

noncomputable def CategoryTheory.equivSmallModel (C : Type u) [Category.{v, u} C] [EssentiallySmall.{w, v, u} C] : C ≌ 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) [Category.{v, u} C] [EssentiallySmall.{w, v, u} C] : EssentiallySmall.{w, v, u} Cᵒᵖ

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

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

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

class CategoryTheory.LocallySmall (C : Type u) [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) [Category.{v, u} C] [LocallySmall.{w, v, u} C] (X Y : C) : Small.{w, v} (X ⟶ Y)

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

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

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

@[instance 100]

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

@[instance 100]

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

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

@[instance 100]

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

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.6} C = C

def CategoryTheory.ShrinkHoms.toShrinkHoms {C' : Type u_2} (X : C') : 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 : 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') : (toShrinkHoms X).fromShrinkHoms = X

@[simp]

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

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

Equations

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

@[simp]

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

@[simp]

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

noncomputable def CategoryTheory.ShrinkHoms.functor (C : Type u) [Category.{v, u} C] [LocallySmall.{w, v, u} C] : Functor C (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_map (C : Type u) [Category.{v, u} C] [LocallySmall.{w, v, u} C] {X Y : C} (f : X ⟶ Y) : (functor C).map f = (equivShrink (X ⟶ Y)) f

@[simp]

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

noncomputable def CategoryTheory.ShrinkHoms.inverse (C : Type u) [Category.{v, u} C] [LocallySmall.{w, v, u} C] : Functor (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_obj (C : Type u) [Category.{v, u} C] [LocallySmall.{w, v, u} C] (X : ShrinkHoms.{u} C) : (inverse C).obj X = X.fromShrinkHoms

@[simp]

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

noncomputable def CategoryTheory.ShrinkHoms.equivalence (C : Type u) [Category.{v, u} C] [LocallySmall.{w, v, u} C] : C ≌ 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) [Category.{v, u} C] [LocallySmall.{w, v, u} C] : (equivalence C).functor = functor C

@[simp]

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

@[simp]

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

@[simp]

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

instance CategoryTheory.ShrinkHoms.instIsEquivalenceFunctor (C : Type u) [Category.{v, u} C] [LocallySmall.{w, v, u} C] : (functor C).IsEquivalence

instance CategoryTheory.ShrinkHoms.instIsEquivalenceInverse (C : Type u) [Category.{v, u} C] [LocallySmall.{w, v, u} C] : (inverse C).IsEquivalence

noncomputable instance CategoryTheory.Shrink.instCategoryShrink (C : Type u) [Category.{v, u} C] [Small.{w, u} C] : 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) [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.Equivalence.induced (equivShrink C).symm).symm

instance CategoryTheory.Shrink.instLocallySmallShrink (C : Type u) [Category.{v, u} C] [Small.{w', u} C] [LocallySmall.{w, v, u} C] : LocallySmall.{w, v, w'} (Shrink.{w', u} C)

theorem CategoryTheory.essentiallySmall_iff (C : Type u) [Category.{v, u} C] : EssentiallySmall.{w, v, u} C ↔ Small.{w, u} (Skeleton C) ∧ 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) [Category.{v, u} C] [Small.{w, u} C] [LocallySmall.{w, v, u} C] : EssentiallySmall.{w, v, u} C

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

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

@[instance 100]

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

Any thin category is locally small.

theorem CategoryTheory.essentiallySmall_iff_of_thin {C : Type u} [Category.{v, u} C] [Quiver.IsThin C] : EssentiallySmall.{w, v, u} C ↔ Small.{w, u} (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} (Discrete C)