From e11bafa5284544728bd3b189942e930e0d4701de Mon Sep 17 00:00:00 2001
From: Jujian Zhang <jujian.zhang1998@outlook.com>
Date: Tue, 6 Sep 2022 07:23:28 +0000
Subject: [PATCH] =?UTF-8?q?feat(category=5Ftheory/limits/shapes/products):?=
 =?UTF-8?q?=20if=20each=20`f=20b=20=E2=9F=B6=20g=20b`=20is=20mono,=20then?=
 =?UTF-8?q?=20`=E2=88=8F=20f=20=E2=9F=B6=20=E2=88=8F=20g`=20is=20mono=20(#?=
 =?UTF-8?q?16180)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

and its dual version: if each `f b ⟶ g b` is epi, then `∐ f ⟶ ∐ g` is epi
---
 src/category_theory/limits/has_limits.lean      | 15 +++++++++++++++
 src/category_theory/limits/shapes/products.lean | 10 ++++++++++
 2 files changed, 25 insertions(+)

diff --git a/src/category_theory/limits/has_limits.lean b/src/category_theory/limits/has_limits.lean
index b409eb045bf50..67bfe897f66f6 100644
--- a/src/category_theory/limits/has_limits.lean
+++ b/src/category_theory/limits/has_limits.lean
@@ -506,6 +506,14 @@ instance : is_right_adjoint (lim : (J ⥤ C) ⥤ C) := ⟨_, const_lim_adj⟩
 
 end lim_functor
 
+instance lim_map_mono' {F G : J ⥤ C} [has_limits_of_shape J C] (α : F ⟶ G)
+  [mono α] : mono (lim_map α) :=
+(lim : (J ⥤ C) ⥤ C).map_mono α
+
+instance lim_map_mono {F G : J ⥤ C} [has_limit F] [has_limit G] (α : F ⟶ G)
+  [∀ j, mono (α.app j)] : mono (lim_map α) :=
+⟨λ Z u v h, limit.hom_ext $ λ j, (cancel_mono (α.app j)).1 $ by simpa using h =≫ limit.π _ j⟩
+
 /--
 We can transport limits of shape `J` along an equivalence `J ≌ J'`.
 -/
@@ -1006,6 +1014,13 @@ instance : is_left_adjoint (colim : (J ⥤ C) ⥤ C) := ⟨_, colim_const_adj⟩
 
 end colim_functor
 
+instance colim_map_epi' {F G : J ⥤ C} [has_colimits_of_shape J C] (α : F ⟶ G) [epi α] :
+  epi (colim_map α) := (colim : (J ⥤ C) ⥤ C).map_epi α
+
+instance colim_map_epi {F G : J ⥤ C} [has_colimit F] [has_colimit G] (α : F ⟶ G)
+  [∀ j, epi (α.app j)] : epi (colim_map α) :=
+⟨λ Z u v h, colimit.hom_ext $ λ j, (cancel_epi (α.app j)).1 $ by simpa using colimit.ι _ j ≫= h⟩
+
 /--
 We can transport colimits of shape `J` along an equivalence `J ≌ J'`.
 -/
diff --git a/src/category_theory/limits/shapes/products.lean b/src/category_theory/limits/shapes/products.lean
index 4bf49c165731f..ed5d4f3caed4b 100644
--- a/src/category_theory/limits/shapes/products.lean
+++ b/src/category_theory/limits/shapes/products.lean
@@ -142,6 +142,11 @@ from a family of morphisms between the factors.
 abbreviation pi.map {f g : β → C} [has_product f] [has_product g]
   (p : Π b, f b ⟶ g b) : ∏ f ⟶ ∏ g :=
 lim_map (discrete.nat_trans (λ X, p X.as))
+
+instance pi.map_mono {f g : β → C} [has_product f] [has_product g]
+  (p : Π b, f b ⟶ g b) [Π i, mono (p i)] : mono $ pi.map p :=
+@@limits.lim_map_mono _ _ _ _ _ (by { dsimp, apply_instance })
+
 /--
 Construct an isomorphism between categorical products (indexed by the same type)
 from a family of isomorphisms between the factors.
@@ -156,6 +161,11 @@ from a family of morphisms between the factors.
 abbreviation sigma.map {f g : β → C} [has_coproduct f] [has_coproduct g]
   (p : Π b, f b ⟶ g b) : ∐ f ⟶ ∐ g :=
 colim_map (discrete.nat_trans (λ X, p X.as))
+
+instance sigma.map_epi {f g : β → C} [has_coproduct f] [has_coproduct g]
+  (p : Π b, f b ⟶ g b) [Π i, epi (p i)] : epi $ sigma.map p :=
+@@limits.colim_map_epi _ _ _ _ _ (by { dsimp, apply_instance })
+
 /--
 Construct an isomorphism between categorical coproducts (indexed by the same type)
 from a family of isomorphisms between the factors.