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} [CategoryTheory.Category.{v, u} C] : CategoryTheory.IsFiltered C ↔ ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.FinCategory J] (F : CategoryTheory.Functor J C), ∃ (X : C), Nonempty (CategoryTheory.Limits.limit (F.op.comp (CategoryTheory.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} [CategoryTheory.Category.{v, u} C] : CategoryTheory.IsCofiltered C ↔ ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.FinCategory J] (F : CategoryTheory.Functor J C), ∃ (X : C), Nonempty (CategoryTheory.Limits.limit (F.comp (CategoryTheory.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) [CategoryTheory.Category.{v, u} C] : Prop

Class for having all cofiltered limits of a given size.

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

  For all filtered types of size w, we have limits

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

For all filtered types of size w, we have limits

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

Class for having all filtered colimits of a given size.

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

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

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

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

@[reducible, inline]

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

Class for having cofiltered limits.

Equations

• CategoryTheory.Limits.HasCofilteredLimits C = CategoryTheory.Limits.HasCofilteredLimitsOfSize.{?u.16, ?u.16, ?u.16, ?u.15} C

@[reducible, inline]

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

Class for having filtered colimits.

Equations

• CategoryTheory.Limits.HasFilteredColimits C = CategoryTheory.Limits.HasFilteredColimitsOfSize.{?u.16, ?u.16, ?u.16, ?u.15} C

@[instance 100]

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

Equations

• ⋯ = ⋯

@[instance 100]

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

Equations

• ⋯ = ⋯