Finally small categories

A category given by (J : Type u) [Category.{v} J] is w-finally small if there exists a FinalModel J : Type w equipped with [SmallCategory (FinalModel J)] and a final functor FinalModel J ⥤ J.

This means that if a category C has colimits of size w and J is w-finally small, then C has colimits of shape J. In this way, the notion of "finally small" can be seen of a generalization of the notion of "essentially small" for indexing categories of colimits.

Dually, we have a notion of initially small category.

We show that a finally small category admits a small weakly terminal set, i.e., a small set s of objects such that from every object there a morphism to a member of s. We also show that the converse holds if J is filtered.

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

A category is FinallySmall.{w} if there is a final functor from a w-small category.

• final_smallCategory : ∃ (S : Type w) (x : CategoryTheory.SmallCategory S) (F : CategoryTheory.Functor S J), CategoryTheory.Functor.Final F

  There is a final functor from a small category.

theorem CategoryTheory.FinallySmall.mk' {J : Type u} [CategoryTheory.Category.{v, u} J] {S : Type w} [CategoryTheory.SmallCategory S] (F : CategoryTheory.Functor S J) [CategoryTheory.Functor.Final F] : CategoryTheory.FinallySmall J

Constructor for FinallySmall C from an explicit small category witness.

def CategoryTheory.FinalModel (J : Type u) [CategoryTheory.Category.{v, u} J] [CategoryTheory.FinallySmall J] : Type w

An arbitrarily chosen small model for a finally small category.

Equations

• CategoryTheory.FinalModel J = Classical.choose ⋯

noncomputable instance CategoryTheory.smallCategoryFinalModel (J : Type u) [CategoryTheory.Category.{v, u} J] [CategoryTheory.FinallySmall J] : CategoryTheory.SmallCategory (CategoryTheory.FinalModel J)

Equations

• CategoryTheory.smallCategoryFinalModel J = Classical.choose ⋯

noncomputable def CategoryTheory.fromFinalModel (J : Type u) [CategoryTheory.Category.{v, u} J] [CategoryTheory.FinallySmall J] : CategoryTheory.Functor (CategoryTheory.FinalModel J) J

An arbitrarily chosen final functor FinalModel J ⥤ J.

Equations

• CategoryTheory.fromFinalModel J = Classical.choose ⋯

instance CategoryTheory.final_fromFinalModel (J : Type u) [CategoryTheory.Category.{v, u} J] [CategoryTheory.FinallySmall J] : CategoryTheory.Functor.Final (CategoryTheory.fromFinalModel J)

Equations

• ⋯ = ⋯

theorem CategoryTheory.finallySmall_of_essentiallySmall (J : Type u) [CategoryTheory.Category.{v, u} J] [CategoryTheory.EssentiallySmall.{w, v, u} J] : CategoryTheory.FinallySmall J

theorem CategoryTheory.finallySmall_of_final_of_finallySmall {J : Type u} [CategoryTheory.Category.{v, u} J] {K : Type u₁} [CategoryTheory.Category.{v₁, u₁} K] (F : CategoryTheory.Functor K J) [CategoryTheory.Functor.Final F] [CategoryTheory.FinallySmall K] : CategoryTheory.FinallySmall J

theorem CategoryTheory.finallySmall_of_final_of_essentiallySmall {J : Type u} [CategoryTheory.Category.{v, u} J] {K : Type u₁} [CategoryTheory.Category.{v₁, u₁} K] (F : CategoryTheory.Functor K J) [CategoryTheory.Functor.Final F] [CategoryTheory.EssentiallySmall.{w, v₁, u₁} K] : CategoryTheory.FinallySmall J

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

A category is InitiallySmall.{w} if there is an initial functor from a w-small category.

• initial_smallCategory : ∃ (S : Type w) (x : CategoryTheory.SmallCategory S) (F : CategoryTheory.Functor S J), CategoryTheory.Functor.Initial F

  There is an initial functor from a small category.

theorem CategoryTheory.InitiallySmall.mk' {J : Type u} [CategoryTheory.Category.{v, u} J] {S : Type w} [CategoryTheory.SmallCategory S] (F : CategoryTheory.Functor S J) [CategoryTheory.Functor.Initial F] : CategoryTheory.InitiallySmall J

Constructor for InitialSmall C from an explicit small category witness.

def CategoryTheory.InitialModel (J : Type u) [CategoryTheory.Category.{v, u} J] [CategoryTheory.InitiallySmall J] : Type w

An arbitrarily chosen small model for an initially small category.

Equations

• CategoryTheory.InitialModel J = Classical.choose ⋯

noncomputable instance CategoryTheory.smallCategoryInitialModel (J : Type u) [CategoryTheory.Category.{v, u} J] [CategoryTheory.InitiallySmall J] : CategoryTheory.SmallCategory (CategoryTheory.InitialModel J)

Equations

• CategoryTheory.smallCategoryInitialModel J = Classical.choose ⋯

noncomputable def CategoryTheory.fromInitialModel (J : Type u) [CategoryTheory.Category.{v, u} J] [CategoryTheory.InitiallySmall J] : CategoryTheory.Functor (CategoryTheory.InitialModel J) J

An arbitrarily chosen initial functor InitialModel J ⥤ J.

Equations

• CategoryTheory.fromInitialModel J = Classical.choose ⋯

instance CategoryTheory.initial_fromInitialModel (J : Type u) [CategoryTheory.Category.{v, u} J] [CategoryTheory.InitiallySmall J] : CategoryTheory.Functor.Initial (CategoryTheory.fromInitialModel J)

Equations

• ⋯ = ⋯

theorem CategoryTheory.initiallySmall_of_essentiallySmall (J : Type u) [CategoryTheory.Category.{v, u} J] [CategoryTheory.EssentiallySmall.{w, v, u} J] : CategoryTheory.InitiallySmall J

theorem CategoryTheory.initiallySmall_of_initial_of_initiallySmall {J : Type u} [CategoryTheory.Category.{v, u} J] {K : Type u₁} [CategoryTheory.Category.{v₁, u₁} K] (F : CategoryTheory.Functor K J) [CategoryTheory.Functor.Initial F] [CategoryTheory.InitiallySmall K] : CategoryTheory.InitiallySmall J

theorem CategoryTheory.initiallySmall_of_initial_of_essentiallySmall {J : Type u} [CategoryTheory.Category.{v, u} J] {K : Type u₁} [CategoryTheory.Category.{v₁, u₁} K] (F : CategoryTheory.Functor K J) [CategoryTheory.Functor.Initial F] [CategoryTheory.EssentiallySmall.{w, v₁, u₁} K] : CategoryTheory.InitiallySmall J

theorem CategoryTheory.FinallySmall.exists_small_weakly_terminal_set (J : Type u) [CategoryTheory.Category.{v, u} J] [CategoryTheory.FinallySmall J] : ∃ (s : Set J) (_ : Small.{w, u} ↑s), ∀ (i : J), ∃ j ∈ s, Nonempty (i ⟶ j)

The converse is true if J is filtered, see finallySmall_of_small_weakly_terminal_set.

theorem CategoryTheory.finallySmall_of_small_weakly_terminal_set {J : Type u} [CategoryTheory.Category.{v, u} J] [CategoryTheory.IsFilteredOrEmpty J] (s : Set J) [Small.{v, u} ↑s] (hs : ∀ (i : J), ∃ j ∈ s, Nonempty (i ⟶ j)) : CategoryTheory.FinallySmall J

theorem CategoryTheory.finallySmall_iff_exists_small_weakly_terminal_set (J : Type u) [CategoryTheory.Category.{v, u} J] [CategoryTheory.IsFilteredOrEmpty J] : CategoryTheory.FinallySmall J ↔ ∃ (s : Set J) (_ : Small.{v, u} ↑s), ∀ (i : J), ∃ j ∈ s, Nonempty (i ⟶ j)

theorem CategoryTheory.InitiallySmall.exists_small_weakly_initial_set (J : Type u) [CategoryTheory.Category.{v, u} J] [CategoryTheory.InitiallySmall J] : ∃ (s : Set J) (_ : Small.{w, u} ↑s), ∀ (i : J), ∃ j ∈ s, Nonempty (j ⟶ i)

The converse is true if J is cofiltered, see intiallySmall_of_small_weakly_initial_set.

theorem CategoryTheory.initiallySmall_of_small_weakly_initial_set {J : Type u} [CategoryTheory.Category.{v, u} J] [CategoryTheory.IsCofilteredOrEmpty J] (s : Set J) [Small.{v, u} ↑s] (hs : ∀ (i : J), ∃ j ∈ s, Nonempty (j ⟶ i)) : CategoryTheory.InitiallySmall J

theorem CategoryTheory.initiallySmall_iff_exists_small_weakly_initial_set (J : Type u) [CategoryTheory.Category.{v, u} J] [CategoryTheory.IsCofilteredOrEmpty J] : CategoryTheory.InitiallySmall J ↔ ∃ (s : Set J) (_ : Small.{v, u} ↑s), ∀ (i : J), ∃ j ∈ s, Nonempty (j ⟶ i)

theorem CategoryTheory.Limits.hasColimitsOfShape_of_finallySmall (J : Type u) [CategoryTheory.Category.{v, u} J] [CategoryTheory.FinallySmall J] (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v₁, u₁} C] : CategoryTheory.Limits.HasColimitsOfShape J C

theorem CategoryTheory.Limits.hasLimitsOfShape_of_initiallySmall (J : Type u) [CategoryTheory.Category.{v, u} J] [CategoryTheory.InitiallySmall J] (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasLimitsOfSize.{w, w, v₁, u₁} C] : CategoryTheory.Limits.HasLimitsOfShape J C