feat(category_theory/limits/shapes/products): if each f b ⟶ g b is …

…mono, then `∏ f ⟶ ∏ g` is mono (#16180)

and its dual version: if each `f b ⟶ g b` is epi, then `∐ f ⟶ ∐ g` is epi

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'`.
 -/

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.