feat(category_theory): Filtered colimits preserves finite limits in algebraic categories (#10604)

Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>

Author: erdOne

src/category_theory/limits/filtered_colimit_commutes_finite_limit.lean

@@ -4,6 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 import category_theory.limits.colimit_limit
+import category_theory.limits.preserves.functor_category
+import category_theory.limits.preserves.finite
+import category_theory.limits.shapes.finite_limits
+import category_theory.limits.preserves.filtered
 
 /-!
 # Filtered colimits commute with finite limits.
@@ -308,14 +312,38 @@ begin
 end
 
 noncomputable
-instance filtered_colim_preserves_finite_limits :
-  preserves_limits_of_shape J (colim : (K ⥤ Type v) ⥤ _) := ⟨λ F, ⟨λ c hc,
+instance filtered_colim_preserves_finite_limits_of_types :
+  preserves_finite_limits (colim : (K ⥤ Type v) ⥤ _) := ⟨λ J _ _, by exactI ⟨λ F, ⟨λ c hc,
 begin
   apply is_limit.of_iso_limit (limit.is_limit _),
   symmetry,
   transitivity (colim.map_cone (limit.cone F)),
   exact functor.map_iso _ (hc.unique_up_to_iso (limit.is_limit F)),
   exact as_iso (colimit_limit_to_limit_colimit_cone F),
-end ⟩⟩
+end ⟩⟩⟩
+
+variables {C : Type u} [category.{v} C] [concrete_category.{v} C]
+section
+variables [has_limits_of_shape J C] [has_colimits_of_shape K C]
+variables [reflects_limits_of_shape J (forget C)] [preserves_colimits_of_shape K (forget C)]
+variables [preserves_limits_of_shape J (forget C)]
+
+noncomputable
+instance filtered_colim_preserves_finite_limits :
+  preserves_limits_of_shape J (colim : (K ⥤ C) ⥤ _) :=
+begin
+  haveI : preserves_limits_of_shape J ((colim : (K ⥤ C) ⥤ _) ⋙ forget C) :=
+    preserves_limits_of_shape_of_nat_iso (preserves_colimit_nat_iso _).symm,
+  exactI preserves_limits_of_shape_of_reflects_of_preserves _ (forget C)
+end
+end
+
+local attribute [instance] reflects_limits_of_shape_of_reflects_isomorphisms
+
+noncomputable
+instance [preserves_finite_limits (forget C)] [preserves_filtered_colimits (forget C)]
+  [has_finite_limits C] [has_colimits_of_shape K C] [reflects_isomorphisms (forget C)] :
+    preserves_finite_limits (colim : (K ⥤ C) ⥤ _) :=
+⟨λ _ _ _, by exactI category_theory.limits.filtered_colim_preserves_finite_limits⟩
 
 end category_theory.limits

src/category_theory/limits/preserves/functor_category.lean

@@ -78,6 +78,22 @@ begin
   exact preserves_limit.preserves hc,
 end ⟩⟩⟩
 
+instance whiskering_right_preserves_limits_of_shape {C : Type u} [category C]
+  {D : Type*} [category D] {E : Type*} [category.{u} E]
+  {J : Type u} [small_category J] [has_limits_of_shape J D]
+    (F : D ⥤ E) [preserves_limits_of_shape J F] :
+  preserves_limits_of_shape J ((whiskering_right C D E).obj F) := ⟨λ K, ⟨λ c hc,
+begin
+  apply evaluation_jointly_reflects_limits,
+  intro k,
+  change is_limit (((evaluation _ _).obj k ⋙ F).map_cone c),
+  exact preserves_limit.preserves hc,
+end ⟩⟩
+
+instance whiskering_right_preserves_limits {C : Type u} [category C]
+  {D : Type*} [category D] {E : Type*} [category.{u} E] (F : D ⥤ E)
+  [has_limits D] [preserves_limits F] : preserves_limits ((whiskering_right C D E).obj F) := {}
+
 /-- If `Lan F.op : (Cᵒᵖ ⥤ Type*) ⥤ (Dᵒᵖ ⥤ Type*)` preserves limits of shape `J`, so will `F`. -/
 noncomputable
 def preserves_limit_of_Lan_presesrves_limit {C D : Type u} [small_category C] [small_category D]

src/category_theory/limits/preserves/limits.lean

@@ -61,6 +61,21 @@ is_limit.cone_point_unique_up_to_iso_inv_comp _ _ j
 lemma lift_comp_preserves_limits_iso_hom (t : cone F) :
   G.map (limit.lift _ t) ≫ (preserves_limit_iso G F).hom = limit.lift (F ⋙ G) (G.map_cone _) :=
 by { ext, simp [← G.map_comp] }
+
+variables [preserves_limits_of_shape J G] [has_limits_of_shape J D] [has_limits_of_shape J C]
+
+/-- If `C, D` has all limits of shape `J`, and `G` preserves them, then `preserves_limit_iso` is
+functorial wrt `F`. -/
+@[simps] def preserves_limit_nat_iso : lim ⋙ G ≅ (whiskering_right J C D).obj G ⋙ lim :=
+nat_iso.of_components (λ F, preserves_limit_iso G F)
+begin
+  intros _ _ f,
+  ext,
+  dsimp,
+  simp only [preserves_limits_iso_hom_π, whisker_right_app, lim_map_π, category.assoc,
+    preserves_limits_iso_hom_π_assoc, ← G.map_comp]
+end
+
 end
 
 section
@@ -95,6 +110,24 @@ lemma ι_preserves_colimits_iso_hom (j : J) :
 lemma preserves_colimits_iso_inv_comp_desc (t : cocone F) :
   (preserves_colimit_iso G F).inv ≫ G.map (colimit.desc _ t) = colimit.desc _ (G.map_cocone t) :=
 by { ext, simp [← G.map_comp] }
+
+variables [preserves_colimits_of_shape J G] [has_colimits_of_shape J D] [has_colimits_of_shape J C]
+
+/-- If `C, D` has all colimits of shape `J`, and `G` preserves them, then `preserves_colimit_iso`
+is functorial wrt `F`. -/
+@[simps] def preserves_colimit_nat_iso : colim ⋙ G ≅ (whiskering_right J C D).obj G ⋙ colim :=
+nat_iso.of_components (λ F, preserves_colimit_iso G F)
+begin
+  intros _ _ f,
+  rw [← iso.inv_comp_eq, ← category.assoc, ← iso.eq_comp_inv],
+  ext,
+  dsimp,
+  erw ι_colim_map_assoc,
+  simp only [ι_preserves_colimits_iso_inv, whisker_right_app, category.assoc,
+    ι_preserves_colimits_iso_inv_assoc, ← G.map_comp],
+  erw ι_colim_map
+end
+
 end
 
 end category_theory