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 as 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 is a morphism to a member of s. We also show that the converse holds if J is filtered.

class CategoryTheory.FinallySmall (J : Type u) [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 : SmallCategory S) (F : Functor S J), F.Final

  There is a final functor from a small category.

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

Constructor for FinallySmall C from an explicit small category witness.

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

An arbitrarily chosen small model for a finally small category.

@[implicit_reducible]

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

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

An arbitrarily chosen final functor FinalModel J ⥤ J.

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

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

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

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

instance CategoryTheory.instFinallySmallOfHasTerminal {J : Type u} [Category.{v, u} J] [Limits.HasTerminal J] : FinallySmall J

instance CategoryTheory.instFinallySmallProd {J : Type u} [Category.{v, u} J] {J' : Type u_1} [Category.{v_1, u_1} J'] [FinallySmall J] [FinallySmall J'] : FinallySmall (J × J')

class CategoryTheory.InitiallySmall (J : Type u) [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 : SmallCategory S) (F : Functor S J), F.Initial

  There is an initial functor from a small category.

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

Constructor for InitialSmall C from an explicit small category witness.

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

An arbitrarily chosen small model for an initially small category.

@[implicit_reducible]

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

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

An arbitrarily chosen initial functor InitialModel J ⥤ J.

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

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

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

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

instance CategoryTheory.instInitiallySmallOfHasInitial {J : Type u} [Category.{v, u} J] [Limits.HasInitial J] : InitiallySmall J

instance CategoryTheory.instInitiallySmallOverOfLocallySmall {J : Type u} [Category.{v, u} J] [LocallySmall.{w, v, u} J] [InitiallySmall J] (X : J) : InitiallySmall (Over X)

instance CategoryTheory.instInitiallySmallProd {J : Type u} [Category.{v, u} J] {J' : Type u_1} [Category.{v_1, u_1} J'] [InitiallySmall J] [InitiallySmall J'] : InitiallySmall (J × J')

instance CategoryTheory.instFinallySmallOppositeOfInitiallySmall {J : Type u} [Category.{v, u} J] [InitiallySmall J] : FinallySmall Jᵒᵖ

instance CategoryTheory.instInitiallySmallOppositeOfFinallySmall {J : Type u} [Category.{v, u} J] [FinallySmall J] : InitiallySmall Jᵒᵖ

theorem CategoryTheory.FinallySmall.exists_small_weakly_terminal_set (J : Type u) [Category.{v, u} J] [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} [Category.{v, u} J] [IsFilteredOrEmpty J] (s : Set J) [Small.{v, u} ↑s] (hs : ∀ (i : J), ∃ j ∈ s, Nonempty (i ⟶ j)) : FinallySmall J

theorem CategoryTheory.finallySmall_iff_exists_small_weakly_terminal_set (J : Type u) [Category.{v, u} J] [IsFilteredOrEmpty J] : 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) [Category.{v, u} J] [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 initiallySmall_of_small_weakly_initial_set.

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

theorem CategoryTheory.initiallySmall_iff_exists_small_weakly_initial_set (J : Type u) [Category.{v, u} J] [IsCofilteredOrEmpty J] : 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) [Category.{v, u} J] [FinallySmall J] (C : Type u₁) [Category.{v₁, u₁} C] [HasColimitsOfSize.{w, w, v₁, u₁} C] : HasColimitsOfShape J C

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