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.

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]

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