Filtered colimits commute with finite limits. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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]
[finite 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.
@[protected, 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] :
@[protected, instance]
def
category_theory.limits.colimit_limit_to_limit_colimit_cone_iso
{J K : Type v}
[category_theory.small_category J]
[category_theory.small_category K]
[category_theory.is_filtered K]
[category_theory.fin_category J]
(F : J ⥤ K ⥤ Type v) :
@[protected, instance]
noncomputable
def
category_theory.limits.filtered_colim_preserves_finite_limits_of_types
{K : Type v}
[category_theory.small_category K]
[category_theory.is_filtered K] :
Equations
- category_theory.limits.filtered_colim_preserves_finite_limits_of_types = category_theory.limits.preserves_finite_limits_of_preserves_finite_limits_of_size category_theory.limits.colim (λ (J : Type v) (𝒥 : category_theory.small_category J) (hJ : category_theory.fin_category J), {preserves_limit := id (λ (F : J ⥤ K ⥤ Type v), {preserves := λ (c : category_theory.limits.cone F) (hc : category_theory.limits.is_limit c), (category_theory.limits.limit.is_limit (F ⋙ category_theory.limits.colim)).of_iso_limit ((category_theory.limits.cones.functoriality F category_theory.limits.colim).map_iso (hc.unique_up_to_iso (category_theory.limits.limit.is_limit F)) ≪≫ category_theory.as_iso (category_theory.limits.colimit_limit_to_limit_colimit_cone F)).symm})})
@[protected, instance]
noncomputable
def
category_theory.limits.filtered_colim_preserves_finite_limits
{J K : Type v}
[category_theory.small_category J]
[category_theory.small_category K]
[category_theory.is_filtered K]
[category_theory.fin_category J]
{C : Type u}
[category_theory.category C]
[category_theory.concrete_category C]
[category_theory.limits.has_limits_of_shape J C]
[category_theory.limits.has_colimits_of_shape K C]
[category_theory.limits.reflects_limits_of_shape J (category_theory.forget C)]
[category_theory.limits.preserves_colimits_of_shape K (category_theory.forget C)]
[category_theory.limits.preserves_limits_of_shape J (category_theory.forget C)] :
@[protected, instance]
noncomputable
def
category_theory.limits.colim.preserves_finite_limits
{K : Type v}
[category_theory.small_category K]
[category_theory.is_filtered K]
{C : Type u}
[category_theory.category C]
[category_theory.concrete_category C]
[category_theory.limits.preserves_finite_limits (category_theory.forget C)]
[category_theory.limits.preserves_filtered_colimits (category_theory.forget C)]
[category_theory.limits.has_finite_limits C]
[category_theory.limits.has_colimits_of_shape K C]
[category_theory.reflects_isomorphisms (category_theory.forget C)] :
Equations
- category_theory.limits.colim.preserves_finite_limits = category_theory.limits.preserves_finite_limits_of_preserves_finite_limits_of_size category_theory.limits.colim (λ (J : Type v) (𝒥 : category_theory.small_category J) (hJ : category_theory.fin_category J), category_theory.limits.filtered_colim_preserves_finite_limits)
noncomputable
def
category_theory.limits.colimit_limit_iso
{J K : Type v}
[category_theory.small_category J]
[category_theory.small_category K]
[category_theory.is_filtered K]
[category_theory.fin_category J]
{C : Type u}
[category_theory.category C]
[category_theory.concrete_category C]
[category_theory.limits.has_limits_of_shape J C]
[category_theory.limits.has_colimits_of_shape K C]
[category_theory.limits.reflects_limits_of_shape J (category_theory.forget C)]
[category_theory.limits.preserves_colimits_of_shape K (category_theory.forget C)]
[category_theory.limits.preserves_limits_of_shape J (category_theory.forget C)]
(F : J ⥤ K ⥤ C) :
A curried version of the fact that filtered colimits commute with finite limits.
Equations
- category_theory.limits.colimit_limit_iso F = (category_theory.limits.is_limit_of_preserves category_theory.limits.colim (category_theory.limits.limit.is_limit F)).cone_point_unique_up_to_iso (category_theory.limits.limit.is_limit (F ⋙ category_theory.limits.colim)) ≪≫ category_theory.limits.has_limit.iso_of_nat_iso (category_theory.limits.colimit_flip_iso_comp_colim F).symm
@[simp]
theorem
category_theory.limits.ι_colimit_limit_iso_limit_π
{J K : Type v}
[category_theory.small_category J]
[category_theory.small_category K]
[category_theory.is_filtered K]
[category_theory.fin_category J]
{C : Type u}
[category_theory.category C]
[category_theory.concrete_category C]
[category_theory.limits.has_limits_of_shape J C]
[category_theory.limits.has_colimits_of_shape K C]
[category_theory.limits.reflects_limits_of_shape J (category_theory.forget C)]
[category_theory.limits.preserves_colimits_of_shape K (category_theory.forget C)]
[category_theory.limits.preserves_limits_of_shape J (category_theory.forget C)]
(F : J ⥤ K ⥤ C)
(a : K)
(b : J) :
@[simp]
theorem
category_theory.limits.ι_colimit_limit_iso_limit_π_assoc
{J K : Type v}
[category_theory.small_category J]
[category_theory.small_category K]
[category_theory.is_filtered K]
[category_theory.fin_category J]
{C : Type u}
[category_theory.category C]
[category_theory.concrete_category C]
[category_theory.limits.has_limits_of_shape J C]
[category_theory.limits.has_colimits_of_shape K C]
[category_theory.limits.reflects_limits_of_shape J (category_theory.forget C)]
[category_theory.limits.preserves_colimits_of_shape K (category_theory.forget C)]
[category_theory.limits.preserves_limits_of_shape J (category_theory.forget C)]
(F : J ⥤ K ⥤ C)
(a : K)
(b : J)
{X' : C}
(f' : (category_theory.limits.colimit F.flip).obj b ⟶ X') :
category_theory.limits.colimit.ι (category_theory.limits.limit F) a ≫ (category_theory.limits.colimit_limit_iso F).hom ≫ category_theory.limits.limit.π (category_theory.limits.colimit F.flip) b ≫ f' = (category_theory.limits.limit.π F b).app a ≫ (category_theory.limits.colimit.ι F.flip a).app b ≫ f'