Finally small filtered categories

In this file, we show that if C is a filtered finally small category that is locally small, there exists a final functor D ⥤ C from a small filtered category. The dual result is also obtained.

theorem CategoryTheory.FinallySmall.exists_of_isFiltered (C : Type u) [Category.{v, u} C] [IsFiltered C] [LocallySmall.{w, v, u} C] [FinallySmall C] : ∃ (D : Type w) (x : SmallCategory D) (_ : IsFiltered D) (F : Functor D C), F.Final

def CategoryTheory.FinallySmall.FilteredFinalModel (C : Type u) [Category.{v, u} C] [IsFiltered C] [LocallySmall.{w, v, u} C] [FinallySmall C] : Type w

If C is a locally small filtered finally small category, this is a small filtered category, equipped with a final functor to C (see fromFilteredFinalModel).

Equations

• CategoryTheory.FinallySmall.FilteredFinalModel C = ⋯.choose

@[implicit_reducible]

noncomputable instance CategoryTheory.FinallySmall.instCategoryFilteredFinalModel (C : Type u) [Category.{v, u} C] [IsFiltered C] [LocallySmall.{w, v, u} C] [FinallySmall C] : Category.{w, w} (FilteredFinalModel C)

Equations

• CategoryTheory.FinallySmall.instCategoryFilteredFinalModel C = ⋯.choose

instance CategoryTheory.FinallySmall.instIsFilteredFilteredFinalModel (C : Type u) [Category.{v, u} C] [IsFiltered C] [LocallySmall.{w, v, u} C] [FinallySmall C] : IsFiltered (FilteredFinalModel C)

noncomputable def CategoryTheory.FinallySmall.fromFilteredFinalModel (C : Type u) [Category.{v, u} C] [IsFiltered C] [LocallySmall.{w, v, u} C] [FinallySmall C] : Functor (FilteredFinalModel C) C

If C is a locally small filtered finally small category, this is a final functor from a small filtered category.

Equations

• CategoryTheory.FinallySmall.fromFilteredFinalModel C = ⋯.choose

instance CategoryTheory.FinallySmall.instFinalFilteredFinalModelFromFilteredFinalModel (C : Type u) [Category.{v, u} C] [IsFiltered C] [LocallySmall.{w, v, u} C] [FinallySmall C] : (fromFilteredFinalModel C).Final

theorem CategoryTheory.FinallySmall.preservesColimitsOfShape_of_isFiltered (C : Type u) [Category.{v, u} C] [IsFiltered C] [LocallySmall.{w, v, u} C] [FinallySmall C] {D : Type u_1} {E : Type u_2} [Category.{v_1, u_1} D] [Category.{v_2, u_2} E] (F : Functor D E) [Limits.PreservesFilteredColimitsOfSize.{w, w, v_1, v_2, u_1, u_2} F] : Limits.PreservesColimitsOfShape C F

theorem CategoryTheory.InitiallySmall.exists_of_isCofiltered (C : Type u) [Category.{v, u} C] [IsCofiltered C] [LocallySmall.{w, v, u} C] [InitiallySmall C] : ∃ (D : Type w) (x : SmallCategory D) (_ : IsCofiltered D) (F : Functor D C), F.Initial

def CategoryTheory.InitiallySmall.CofilteredInitialModel (C : Type u) [Category.{v, u} C] [IsCofiltered C] [LocallySmall.{w, v, u} C] [InitiallySmall C] : Type w

If C is a locally small cofiltered initially small category, this is a small cofiltered category, equipped with an initial functor to C (see fromCofilteredInitialModel).

Equations

• CategoryTheory.InitiallySmall.CofilteredInitialModel C = ⋯.choose

@[implicit_reducible]

noncomputable instance CategoryTheory.InitiallySmall.instCategoryCofilteredInitialModel (C : Type u) [Category.{v, u} C] [IsCofiltered C] [LocallySmall.{w, v, u} C] [InitiallySmall C] : Category.{w, w} (CofilteredInitialModel C)

Equations

• CategoryTheory.InitiallySmall.instCategoryCofilteredInitialModel C = ⋯.choose

instance CategoryTheory.InitiallySmall.instIsCofilteredCofilteredInitialModel (C : Type u) [Category.{v, u} C] [IsCofiltered C] [LocallySmall.{w, v, u} C] [InitiallySmall C] : IsCofiltered (CofilteredInitialModel C)

noncomputable def CategoryTheory.InitiallySmall.fromCofilteredInitialModel (C : Type u) [Category.{v, u} C] [IsCofiltered C] [LocallySmall.{w, v, u} C] [InitiallySmall C] : Functor (CofilteredInitialModel C) C

If C is a locally small cofiltered initially small category, this is an initial functor from a small cofiltered category.

Equations

• CategoryTheory.InitiallySmall.fromCofilteredInitialModel C = ⋯.choose

instance CategoryTheory.InitiallySmall.instInitialCofilteredInitialModelFromCofilteredInitialModel (C : Type u) [Category.{v, u} C] [IsCofiltered C] [LocallySmall.{w, v, u} C] [InitiallySmall C] : (fromCofilteredInitialModel C).Initial