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.

source

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.

Instances

source

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.

source

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

Instances For

source

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

SmallCategory (SmallModel.{w, v, u} C)

Equations

source

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

Instances For

source

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

EssentiallySmall.{w, v, u} Cᵒᵖ

source

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

source

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

EssentiallySmall.{w, u, u} (Discrete α)

source

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

EssentiallySmall.{max w v u, v, u} C

source

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.

Instances

source

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

Small.{w, v} (X ⟶ Y)

source

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

LocallySmall.{w, v, u} Cᵒᵖ

source

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

source

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

source

@[instance 100]

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

LocallySmall.{v, v, u} C

source

@[instance 100]

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

LocallySmall.{w, v, u} C

source

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

LocallySmall.{max v w, v, u} C

source

@[instance 100]

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

LocallySmall.{w, v, u} C

source

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

Instances For

source

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

Instances For

source

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

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

Equations

Instances For

source

@[simp]

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

(toShrinkHoms X).fromShrinkHoms = X

source

@[simp]

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

toShrinkHoms X.fromShrinkHoms = X

source

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

Category.{w, u} (ShrinkHoms.{u} C)

Equations

source

@[simp]

theorem CategoryTheory.ShrinkHoms.id_def (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)

source

@[simp]

theorem CategoryTheory.ShrinkHoms.comp_def (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))

source

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

Instances For

source

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

source

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

source

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

Instances For

source

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

source

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

source

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

Instances For

source

@[simp]

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

(equivalence C).inverse = inverse C

source

@[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)) ⋯

source

@[simp]

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

(equivalence C).functor = functor C

source

@[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)) ⋯

source

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

(functor C).IsEquivalence

source

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

(inverse C).IsEquivalence

source

instance CategoryTheory.ShrinkHoms.instUnique {T : Type u} [Unique T] :

Unique (ShrinkHoms.{u} T)

Equations

source

instance CategoryTheory.ShrinkHoms.instIsDiscrete {T : Type u} [Category.{v, u} T] [IsDiscrete T] :

IsDiscrete (ShrinkHoms.{u} T)

source

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

Category.{v, w} (Shrink.{w, u} C)

Equations

source

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

Instances For

source

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)

source

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.

source