Filtered categories and limits

In this file , we show that C is filtered if and only if for every functor F : J ⥤ C from a finite category there is some X : C such that lim Hom(F·, X) is nonempty.

Furthermore, we define the type classes HasCofilteredLimitsOfSize and HasFilteredColimitsOfSize.

theorem CategoryTheory.IsFiltered.iff_nonempty_limit {C : Type u} [Category.{v, u} C] : IsFiltered C ↔ ∀ {J : Type v} [inst : SmallCategory J] [FinCategory J] (F : Functor J C), ∃ (X : C), Nonempty (Limits.limit (F.op.comp (yoneda.obj X)))

C is filtered if and only if for every functor F : J ⥤ C from a finite category there is some X : C such that lim Hom(F·, X) is nonempty.

Lemma 3.1.2 of [KS06]

theorem CategoryTheory.IsCofiltered.iff_nonempty_limit {C : Type u} [Category.{v, u} C] : IsCofiltered C ↔ ∀ {J : Type v} [inst : SmallCategory J] [FinCategory J] (F : Functor J C), ∃ (X : C), Nonempty (Limits.limit (F.comp (coyoneda.obj (Opposite.op X))))

C is cofiltered if and only if for every functor F : J ⥤ C from a finite category there is some X : C such that lim Hom(X, F·) is nonempty.

class CategoryTheory.Limits.HasCofilteredLimitsOfSize (C : Type u) [Category.{v, u} C] : Prop

Class for having all cofiltered limits of a given size.

• HasLimitsOfShape (I : Type w) [Category.{w', w} I] [IsCofiltered I] : Limits.HasLimitsOfShape I C

  For all filtered types of size w, we have limits

class CategoryTheory.Limits.HasFilteredColimitsOfSize (C : Type u) [Category.{v, u} C] : Prop

Class for having all filtered colimits of a given size.

• HasColimitsOfShape (I : Type w) [Category.{w', w} I] [IsFiltered I] : Limits.HasColimitsOfShape I C

  For all filtered types of a size w, we have colimits

@[reducible, inline]

abbrev CategoryTheory.Limits.HasCofilteredLimits (C : Type u) [Category.{v, u} C] : Prop

Class for having cofiltered limits.

Equations

• CategoryTheory.Limits.HasCofilteredLimits C = CategoryTheory.Limits.HasCofilteredLimitsOfSize.{?u.11, ?u.11, ?u.11, ?u.10} C

@[reducible, inline]

abbrev CategoryTheory.Limits.HasFilteredColimits (C : Type u) [Category.{v, u} C] : Prop

Class for having filtered colimits.

Equations

• CategoryTheory.Limits.HasFilteredColimits C = CategoryTheory.Limits.HasFilteredColimitsOfSize.{?u.11, ?u.11, ?u.11, ?u.10} C

@[instance 100]

instance CategoryTheory.Limits.hasFilteredColimitsOfSize_of_hasColimitsOfSize {C : Type u} [Category.{v, u} C] [HasColimitsOfSize.{w', w, v, u} C] : HasFilteredColimitsOfSize.{w', w, v, u} C

@[instance 100]

instance CategoryTheory.Limits.hasCofilteredLimitsOfSize_of_hasLimitsOfSize {C : Type u} [Category.{v, u} C] [HasLimitsOfSize.{w', w, v, u} C] : HasCofilteredLimitsOfSize.{w', w, v, u} C

@[instance 100]

instance CategoryTheory.Limits.hasLimitsOfShape_of_has_cofiltered_limits {C : Type u} [Category.{v, u} C] [HasCofilteredLimitsOfSize.{w', w, v, u} C] (I : Type w) [Category.{w', w} I] [IsCofiltered I] : HasLimitsOfShape I C

@[instance 100]

instance CategoryTheory.Limits.hasColimitsOfShape_of_has_filtered_colimits {C : Type u} [Category.{v, u} C] [HasFilteredColimitsOfSize.{w', w, v, u} C] (I : Type w) [Category.{w', w} I] [IsFiltered I] : HasColimitsOfShape I C

theorem CategoryTheory.Limits.hasCofilteredLimitsOfSize_of_univLE {C : Type u} [Category.{v, u} C] [UnivLE.{w, w₂}] [UnivLE.{w', w₂'}] [HasCofilteredLimitsOfSize.{w₂', w₂, v, u} C] : HasCofilteredLimitsOfSize.{w', w, v, u} C

theorem CategoryTheory.Limits.hasCofilteredLimitsOfSize_shrink {C : Type u} [Category.{v, u} C] [HasCofilteredLimitsOfSize.{max w' w₂', max w w₂, v, u} C] : HasCofilteredLimitsOfSize.{w', w, v, u} C

theorem CategoryTheory.Limits.hasFilteredColimitsOfSize_of_univLE {C : Type u} [Category.{v, u} C] [UnivLE.{w, w₂}] [UnivLE.{w', w₂'}] [HasFilteredColimitsOfSize.{w₂', w₂, v, u} C] : HasFilteredColimitsOfSize.{w', w, v, u} C

theorem CategoryTheory.Limits.hasFilteredColimitsOfSize_shrink {C : Type u} [Category.{v, u} C] [HasFilteredColimitsOfSize.{max w' w₂', max w w₂, v, u} C] : HasFilteredColimitsOfSize.{w', w, v, u} C