chore(algebra/group/hom_instances): add monoid_hom versions of linear_map lemmas (#8461)

I mainly want the additive versions, but we may as well get the multiplicative ones too.

This also adds the missing `monoid_hom.map_div` and some other division versions of subtraction lemmas.

Author: eric-wieser

src/algebra/group/hom.lean

@@ -701,6 +701,11 @@ eq_inv_of_mul_eq_one $ f.map_mul_eq_one $ inv_mul_self g
 theorem map_mul_inv {G H} [group G] [group H] (f : G →* H) (g h : G) :
   f (g * h⁻¹) = (f g) * (f h)⁻¹ := by rw [f.map_mul, f.map_inv]
 
+/-- Group homomorphisms preserve division. -/
+@[simp, to_additive /-" Additive group homomorphisms preserve subtraction. "-/]
+theorem map_div {G H} [group G] [group H] (f : G →* H) (g h : G) : f (g / h) = (f g) / (f h) :=
+by rw [div_eq_mul_inv, div_eq_mul_inv, f.map_mul_inv g h]
+
 /-- A homomorphism from a group to a monoid is injective iff its kernel is trivial.
 For the iff statement on the triviality of the kernel, see `monoid_hom.injective_iff'`.  -/
 @[to_additive /-" A homomorphism from an additive group to an additive monoid is injective iff
@@ -733,6 +738,7 @@ def mk' (f : M → G) (map_mul : ∀ a b : M, f (a * b) = f a * f b) : M →* G
 omit mM
 
 /-- Makes a group homomorphism from a proof that the map preserves right division `λ x y, x * y⁻¹`.
+See also `monoid_hom.of_map_div` for a version using `λ x y, x / y`.
 -/
 @[to_additive "Makes an additive group homomorphism from a proof that the map preserves
 the operation `λ a b, a + -b`. See also `add_monoid_hom.of_map_sub` for a version using
@@ -749,6 +755,16 @@ calc f (x * y) = f x * (f $ 1 * 1⁻¹ * y⁻¹)⁻¹ : by simp only [one_mul, o
   ⇑(of_map_mul_inv f map_div) = f :=
 rfl
 
+/-- Define a morphism of additive groups given a map which respects ratios. -/
+@[to_additive /-"Define a morphism of additive groups given a map which respects difference."-/]
+def of_map_div {H : Type*} [group H] (f : G → H) (hf : ∀ x y, f (x / y) = f x / f y) : G →* H :=
+of_map_mul_inv f (by simpa only [div_eq_mul_inv] using hf)
+
+@[simp, to_additive]
+lemma coe_of_map_div {H : Type*} [group H] (f : G → H) (hf : ∀ x y, f (x / y) = f x / f y) :
+  ⇑(of_map_div f hf) = f :=
+rfl
+
 /-- If `f` is a monoid homomorphism to a commutative group, then `f⁻¹` is the homomorphism sending
 `x` to `(f x)⁻¹`. -/
 @[to_additive]
@@ -788,24 +804,6 @@ add_decl_doc add_monoid_hom.has_sub
 
 end monoid_hom
 
-namespace add_monoid_hom
-
-variables {A B : Type*} [add_zero_class A] [add_comm_group B] [add_group G] [add_group H]
-
-/-- Additive group homomorphisms preserve subtraction. -/
-@[simp] theorem map_sub (f : G →+ H) (g h : G) : f (g - h) = (f g) - (f h) :=
-by rw [sub_eq_add_neg, sub_eq_add_neg, f.map_add_neg g h]
-
-/-- Define a morphism of additive groups given a map which respects difference. -/
-def of_map_sub (f : G → H) (hf : ∀ x y, f (x - y) = f x - f y) : G →+ H :=
-of_map_add_neg f (by simpa only [sub_eq_add_neg] using hf)
-
-@[simp] lemma coe_of_map_sub (f : G → H) (hf : ∀ x y, f (x - y) = f x - f y) :
-  ⇑(of_map_sub f hf) = f :=
-rfl
-
-end add_monoid_hom
-
 section commute
 
 variables [mul_one_class M] [mul_one_class N] {a x y : M}

src/algebra/group/hom_instances.lean

@@ -112,6 +112,26 @@ def flip {mM : mul_one_class M} {mN : mul_one_class N} {mP : comm_monoid P} (f :
   f.flip y x = f x y :=
 rfl
 
+@[to_additive]
+lemma map_one₂ {mM : mul_one_class M} {mN : mul_one_class N} {mP : comm_monoid P}
+  (f : M →* N →* P) (n : N) : f 1 n = 1 :=
+(flip f n).map_one
+
+@[to_additive]
+lemma map_mul₂ {mM : mul_one_class M} {mN : mul_one_class N} {mP : comm_monoid P}
+  (f : M →* N →* P) (m₁ m₂ : M) (n : N) : f (m₁ * m₂) n = f m₁ n * f m₂ n :=
+(flip f n).map_mul _ _
+
+@[to_additive]
+lemma map_inv₂ {mM : group M} {mN : mul_one_class N} {mP : comm_group P}
+  (f : M →* N →* P) (m : M) (n : N) : f m⁻¹ n = (f m n)⁻¹ :=
+(flip f n).map_inv _
+
+@[to_additive]
+lemma map_div₂ {mM : group M} {mN : mul_one_class N} {mP : comm_group P}
+  (f : M →* N →* P) (m₁ m₂ : M) (n : N) : f (m₁ / m₂) n = f m₁ n / f m₂ n :=
+(flip f n).map_div _ _
+
 /-- Evaluation of a `monoid_hom` at a point as a monoid homomorphism. See also `monoid_hom.apply`
 for the evaluation of any function at a point. -/
 @[to_additive "Evaluation of an `add_monoid_hom` at a point as an additive monoid homomorphism.