feat(algebra/group): composition of monoid homs as "bilinear" monoid …

…hom (#5202)

src/algebra/group/hom.lean

@@ -584,6 +584,12 @@ add_decl_doc add_monoid_hom.has_zero
 @[simp, to_additive] lemma monoid_hom.one_apply [monoid M] [monoid N]
   (x : M) : (1 : M →* N) x = 1 := rfl
 
+@[simp, to_additive] lemma one_hom.one_comp [has_one M] [has_one N] [has_one P] (f : one_hom M N) :
+  (1 : one_hom N P).comp f = 1 := rfl
+@[simp, to_additive] lemma one_hom.comp_one [has_one M] [has_one N] [has_one P] (f : one_hom N P) :
+  f.comp (1 : one_hom M N) = 1 :=
+by { ext, simp only [one_hom.map_one, one_hom.coe_comp, function.comp_app, one_hom.one_apply] }
+
 @[to_additive]
 instance [has_one M] [has_one N] : inhabited (one_hom M N) := ⟨1⟩
 @[to_additive]
@@ -615,6 +621,20 @@ add_decl_doc add_monoid_hom.has_add
   (f g : M →* N) (x : M) :
   (f * g) x = f x * g x := rfl
 
+@[simp, to_additive] lemma one_comp [monoid M] [monoid N] [monoid P] (f : M →* N) :
+  (1 : N →* P).comp f = 1 := rfl
+@[simp, to_additive] lemma comp_one [monoid M] [monoid N] [monoid P] (f : N →* P) :
+  f.comp (1 : M →* N) = 1 :=
+by { ext, simp only [map_one, coe_comp, function.comp_app, one_apply] }
+
+@[to_additive] lemma mul_comp [monoid M] [comm_monoid N] [comm_monoid P]
+  (g₁ g₂ : N →* P) (f : M →* N) :
+  (g₁ * g₂).comp f = (g₁.comp f) * (g₂.comp f) := rfl
+@[to_additive] lemma comp_mul [monoid M] [comm_monoid N] [comm_monoid P]
+  (g : N →* P) (f₁ f₂ : M →* N) :
+  g.comp (f₁ * f₂) = (g.comp f₁) * (g.comp f₂) :=
+by { ext, simp only [mul_apply, function.comp_app, map_mul, coe_comp] }
+
 /-- (M →* N) is a comm_monoid if N is commutative. -/
 @[to_additive]
 instance {M N} [monoid M] [comm_monoid N] : comm_monoid (M →* N) :=
@@ -647,6 +667,15 @@ def eval [monoid M] [comm_monoid N] : M →* (M →* N) →* N := (monoid_hom.id
 @[simp, to_additive]
 lemma eval_apply [monoid M] [comm_monoid N] (x : M) (f : M →* N) : eval x f = f x := rfl
 
+/-- Composition of monoid morphisms (`monoid_hom.comp`) as a monoid morphism. -/
+@[simps, to_additive "Composition of additive monoid morphisms
+(`add_monoid_hom.comp`) as an additive monoid morphism."]
+def comp_hom [monoid M] [comm_monoid N] [comm_monoid P] :
+  (N →* P) →* (M →* N) →* (M →* P) :=
+{ to_fun := λ g, { to_fun := g.comp, map_one' := comp_one g, map_mul' := comp_mul g },
+  map_one' := by { ext1 f, exact one_comp f },
+  map_mul' := λ g₁ g₂, by { ext1 f, exact mul_comp g₁ g₂ f } }
+
 /-- If two homomorphism from a group to a monoid are equal at `x`, then they are equal at `x⁻¹`. -/
 @[to_additive "If two homomorphism from an additive group to an additive monoid are equal at `x`,
 then they are equal at `-x`." ]

src/category_theory/preadditive/default.lean

@@ -145,7 +145,7 @@ lemma mono_iff_cancel_zero {Q R : C} (f : Q ⟶ R) :
 
 lemma mono_of_kernel_zero {X Y : C} {f : X ⟶ Y} [has_limit (parallel_pair f 0)]
   (w : kernel.ι f = 0) : mono f :=
-mono_of_cancel_zero f (λ P g h, by rw [←kernel.lift_ι f g h, w, comp_zero])
+mono_of_cancel_zero f (λ P g h, by rw [←kernel.lift_ι f g h, w, limits.comp_zero])
 
 lemma epi_of_cancel_zero {P Q : C} (f : P ⟶ Q) (h : ∀ {R : C} (g : Q ⟶ R), f ≫ g = 0 → g = 0) :
   epi f :=
@@ -157,7 +157,7 @@ lemma epi_iff_cancel_zero {P Q : C} (f : P ⟶ Q) :
 
 lemma epi_of_cokernel_zero {X Y : C} (f : X ⟶ Y) [has_colimit (parallel_pair f 0 )]
   (w : cokernel.π f = 0) : epi f :=
-epi_of_cancel_zero f (λ P g h, by rw [←cokernel.π_desc f g h, w, zero_comp])
+epi_of_cancel_zero f (λ P g h, by rw [←cokernel.π_desc f g h, w, limits.zero_comp])
 
 end preadditive