mathlib documentation

category_theory.limits.preserves.functor_category

Preservation of (co)limits in the functor category #

Show that if X ⨯ - preserves colimits in D for any X : D, then the product functor F ⨯ - for F : C ⥤ D preserves 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 ⥤ D preserves limits of a certain shape if Lan F.op : Cᵒᵖ ⥤ Type* preserves such limits.

References #

https://ncatlab.org/nlab/show/commutativity+of+limits+and+colimits#preservation_by_functor_categories_and_localizations

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) :

category_theory.limits.preserves_colimits (category_theory.limits.prod.functor.obj F)

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) :

category_theory.limits.preserves_limits ((category_theory.whiskering_left C E D).obj F)

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] :

category_theory.limits.preserves_limits_of_shape J ((category_theory.whiskering_right C D E).obj 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] :

category_theory.limits.preserves_limits ((category_theory.whiskering_right C D E).obj F)

Equations

category_theory.whiskering_right_preserves_limits F = {preserves_limits_of_shape := λ {J : Type u} [_inst_4_1 : category_theory.category J], category_theory.whiskering_right_preserves_limits_of_shape F}

noncomputable def category_theory.preserves_limit_of_Lan_presesrves_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)] :

category_theory.limits.preserves_limits_of_shape J F

If Lan F.op : (Cᵒᵖ ⥤ Type*) ⥤ (Dᵒᵖ ⥤ Type*) preserves limits of shape J, so will F.

Equations

category_theory.preserves_limit_of_Lan_presesrves_limit F J = category_theory.limits.preserves_limits_of_shape_of_reflects_of_preserves F category_theory.yoneda