feat(category_theory/flat_functor): Generalize results into algebraic…

… categories. (#10735)

Also proves that the identity is flat, and compositions of flat functors are flat.

src/category_theory/flat_functors.lean

@@ -83,6 +83,7 @@ end structured_arrow_cone
 
 section representably_flat
 variables {C : Type u₁} [category.{v₁} C] {D : Type u₂} [category.{v₂} D]
+variables {E : Type u₃} [category.{v₃} E]
 
 /--
 A functor `F : C ⥤ D` is representably-flat functor if the comma category `(X/F)`
@@ -93,6 +94,74 @@ class representably_flat (F : C ⥤ D) : Prop :=
 
 attribute [instance] representably_flat.cofiltered
 
+local attribute [instance] is_cofiltered.nonempty
+
+instance representably_flat.id : representably_flat (𝟭 C) :=
+begin
+  constructor,
+  intro X,
+  haveI : nonempty (structured_arrow X (𝟭 C)) := ⟨structured_arrow.mk (𝟙 _)⟩,
+  suffices : is_cofiltered_or_empty (structured_arrow X (𝟭 C)),
+  { resetI, constructor },
+  constructor,
+  { intros Y Z,
+    use structured_arrow.mk (𝟙 _),
+    use structured_arrow.hom_mk Y.hom (by erw [functor.id_map, category.id_comp]),
+    use structured_arrow.hom_mk Z.hom (by erw [functor.id_map, category.id_comp]) },
+  { intros Y Z f g,
+    use structured_arrow.mk (𝟙 _),
+    use structured_arrow.hom_mk Y.hom (by erw [functor.id_map, category.id_comp]),
+    ext,
+    transitivity Z.hom; simp }
+end
+
+instance representably_flat.comp (F : C ⥤ D) (G : D ⥤ E)
+  [representably_flat F] [representably_flat G] : representably_flat (F ⋙ G) :=
+begin
+  constructor,
+  intro X,
+  haveI : nonempty (structured_arrow X (F ⋙ G)),
+  { have f₁ : structured_arrow X G := nonempty.some infer_instance,
+    have f₂ : structured_arrow f₁.right F := nonempty.some infer_instance,
+    exact ⟨structured_arrow.mk (f₁.hom ≫ G.map f₂.hom)⟩ },
+  suffices : is_cofiltered_or_empty (structured_arrow X (F ⋙ G)),
+  { resetI, constructor },
+  constructor,
+  { intros Y Z,
+    let W := @is_cofiltered.min (structured_arrow X G) _ _
+      (structured_arrow.mk Y.hom) (structured_arrow.mk Z.hom),
+    let Y' : W ⟶ _ := is_cofiltered.min_to_left _ _,
+    let Z' : W ⟶ _ := is_cofiltered.min_to_right _ _,
+
+    let W' := @is_cofiltered.min (structured_arrow W.right F) _ _
+      (structured_arrow.mk Y'.right) (structured_arrow.mk Z'.right),
+    let Y'' : W' ⟶ _ := is_cofiltered.min_to_left _ _,
+    let Z'' : W' ⟶ _ := is_cofiltered.min_to_right _ _,
+
+    use structured_arrow.mk (W.hom ≫ G.map W'.hom),
+    use structured_arrow.hom_mk Y''.right (by simp [← G.map_comp]),
+    use structured_arrow.hom_mk Z''.right (by simp [← G.map_comp]) },
+  { intros Y Z f g,
+    let W := @is_cofiltered.eq (structured_arrow X G) _ _
+        (structured_arrow.mk Y.hom) (structured_arrow.mk Z.hom)
+        (structured_arrow.hom_mk (F.map f.right) (structured_arrow.w f))
+        (structured_arrow.hom_mk (F.map g.right) (structured_arrow.w g)),
+    let h : W ⟶ _ := is_cofiltered.eq_hom _ _,
+    let h_cond : h ≫ _ = h ≫ _ := is_cofiltered.eq_condition _ _,
+
+    let W' := @is_cofiltered.eq (structured_arrow W.right F) _ _
+        (structured_arrow.mk h.right) (structured_arrow.mk (h.right ≫ F.map f.right))
+        (structured_arrow.hom_mk f.right rfl)
+        (structured_arrow.hom_mk g.right (congr_arg comma_morphism.right h_cond).symm),
+    let h' : W' ⟶ _ := is_cofiltered.eq_hom _ _,
+    let h'_cond : h' ≫ _ = h' ≫ _ := is_cofiltered.eq_condition _ _,
+
+    use structured_arrow.mk (W.hom ≫ G.map W'.hom),
+    use structured_arrow.hom_mk h'.right (by simp [← G.map_comp]),
+    ext,
+    exact (congr_arg comma_morphism.right h'_cond : _) }
+end
+
 end representably_flat
 
 section has_limit
@@ -207,14 +276,14 @@ end has_limit
 
 
 section small_category
-variables {C D : Type u₁} [small_category C] [small_category D]
+variables {C D : Type u₁} [small_category C] [small_category D] (E : Type u₂) [category.{u₁} E]
 
 /--
 (Implementation)
 The evaluation of `Lan F` at `X` is the colimit over the costructured arrows over `X`.
 -/
 noncomputable
-def Lan_evaluation_iso_colim (E : Type u₂) [category.{u₁} E] (F : C ⥤ D) (X : D)
+def Lan_evaluation_iso_colim (F : C ⥤ D) (X : D)
   [∀ (X : D), has_colimits_of_shape (costructured_arrow F X) E] :
   Lan F ⋙ (evaluation D E).obj X ≅
   ((whiskering_left _ _ E).obj (costructured_arrow.proj F X)) ⋙ colim :=
@@ -232,30 +301,34 @@ begin
   rw [costructured_arrow.map_mk, category.id_comp, costructured_arrow.mk]
 end
 
+variables [concrete_category.{u₁} E] [has_limits E] [has_colimits E]
+variables [reflects_limits (forget E)] [preserves_filtered_colimits (forget E)]
+variables [preserves_limits (forget E)]
+
 /--
 If `F : C ⥤ D` is a representably flat functor between small categories, then the functor
 `Lan F.op` that takes presheaves over `C` to presheaves over `D` preserves finite limits.
 -/
 noncomputable
 instance Lan_preserves_finite_limits_of_flat (F : C ⥤ D) [representably_flat F] :
-  preserves_finite_limits (Lan F.op : _ ⥤ (Dᵒᵖ ⥤ Type u₁)) :=
+  preserves_finite_limits (Lan F.op : _ ⥤ (Dᵒᵖ ⥤ E)) :=
 ⟨λ J _ _, begin
   resetI,
-  apply preserves_limits_of_shape_of_evaluation (Lan F.op : (Cᵒᵖ ⥤ Type u₁) ⥤ (Dᵒᵖ ⥤ Type u₁)) J,
+  apply preserves_limits_of_shape_of_evaluation (Lan F.op : (Cᵒᵖ ⥤ E) ⥤ (Dᵒᵖ ⥤ E)) J,
   intro K,
   haveI : is_filtered (costructured_arrow F.op K) :=
     is_filtered.of_equivalence (structured_arrow_op_equivalence F (unop K)),
   exact preserves_limits_of_shape_of_nat_iso (Lan_evaluation_iso_colim _ _ _).symm
 end⟩
 
 instance Lan_flat_of_flat (F : C ⥤ D) [representably_flat F] :
-  representably_flat (Lan F.op : _ ⥤ (Dᵒᵖ ⥤ Type u₁)) := flat_of_preserves_finite_limits _
+  representably_flat (Lan F.op : _ ⥤ (Dᵒᵖ ⥤ E)) := flat_of_preserves_finite_limits _
 
 variable [has_finite_limits C]
 
 noncomputable
 instance Lan_preserves_finite_limits_of_preserves_finite_limits (F : C ⥤ D)
-  [preserves_finite_limits F] : preserves_finite_limits (Lan F.op : _ ⥤ (Dᵒᵖ ⥤ Type u₁)) :=
+  [preserves_finite_limits F] : preserves_finite_limits (Lan F.op : _ ⥤ (Dᵒᵖ ⥤ E)) :=
 begin
   haveI := flat_of_preserves_finite_limits F,
   apply_instance