Documentation

Mathlib.CategoryTheory.Limits.Filtered

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] [inst_1 : 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] [inst_1 : 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 for having all cofiltered limits of a given size.

Instances

    Class for having all filtered colimits of a given size.

    Instances