chore(category_theory/limits): preserving coequalizers (#5212)

dualise stuff from before

Author: b-mehta

src/category_theory/limits/preserves/shapes/equalizers.lean

@@ -7,13 +7,13 @@ import category_theory.limits.shapes.equalizers
 import category_theory.limits.preserves.basic
 
 /-!
-# Preserving equalizers
+# Preserving (co)equalizers
 
-Constructions to relate the notions of preserving equalizers and reflecting equalizers
-to concrete forks.
+Constructions to relate the notions of preserving (co)equalizers and reflecting (co)equalizers
+to concrete (co)forks.
 
 In particular, we show that `equalizer_comparison G f` is an isomorphism iff `G` preserves
-the limit of `f`.
+the limit of `f` as well as the dual.
 -/
 
 noncomputable theory
@@ -28,6 +28,7 @@ variables (G : C ⥤ D)
 
 namespace category_theory.limits
 
+section equalizers
 variables {X Y Z : C} {f g : X ⟶ Y} {h : Z ⟶ X} (w : h ≫ f = h ≫ g)
 
 /--
@@ -38,7 +39,7 @@ def is_limit_map_cone_fork_equiv :
   is_limit (G.map_cone (fork.of_ι h w)) ≃
   is_limit (fork.of_ι (G.map h) (by simp only [←G.map_comp, w]) : fork (G.map f) (G.map g)) :=
 (is_limit.postcompose_hom_equiv (diagram_iso_parallel_pair _) _).symm.trans
-  (is_limit.equiv_iso_limit (fork.ext (iso.refl _) (by simp [fork.ι_eq_app_zero])))
+  (is_limit.equiv_iso_limit (fork.ext (iso.refl _) (by simp)))
 
 /-- The property of preserving equalizers expressed in terms of forks. -/
 def is_limit_fork_map_of_is_limit [preserves_limit (parallel_pair f g) G]
@@ -80,7 +81,6 @@ begin
 end
 
 variables [preserves_limit (parallel_pair f g) G]
-
 /--
 If `G` preserves the equalizer of `(f,g)`, then the equalizer comparison map for `G` at `(f,g)` is
 an isomorphism.
@@ -102,4 +102,83 @@ begin
   apply_instance
 end
 
+end equalizers
+
+section coequalizers
+
+variables {X Y Z : C} {f g : X ⟶ Y} {h : Y ⟶ Z} (w : f ≫ h = g ≫ h)
+
+/--
+The map of a cofork is a colimit iff the cofork consisting of the mapped morphisms is a colimit.
+This essentially lets us commute `cofork.of_π` with `functor.map_cocone`.
+-/
+def is_colimit_map_cocone_cofork_equiv :
+  is_colimit (G.map_cocone (cofork.of_π h w)) ≃
+  is_colimit (cofork.of_π (G.map h) (by simp only [←G.map_comp, w]) : cofork (G.map f) (G.map g)) :=
+(is_colimit.precompose_inv_equiv (diagram_iso_parallel_pair _) _).symm.trans
+  (is_colimit.equiv_iso_colimit (cofork.ext (iso.refl _) (by { dsimp, simp })))
+
+/-- The property of preserving coequalizers expressed in terms of coforks. -/
+def is_colimit_cofork_map_of_is_colimit [preserves_colimit (parallel_pair f g) G]
+  (l : is_colimit (cofork.of_π h w)) :
+  is_colimit (cofork.of_π (G.map h) (by simp only [←G.map_comp, w]) : cofork (G.map f) (G.map g)) :=
+is_colimit_map_cocone_cofork_equiv G w (preserves_colimit.preserves l)
+
+/-- The property of reflecting coequalizers expressed in terms of coforks. -/
+def is_colimit_of_is_colimit_cofork_map [reflects_colimit (parallel_pair f g) G]
+  (l : is_colimit (cofork.of_π (G.map h) (by simp only [←G.map_comp, w])
+                  : cofork (G.map f) (G.map g))) :
+  is_colimit (cofork.of_π h w) :=
+reflects_colimit.reflects ((is_colimit_map_cocone_cofork_equiv G w).symm l)
+
+variables (f g) [has_coequalizer f g]
+
+/--
+If `G` preserves coequalizers and `C` has them, then the cofork constructed of the mapped morphisms
+of a cofork is a colimit.
+-/
+def is_colimit_of_has_coequalizer_of_preserves_colimit
+  [preserves_colimit (parallel_pair f g) G] :
+  is_colimit (cofork.of_π (G.map (coequalizer.π f g)) _) :=
+is_colimit_cofork_map_of_is_colimit G _ (coequalizer_is_coequalizer f g)
+
+variables [has_coequalizer (G.map f) (G.map g)]
+
+/--
+If the coequalizer comparison map for `G` at `(f,g)` is an isomorphism, then `G` preserves the
+coequalizer of `(f,g)`.
+-/
+def of_iso_comparison [i : is_iso (coequalizer_comparison f g G)] :
+  preserves_colimit (parallel_pair f g) G :=
+begin
+  apply preserves_colimit_of_preserves_colimit_cocone (coequalizer_is_coequalizer f g),
+  apply (is_colimit_map_cocone_cofork_equiv _ _).symm _,
+  apply is_colimit.of_point_iso (colimit.is_colimit (parallel_pair (G.map f) (G.map g))),
+  apply i,
+end
+
+variables [preserves_colimit (parallel_pair f g) G]
+/--
+If `G` preserves the coequalizer of `(f,g)`, then the coequalizer comparison map for `G` at `(f,g)`
+is an isomorphism.
+-/
+def preserves_coequalizer.iso :
+  coequalizer (G.map f) (G.map g) ≅ G.obj (coequalizer f g) :=
+is_colimit.cocone_point_unique_up_to_iso
+  (colimit.is_colimit _)
+  (is_colimit_of_has_coequalizer_of_preserves_colimit G f g)
+
+@[simp]
+lemma preserves_coequalizer.iso_hom :
+  (preserves_coequalizer.iso G f g).hom = coequalizer_comparison f g G :=
+rfl
+
+instance : is_iso (coequalizer_comparison f g G) :=
+begin
+  rw ← preserves_coequalizer.iso_hom,
+  apply_instance
+end
+
+end coequalizers
+
 end category_theory.limits

src/category_theory/limits/shapes/equalizers.lean

@@ -682,7 +682,6 @@ lemma map_lift_equalizer_comparison [has_equalizer f g] [has_equalizer (G.map f)
       equalizer.lift (G.map h) (by simp only [←G.map_comp, w]) :=
 by { ext, simp [← G.map_comp] }
 
--- TODO: show this is an iso iff G preserves the coequalizer of `f,g`.
 /-- The comparison morphism for the coequalizer of `f,g`. -/
 def coequalizer_comparison [has_coequalizer f g] [has_coequalizer (G.map f) (G.map g)] :
   coequalizer (G.map f) (G.map g) ⟶ G.obj (coequalizer f g) :=