Filtered colimits commute with finite limits. #

We show that for a functor F : J × K ⥤ Type v, when J is finite and K is filtered, the universal morphism colimit_limit_to_limit_colimit F comparing the colimit (over K) of the limits (over J) with the limit of the colimits is an isomorphism.

(In fact, to prove that it is injective only requires that J has finitely many objects.)

References #

Borceux, Handbook of categorical algebra 1, Theorem 2.13.4
Stacks: Filtered colimits

Injectivity doesn't need that we have finitely many morphisms in J, only that there are finitely many objects.

source

theorem category_theory.limits.colimit_limit_to_limit_colimit_injective {J K : Type v} [category_theory.small_category J] [category_theory.small_category K] (F : J × K ⥤ Type v) [category_theory.is_filtered K] [fintype J] :

function.injective (category_theory.limits.colimit_limit_to_limit_colimit F)

This follows this proof from

Borceux, Handbook of categorical algebra 1, Theorem 2.13.4

source

theorem category_theory.limits.colimit_limit_to_limit_colimit_surjective {J K : Type v} [category_theory.small_category J] [category_theory.small_category K] (F : J × K ⥤ Type v) [category_theory.is_filtered K] [category_theory.fin_category J] :

function.surjective (category_theory.limits.colimit_limit_to_limit_colimit F)

This follows this proof from

Borceux, Handbook of categorical algebra 1, Theorem 2.13.4 although with different names.

source

@[instance]

def category_theory.limits.colimit_limit_to_limit_colimit_is_iso {J K : Type v} [category_theory.small_category J] [category_theory.small_category K] (F : J × K ⥤ Type v) [category_theory.is_filtered K] [category_theory.fin_category J] :

category_theory.is_iso (category_theory.limits.colimit_limit_to_limit_colimit F)