# 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.

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

• final_smallCategory : ∃ (S : Type w) (x : ) (F : ), F.Final

There is a final functor from a small category.

Instances
theorem CategoryTheory.FinallySmall.final_smallCategory {J : Type u} [self : ] :
∃ (S : Type w) (x : ) (F : ), F.Final

There is a final functor from a small category.

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

Constructor for FinallySmall C from an explicit small category witness.

An arbitrarily chosen small model for a finally small category.

Equations
Instances For
noncomputable instance CategoryTheory.smallCategoryFinalModel (J : Type u) :
Equations
noncomputable def CategoryTheory.fromFinalModel (J : Type u) :

An arbitrarily chosen final functor FinalModel J ⥤ J.

Equations
Instances For
instance CategoryTheory.final_fromFinalModel (J : Type u) :
.Final
Equations
• =
theorem CategoryTheory.finallySmall_of_final_of_finallySmall {J : Type u} {K : Type u₁} [] (F : ) [F.Final] :
theorem CategoryTheory.finallySmall_of_final_of_essentiallySmall {J : Type u} {K : Type u₁} [] (F : ) [F.Final] [] :

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

• initial_smallCategory : ∃ (S : Type w) (x : ) (F : ), F.Initial

There is an initial functor from a small category.

Instances
theorem CategoryTheory.InitiallySmall.initial_smallCategory {J : Type u} [self : ] :
∃ (S : Type w) (x : ) (F : ), F.Initial

There is an initial functor from a small category.

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

Constructor for InitialSmall C from an explicit small category witness.

An arbitrarily chosen small model for an initially small category.

Equations
Instances For
noncomputable instance CategoryTheory.smallCategoryInitialModel (J : Type u) :
Equations
noncomputable def CategoryTheory.fromInitialModel (J : Type u) :

An arbitrarily chosen initial functor InitialModel J ⥤ J.

Equations
Instances For
Equations
• =
theorem CategoryTheory.initiallySmall_of_initial_of_initiallySmall {J : Type u} {K : Type u₁} [] (F : ) [F.Initial] :
theorem CategoryTheory.initiallySmall_of_initial_of_essentiallySmall {J : Type u} {K : Type u₁} [] (F : ) [F.Initial] [] :
theorem CategoryTheory.FinallySmall.exists_small_weakly_terminal_set (J : Type u) :
∃ (s : Set J) (_ : ), ∀ (i : J), js, 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} (s : Set J) [] (hs : ∀ (i : J), js, Nonempty (i j)) :
theorem CategoryTheory.finallySmall_iff_exists_small_weakly_terminal_set (J : Type u) :
∃ (s : Set J) (_ : ), ∀ (i : J), js, Nonempty (i j)
theorem CategoryTheory.InitiallySmall.exists_small_weakly_initial_set (J : Type u) :
∃ (s : Set J) (_ : ), ∀ (i : J), js, 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} (s : Set J) [] (hs : ∀ (i : J), js, Nonempty (j i)) :
theorem CategoryTheory.initiallySmall_iff_exists_small_weakly_initial_set (J : Type u) :
∃ (s : Set J) (_ : ), ∀ (i : J), js, Nonempty (j i)