Mathlib.CategoryTheory.EssentiallySmall

CategoryTheory.EssentiallySmall structure

(C : Type u) [Category.{v} C]

Full source

/-- A category is `EssentiallySmall.{w}` if there exists
an equivalence to some `S : Type w` with `[SmallCategory S]`. -/
@[pp_with_univ]
class EssentiallySmall (C : Type u) [Category.{v} C] : Prop where
  /-- An essentially small category is equivalent to some small category. -/
  equiv_smallCategory : ∃ (S : Type w) (_ : SmallCategory S), Nonempty (C ≌ S)

Essentially small category

Informal description

A category $ C $ is called essentially small (with respect to a universe $ w $) if there exists a small category $ S $ (i.e., $ S $ is of type $ \text{Type } w $) and an equivalence of categories $ C \simeq S $.

CategoryTheory.EssentiallySmall.mk' theorem

{C : Type u} [Category.{v} C] {S : Type w} [SmallCategory S] (e : C ≌ S) : EssentiallySmall.{w} C

Full source

/-- Constructor for `EssentiallySmall C` from an explicit small category witness. -/
theorem EssentiallySmall.mk' {C : Type u} [Category.{v} C] {S : Type w} [SmallCategory S]
    (e : C ≌ S) : EssentiallySmall.{w} C :=
  ⟨⟨S, _, ⟨e⟩⟩⟩

Construction of Essentially Small Category via Equivalence

Informal description

Given a category $C$ and a small category $S$ (i.e., $S$ is of type $\text{Type } w$), if there exists an equivalence of categories $e \colon C \simeq S$, then $C$ is essentially small with respect to the universe $w$.

CategoryTheory.SmallModel definition

(C : Type u) [Category.{v} C] [EssentiallySmall.{w} C] : Type w

Full source

/-- An arbitrarily chosen small model for an essentially small category.
-/
@[pp_with_univ]
def SmallModel (C : Type u) [Category.{v} C] [EssentiallySmall.{w} C] : Type w :=
  Classical.choose (@EssentiallySmall.equiv_smallCategory C _ _)

Small model of an essentially small category

Informal description

Given an essentially small category $ C $ (with respect to universe $ w $), the structure `SmallModel C` provides an arbitrarily chosen small category (of type $ \text{Type } w $) that is equivalent to $ C $.

CategoryTheory.smallCategorySmallModel instance

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

Full source

noncomputable instance smallCategorySmallModel (C : Type u) [Category.{v} C]
    [EssentiallySmall.{w} C] : SmallCategory (SmallModel C) :=
  Classical.choose (Classical.choose_spec (@EssentiallySmall.equiv_smallCategory C _ _))

Small Category Structure on the Small Model of an Essentially Small Category

Informal description

For any essentially small category $C$ (with respect to universe $w$), its small model $\text{SmallModel}\, C$ carries a canonical small category structure.

CategoryTheory.equivSmallModel definition

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

Full source

/-- The (noncomputable) categorical equivalence between
an essentially small category and its small model.
-/
noncomputable def equivSmallModel (C : Type u) [Category.{v} C] [EssentiallySmall.{w} C] :
    C ≌ SmallModel C :=
  Nonempty.some
    (Classical.choose_spec (Classical.choose_spec (@EssentiallySmall.equiv_smallCategory C _ _)))

Equivalence between an essentially small category and its small model

Informal description

For any essentially small category $ C $ (with respect to universe $ w $), there exists a (noncomputable) categorical equivalence between $ C $ and its small model $\text{SmallModel}\, C$.

CategoryTheory.instEssentiallySmallOpposite instance

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

Full source

instance (C : Type u) [Category.{v} C] [EssentiallySmall.{w} C] : EssentiallySmall.{w} Cᵒᵖ :=
  EssentiallySmall.mk' (equivSmallModel C).op

Essential Smallness of Opposite Categories

Informal description

For any essentially small category $C$ (with respect to universe $w$), its opposite category $C^{\mathrm{op}}$ is also essentially small with respect to $w$.

CategoryTheory.essentiallySmall_congr theorem

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

Full source

theorem essentiallySmall_congr {C : Type u} [Category.{v} C] {D : Type u'} [Category.{v'} D]
    (e : C ≌ D) : EssentiallySmallEssentiallySmall.{w} C ↔ EssentiallySmall.{w} D := by
  fconstructor
  · rintro ⟨S, 𝒮, ⟨f⟩⟩
    exact EssentiallySmall.mk' (e.symm.trans f)
  · rintro ⟨S, 𝒮, ⟨f⟩⟩
    exact EssentiallySmall.mk' (e.trans f)

Essential Smallness is Preserved by Equivalence of Categories

Informal description

Let $C$ and $D$ be categories (with objects in universes $u$ and $u'$ respectively, and morphisms in universes $v$ and $v'$ respectively). Given an equivalence of categories $e \colon C \simeq D$, the category $C$ is essentially small with respect to universe $w$ if and only if $D$ is essentially small with respect to $w$.

CategoryTheory.Discrete.essentiallySmallOfSmall theorem

{α : Type u} [Small.{w} α] : EssentiallySmall.{w} (Discrete α)

Full source

theorem Discrete.essentiallySmallOfSmall {α : Type u} [Small.{w} α] :
    EssentiallySmall.{w} (Discrete α) :=
  ⟨⟨Discrete (Shrink α), ⟨inferInstance, ⟨Discrete.equivalence (equivShrink _)⟩⟩⟩⟩

Essential Smallness of Discrete Categories from Small Types

Informal description

For any type $\alpha$ in universe $u$, if $\alpha$ is $w$-small (i.e., there exists an equivalence between $\alpha$ and a type in universe $w$), then the discrete category on $\alpha$ is $w$-essentially small.

CategoryTheory.essentiallySmallSelf theorem

: EssentiallySmall.{max w v u} C

Full source

theorem essentiallySmallSelf : EssentiallySmall.{max w v u} C :=
  EssentiallySmall.mk' (AsSmall.equiv : C ≌ AsSmall.{w} C)

Essential Smallness of a Category in the Maximum Universe

Informal description

For any category $C$ with objects in universe $u$ and morphisms in universe $v$, $C$ is essentially small with respect to the universe $\max(w, v, u)$.

CategoryTheory.LocallySmall structure

(C : Type u) [Category.{v} C]

Full source

/-- 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.
-/
@[pp_with_univ]
class LocallySmall (C : Type u) [Category.{v} C] : Prop where
  /-- A locally small category has small hom-types. -/
  hom_small : ∀ X Y : C, Small.{w} (X ⟶ Y) := by infer_instance

Locally small category

Informal description

A category $\mathcal{C}$ is called $w$-locally small if for every pair of objects $X, Y$ in $\mathcal{C}$, the hom-set $\text{Hom}(X, Y)$ is $w$-small (i.e., there exists a bijection between $\text{Hom}(X, Y)$ and a type in the universe $w$).

CategoryTheory.instSmallHomOfLocallySmall instance

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

Full source

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

Hom-sets in Locally Small Categories are Small

Informal description

For any locally small category $\mathcal{C}$ (with respect to universe $w$) and objects $X, Y$ in $\mathcal{C}$, the hom-set $\text{Hom}(X, Y)$ is $w$-small.

CategoryTheory.instLocallySmallOpposite instance

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

Full source

instance (C : Type u) [Category.{v} C] [LocallySmall.{w} C] : LocallySmall.{w} Cᵒᵖ where
  hom_small X Y := small_of_injective (opEquiv X Y).injective

Opposite Category Preserves Local Smallness

Informal description

For any locally small category $\mathcal{C}$ (with respect to universe $w$), its opposite category $\mathcal{C}^\mathrm{op}$ is also $w$-locally small.

CategoryTheory.locallySmall_of_faithful theorem

 {C : Type u} [Category.{v} C] {D : Type u'} [Category.{v'} D] (F : C ⥤ D) [F.Faithful] [LocallySmall.{w} D] :
  LocallySmall.{w} C

Full source

theorem locallySmall_of_faithful {C : Type u} [Category.{v} C] {D : Type u'} [Category.{v'} D]
    (F : C ⥤ D) [F.Faithful] [LocallySmall.{w} D] : LocallySmall.{w} C where
  hom_small {_ _} := small_of_injective F.map_injective

Faithful Functor Preserves Local Smallness

Informal description

Let $\mathcal{C}$ and $\mathcal{D}$ be categories, and let $F : \mathcal{C} \to \mathcal{D}$ be a faithful functor. If $\mathcal{D}$ is $w$-locally small, then $\mathcal{C}$ is also $w$-locally small.

CategoryTheory.locallySmall_congr theorem

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

Full source

theorem locallySmall_congr {C : Type u} [Category.{v} C] {D : Type u'} [Category.{v'} D]
    (e : C ≌ D) : LocallySmallLocallySmall.{w} C ↔ LocallySmall.{w} D :=
  ⟨fun _ => locallySmall_of_faithful e.inverse, fun _ => locallySmall_of_faithful e.functor⟩

Equivalence of Categories Preserves Local Smallness

Informal description

Let $\mathcal{C}$ and $\mathcal{D}$ be categories, and let $e \colon \mathcal{C} \simeq \mathcal{D}$ be an equivalence of categories. Then $\mathcal{C}$ is $w$-locally small if and only if $\mathcal{D}$ is $w$-locally small. Here, $w$-locally small means that for every pair of objects $X, Y$ in the category, the hom-set $\text{Hom}(X, Y)$ is $w$-small (i.e., there exists a bijection between $\text{Hom}(X, Y)$ and a type in the universe $w$).

CategoryTheory.locallySmall_self instance

(C : Type u) [Category.{v} C] : LocallySmall.{v} C

Full source

instance (priority := 100) locallySmall_self (C : Type u) [Category.{v} C] :
    LocallySmall.{v} C where

Every Category is Locally Small in its Morphism Universe

Informal description

For any category $\mathcal{C}$ with objects in universe level $u$ and morphisms in universe level $v$, $\mathcal{C}$ is $v$-locally small. That is, for any two objects $X, Y$ in $\mathcal{C}$, the hom-set $\text{Hom}(X, Y)$ is $v$-small.

CategoryTheory.locallySmall_of_univLE instance

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

Full source

instance (priority := 100) locallySmall_of_univLE (C : Type u) [Category.{v} C] [UnivLEUnivLE.{v, w}] :
    LocallySmall.{w} C where

Local Smallness under Universe Level Constraint

Informal description

For any category $\mathcal{C}$ with objects in universe level $u$ and morphisms in universe level $v$, if the universe level $v$ is less than or equal to $w$ (denoted by $\text{UnivLE}\{v, w\}$), then $\mathcal{C}$ is $w$-locally small. That is, for any two objects $X, Y$ in $\mathcal{C}$, the hom-set $\text{Hom}(X, Y)$ is $w$-small.

CategoryTheory.locallySmall_max theorem

{C : Type u} [Category.{v} C] : LocallySmall.{max v w} C

Full source

theorem locallySmall_max {C : Type u} [Category.{v} C] : LocallySmall.{max v w} C where
  hom_small _ _ := small_max.{w} _

Local Smallness in Maximum Universe Level

Informal description

For any category $\mathcal{C}$ with objects in universe level $u$ and morphisms in universe level $v$, $\mathcal{C}$ is locally small with respect to the universe level $\max(v, w)$. That is, for any two objects $X, Y$ in $\mathcal{C}$, the hom-set $\text{Hom}(X, Y)$ is $\max(v, w)$-small.

CategoryTheory.locallySmall_of_essentiallySmall instance

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

Full source

instance (priority := 100) locallySmall_of_essentiallySmall (C : Type u) [Category.{v} C]
    [EssentiallySmall.{w} C] : LocallySmall.{w} C :=
  (locallySmall_congr (equivSmallModel C)).mpr (CategoryTheory.locallySmall_self _)

Essentially Small Categories are Locally Small

Informal description

For any essentially small category $\mathcal{C}$ (with respect to universe $w$), $\mathcal{C}$ is $w$-locally small. That is, for any two objects $X, Y$ in $\mathcal{C}$, the hom-set $\text{Hom}(X, Y)$ is $w$-small.

CategoryTheory.ShrinkHoms definition

(C : Type u)

Full source

/-- 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`.
-/
@[pp_with_univ]
def ShrinkHoms (C : Type u) :=
  C

Type alias for hom-shrinking in categories

Informal description

The type alias `ShrinkHoms C` is defined to be equal to `C`. When the category `C` is locally small with respect to a universe level `w`, this type alias will be equipped with a category structure in universe `w`.

CategoryTheory.ShrinkHoms.toShrinkHoms definition

{C' : Type*} (X : C') : ShrinkHoms C'

Full source

/-- Help the typechecker by explicitly translating from `C` to `ShrinkHoms C`. -/
def toShrinkHoms {C' : Type*} (X : C') : ShrinkHoms C' :=
  X

Inclusion into hom-shrunk category type

Informal description

The function maps an object $ X $ of a category $ C' $ to the corresponding object in the type alias `ShrinkHoms C'`, which is definitionally equal to $ X $.

CategoryTheory.ShrinkHoms.fromShrinkHoms definition

{C' : Type*} (X : ShrinkHoms C') : C'

Full source

/-- Help the typechecker by explicitly translating from `ShrinkHoms C` to `C`. -/
def fromShrinkHoms {C' : Type*} (X : ShrinkHoms C') : C' :=
  X

Inverse of hom-shrinking type alias

Informal description

The function maps an element of the type alias `ShrinkHoms C'` back to the original type `C'`. This is the inverse of the `toShrinkHoms` function, and satisfies the property that `fromShrinkHoms (toShrinkHoms X) = X` for any `X : C'`.

CategoryTheory.ShrinkHoms.to_from theorem

(X : C') : fromShrinkHoms (toShrinkHoms X) = X

Full source

@[simp]
theorem to_from (X : C') : fromShrinkHoms (toShrinkHoms X) = X :=
  rfl

Inverse Property of Hom-Shrinking Inclusion

Informal description

For any object $X$ in a category $C'$, the composition of the inclusion into the hom-shrunk category type followed by its inverse yields the original object, i.e., $\text{fromShrinkHoms}(\text{toShrinkHoms}(X)) = X$.

CategoryTheory.ShrinkHoms.from_to theorem

(X : ShrinkHoms C') : toShrinkHoms (fromShrinkHoms X) = X

Full source

@[simp]
theorem from_to (X : ShrinkHoms C') : toShrinkHoms (fromShrinkHoms X) = X :=
  rfl

Inverse Property of Hom-Shrinking Projection

Informal description

For any object $X$ in the hom-shrunk category type $\text{ShrinkHoms}(C')$, the composition of the inverse function followed by the inclusion function yields the original object, i.e., $\text{toShrinkHoms}(\text{fromShrinkHoms}(X)) = X$.

CategoryTheory.ShrinkHoms.instCategory instance

: Category.{w} (ShrinkHoms C)

Full source

@[simps]
noncomputable instance : Category.{w} (ShrinkHoms C) where
  Hom X Y := Shrink (fromShrinkHoms X ⟶ fromShrinkHoms Y)
  id X := equivShrink _ (𝟙 (fromShrinkHoms X))
  comp f g := equivShrink _ ((equivShrink _).symm f ≫ (equivShrink _).symm g)

Category Structure on Hom-Shrunk Type

Informal description

For any category $\mathcal{C}$, the type alias $\text{ShrinkHoms}(\mathcal{C})$ is equipped with a category structure in universe $w$.

CategoryTheory.ShrinkHoms.functor definition

: C ⥤ ShrinkHoms C

Full source

/-- Implementation of `ShrinkHoms.equivalence`. -/
@[simps]
noncomputable def functor : C ⥤ ShrinkHoms C where
  obj X := toShrinkHoms X
  map {X Y} f := equivShrink (X ⟶ Y) f

Functor to hom-shrunk category

Informal description

The functor maps an object $ X $ in the category $ \mathcal{C} $ to its corresponding object in the hom-shrunk type $ \text{ShrinkHoms}(\mathcal{C}) $, and a morphism $ f \in \text{Hom}(X, Y) $ to its image under the equivalence $ \text{equivShrink} $ on hom-sets.

CategoryTheory.ShrinkHoms.inverse definition

: ShrinkHoms C ⥤ C

Full source

/-- Implementation of `ShrinkHoms.equivalence`. -/
@[simps]
noncomputable def inverse : ShrinkHomsShrinkHoms C ⥤ C where
  obj X := fromShrinkHoms X
  map {X Y} f := (equivShrink (fromShrinkHoms X ⟶ fromShrinkHoms Y)).symm f

Inverse functor of hom-shrinking equivalence

Informal description

The functor maps an object $X$ in the hom-shrunk type $\text{ShrinkHoms}(\mathcal{C})$ back to its corresponding object in the original category $\mathcal{C}$, and a morphism $f$ in $\text{ShrinkHoms}(\mathcal{C})$ to its corresponding morphism in $\mathcal{C}$ via the inverse of the equivalence $\text{equivShrink}$ on hom-sets.

CategoryTheory.ShrinkHoms.equivalence definition

: C ≌ ShrinkHoms C

Full source

/-- The categorical equivalence between `C` and `ShrinkHoms C`, when `C` is locally small.
-/
@[simps]
noncomputable def equivalence : C ≌ ShrinkHoms C where
  functor := functor C
  inverse := inverse C
  unitIso := NatIso.ofComponents (fun _ ↦ Iso.refl _)
  counitIso := NatIso.ofComponents (fun _ ↦ Iso.refl _)

Equivalence between a category and its hom-shrunk version

Informal description

The categorical equivalence between a locally small category $\mathcal{C}$ and its hom-shrunk version $\text{ShrinkHoms}(\mathcal{C})$, consisting of: - A functor from $\mathcal{C}$ to $\text{ShrinkHoms}(\mathcal{C})$, - An inverse functor from $\text{ShrinkHoms}(\mathcal{C})$ back to $\mathcal{C}$, - Natural isomorphisms given by identity isomorphisms for both the unit and counit. This equivalence holds when $\mathcal{C}$ is locally small with respect to some universe level $w$.

CategoryTheory.ShrinkHoms.instIsEquivalenceFunctor instance

: (functor C).IsEquivalence

Full source

instance : (functor C).IsEquivalence := (equivalence C).isEquivalence_functor

Equivalence of Hom-Shrunk Category Functor

Informal description

The functor from a category $\mathcal{C}$ to its hom-shrunk version $\text{ShrinkHoms}(\mathcal{C})$ is an equivalence of categories.

CategoryTheory.ShrinkHoms.instIsEquivalenceInverse instance

: (inverse C).IsEquivalence

Full source

instance : (inverse C).IsEquivalence := (equivalence C).isEquivalence_inverse

Inverse Functor of Hom-Shrinking is an Equivalence

Informal description

The inverse functor of the hom-shrinking equivalence for a category $\mathcal{C}$ is an equivalence of categories. That is, the functor from $\text{ShrinkHoms}(\mathcal{C})$ back to $\mathcal{C}$ is full, faithful, and essentially surjective.

CategoryTheory.Shrink.instCategoryShrink instance

[Small.{w} C] : Category.{v} (Shrink.{w} C)

Full source

noncomputable instance [Small.{w} C] : Category.{v} (Shrink.{w} C) :=
  InducedCategory.category (equivShrink C).symm

Category Structure on a Small Representative of a Category

Informal description

For any category $C$ that is small with respect to a universe $w$, the type $\text{Shrink}\, C$ (a small representative of $C$) inherits a category structure in universe $v$.

CategoryTheory.Shrink.equivalence definition

[Small.{w} C] : C ≌ Shrink.{w} C

Full source

/-- The categorical equivalence between `C` and `Shrink C`, when `C` is small. -/
noncomputable def equivalence [Small.{w} C] : C ≌ Shrink.{w} C :=
  (Equivalence.induced _).symm

Equivalence between a category and its small representative

Informal description

Given a category $C$ that is small with respect to a universe $w$, there exists an equivalence of categories between $C$ and its small representative $\text{Shrink}\, C$. This equivalence is constructed by: 1. Using the induced category structure on $\text{Shrink}\, C$ via the bijection between $C$ and $\text{Shrink}\, C$ 2. Taking the symmetric equivalence of the induced equivalence between $\text{InducedCategory}\, C\, \text{shrinkEquiv}$ and $C$

CategoryTheory.Shrink.instLocallySmallShrink instance

[Small.{w'} C] [LocallySmall.{w} C] : LocallySmall.{w} (Shrink.{w'} C)

Full source

instance [Small.{w'} C] [LocallySmall.{w} C] :
    LocallySmall.{w} (Shrink.{w'} C) :=
  locallySmall_of_faithful.{w} (equivalence.{w'} C).inverse

Local Smallness of a Small Representative Category

Informal description

For any category $\mathcal{C}$ that is small with respect to a universe $w'$ and $w$-locally small, its small representative $\text{Shrink}\, \mathcal{C}$ is also $w$-locally small.

CategoryTheory.essentiallySmall_iff theorem

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

Full source

/-- 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 essentiallySmall_iff (C : Type u) [Category.{v} C] :
    EssentiallySmallEssentiallySmall.{w} C ↔ Small.{w} (Skeleton C) ∧ LocallySmall.{w} C := by
  -- This theorem is the only bit of real work in this file.
  fconstructor
  · intro h
    fconstructor
    · rcases h with ⟨S, 𝒮, ⟨e⟩⟩
      refine ⟨⟨Skeleton S, ⟨?_⟩⟩⟩
      exact e.skeletonEquiv
    · infer_instance
  · rintro ⟨⟨S, ⟨e⟩⟩, L⟩
    let e' := (ShrinkHoms.equivalence C).skeletonEquiv.symm
    letI : Category S := InducedCategory.category (e'.trans e).symm
    refine ⟨⟨S, this, ⟨?_⟩⟩⟩
    refine (ShrinkHoms.equivalence C).trans <|
      (skeletonEquivalence (ShrinkHoms C)).symm.trans
        ((inducedFunctor (e'.trans e).symm).asEquivalence.symm)

Characterization of Essentially Small Categories via Skeletons and Local Smallness

Informal description

A category $\mathcal{C}$ is $w$-essentially small if and only if its skeleton (the type of isomorphism classes of objects) is $w$-small and $\mathcal{C}$ is $w$-locally small (i.e., all hom-sets are $w$-small).

CategoryTheory.essentiallySmall_of_small_of_locallySmall theorem

[Small.{w} C] [LocallySmall.{w} C] : EssentiallySmall.{w} C

Full source

theorem essentiallySmall_of_small_of_locallySmall [Small.{w} C] [LocallySmall.{w} C] :
    EssentiallySmall.{w} C :=
  (essentiallySmall_iff C).2 ⟨small_of_surjective Quotient.exists_rep, by infer_instance⟩

Essential Smallness from Smallness and Local Smallness

Informal description

If a category $\mathcal{C}$ is $w$-small (i.e., the type of its objects is $w$-small) and $w$-locally small (i.e., all hom-sets are $w$-small), then $\mathcal{C}$ is $w$-essentially small.

CategoryTheory.locallySmall_fullSubcategory instance

[LocallySmall.{w} C] (P : ObjectProperty C) : LocallySmall.{w} P.FullSubcategory

Full source

instance locallySmall_fullSubcategory [LocallySmall.{w} C] (P : ObjectProperty C) :
    LocallySmall.{w} P.FullSubcategory :=
  locallySmall_of_faithful <| P.ι

Local Smallness of Full Subcategories

Informal description

For any locally small category $\mathcal{C}$ with respect to universe $w$ and any property $P$ on the objects of $\mathcal{C}$, the full subcategory of $\mathcal{C}$ determined by $P$ is also locally small with respect to $w$.

CategoryTheory.essentiallySmall_fullSubcategory_mem instance

(s : Set C) [Small.{w} s] [LocallySmall.{w} C] : EssentiallySmall.{w} (ObjectProperty.FullSubcategory (· ∈ s))

Full source

instance essentiallySmall_fullSubcategory_mem (s : Set C) [Small.{w} s] [LocallySmall.{w} C] :
    EssentiallySmall.{w} (ObjectProperty.FullSubcategory (· ∈ s)) :=
  suffices Small.{w} (ObjectProperty.FullSubcategory (· ∈ s)) from
    essentiallySmall_of_small_of_locallySmall _
  small_of_injective (f := fun x => (⟨x.1, x.2⟩ : s)) (by aesop_cat)

Essential Smallness of Full Subcategories Defined by Small Sets of Objects

Informal description

For any category $\mathcal{C}$ and a subset $s$ of its objects, if $s$ is $w$-small and $\mathcal{C}$ is $w$-locally small, then the full subcategory of $\mathcal{C}$ consisting of objects in $s$ is $w$-essentially small.

CategoryTheory.locallySmall_of_thin instance

{C : Type u} [Category.{v} C] [Quiver.IsThin C] : LocallySmall.{w} C

Full source

/-- Any thin category is locally small.
-/
instance (priority := 100) locallySmall_of_thin {C : Type u} [Category.{v} C] [Quiver.IsThin C] :
    LocallySmall.{w} C where

Local Smallness of Thin Categories

Informal description

Every thin category is locally small. That is, for any thin category $\mathcal{C}$ (where there is at most one morphism between any two objects), the hom-sets $\text{Hom}(X, Y)$ are small for all objects $X, Y$ in $\mathcal{C}$.

CategoryTheory.essentiallySmall_iff_of_thin theorem

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

Full source

/--
A thin category is essentially small if and only if the underlying type of its skeleton is small.
-/
theorem essentiallySmall_iff_of_thin {C : Type u} [Category.{v} C] [Quiver.IsThin C] :
    EssentiallySmallEssentiallySmall.{w} C ↔ Small.{w} (Skeleton C) := by
  simp [essentiallySmall_iff, CategoryTheory.locallySmall_of_thin]

Equivalence of Essential Smallness and Smallness of Skeleton for Thin Categories

Informal description

For a thin category $C$ (i.e., a category where there is at most one morphism between any two objects), the following are equivalent: 1. $C$ is essentially small with respect to universe $w$. 2. The skeleton of $C$ (a category equivalent to $C$ where isomorphic objects are equal) is small with respect to universe $w$.

CategoryTheory.instSmallDiscrete instance

[Small.{w} C] : Small.{w} (Discrete C)

Full source

instance [Small.{w} C] : Small.{w} (Discrete C) := small_map discreteEquiv

Smallness of Discrete Categories for Small Types

Informal description

For any type $C$ that is small with respect to universe level $w$, the discrete category on $C$ is also small with respect to $w$.