Preservation of (co)limits in the functor category #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
- Show that if
X ⨯ -preserves colimits inDfor anyX : D, then the product functorF ⨯ -forF : C ⥤ Dpreserves colimits.
The idea of the proof is simply that products and colimits in the functor category are computed pointwise, so pointwise preservation implies general preservation.
- Show that
F ⋙ -preserves limits if the target category has limits. - Show that
F : C ⥤ Dpreserves limits of a certain shape ifLan F.op : Cᵒᵖ ⥤ Type*preserves such limits.
References #
noncomputable
def
category_theory.functor_category.prod_preserves_colimits
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_binary_products D]
[category_theory.limits.has_colimits D]
[Π (X : D), category_theory.limits.preserves_colimits (category_theory.limits.prod.functor.obj X)]
(F : C ⥤ D) :
If X × - preserves colimits in D for any X : D, then the product functor F ⨯ - for
F : C ⥤ D also preserves colimits.
Note this is (mathematically) a special case of the statement that
"if limits commute with colimits in D, then they do as well in C ⥤ D"
but the story in Lean is a bit more complex, and this statement isn't directly a special case.
That is, even with a formalised proof of the general statement, there would still need to be some
work to convert to this version: namely, the natural isomorphism
(evaluation C D).obj k ⋙ prod.functor.obj (F.obj k) ≅ prod.functor.obj F ⋙ (evaluation C D).obj k
Equations
- category_theory.functor_category.prod_preserves_colimits F = {preserves_colimits_of_shape := λ (J : Type u) (𝒥 : category_theory.category J), {preserves_colimit := λ (K : J ⥤ C ⥤ D), {preserves := λ (c : category_theory.limits.cocone K) (t : category_theory.limits.is_colimit c), category_theory.limits.evaluation_jointly_reflects_colimits ((category_theory.limits.prod.functor.obj F).map_cocone c) (λ (k : C), id (let this : category_theory.limits.is_colimit (((category_theory.evaluation C D).obj k ⋙ category_theory.limits.prod.functor.obj (F.obj k)).map_cocone c) := category_theory.limits.is_colimit_of_preserves ((category_theory.evaluation C D).obj k ⋙ category_theory.limits.prod.functor.obj (F.obj k)) t in category_theory.limits.is_colimit.map_cocone_equiv (category_theory.nat_iso.of_components (λ (G : C ⥤ D), category_theory.as_iso (category_theory.limits.prod_comparison ((category_theory.evaluation C D).obj k) F G)) _).symm this))}}}
@[protected, instance]
noncomputable
def
category_theory.whiskering_left_preserves_limits
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{E : Type u}
[category_theory.category E]
[category_theory.limits.has_limits D]
(F : C ⥤ E) :
Equations
- category_theory.whiskering_left_preserves_limits F = {preserves_limits_of_shape := λ (J : Type u) (hJ : category_theory.category J), {preserves_limit := λ (K : J ⥤ E ⥤ D), {preserves := λ (c : category_theory.limits.cone K) (hc : category_theory.limits.is_limit c), category_theory.limits.evaluation_jointly_reflects_limits (((category_theory.whiskering_left C E D).obj F).map_cone c) (λ (Y : C), id (category_theory.limits.preserves_limit.preserves hc))}}}
@[protected, instance]
noncomputable
def
category_theory.whiskering_right_preserves_limits_of_shape
{C : Type u}
[category_theory.category C]
{D : Type u_2}
[category_theory.category D]
{E : Type u_3}
[category_theory.category E]
{J : Type u}
[category_theory.small_category J]
[category_theory.limits.has_limits_of_shape J D]
(F : D ⥤ E)
[category_theory.limits.preserves_limits_of_shape J F] :
Equations
- category_theory.whiskering_right_preserves_limits_of_shape F = {preserves_limit := λ (K : J ⥤ C ⥤ D), {preserves := λ (c : category_theory.limits.cone K) (hc : category_theory.limits.is_limit c), category_theory.limits.evaluation_jointly_reflects_limits (((category_theory.whiskering_right C D E).obj F).map_cone c) (λ (k : C), id (category_theory.limits.preserves_limit.preserves hc))}}
@[protected, instance]
noncomputable
def
category_theory.whiskering_right_preserves_limits
{C : Type u}
[category_theory.category C]
{D : Type u_2}
[category_theory.category D]
{E : Type u_3}
[category_theory.category E]
(F : D ⥤ E)
[category_theory.limits.has_limits D]
[category_theory.limits.preserves_limits F] :
Equations
noncomputable
def
category_theory.preserves_limit_of_Lan_preserves_limit
{C D : Type u}
[category_theory.small_category C]
[category_theory.small_category D]
(F : C ⥤ D)
(J : Type u)
[category_theory.small_category J]
[category_theory.limits.preserves_limits_of_shape J (category_theory.Lan F.op)] :
If Lan F.op : (Cᵒᵖ ⥤ Type*) ⥤ (Dᵒᵖ ⥤ Type*) preserves limits of shape J, so will F.