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.
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] :
This follows this proof from
- Borceux, Handbook of categorical algebra 1, Theorem 2.13.4
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] :
This follows this proof from
- Borceux, Handbook of categorical algebra 1, Theorem 2.13.4 although with different names.
@[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] :