fix(group_theory/group_action/defs): deduplicate const_smul_hom and…

… `distrib_mul_action.to_add_monoid_hom` (#8953)

This removes `const_smul_hom` as `distrib_mul_action.to_add_monoid_hom` fits a larger family of similarly-named definitions.

This also renames `distrib_mul_action.hom_add_monoid_hom` to `distrib_mul_action.to_add_monoid_End` to better match its statement.

[Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Definition.20elimination.20contest/near/237347199)

src/algebra/direct_sum/algebra.lean

@@ -80,10 +80,11 @@ instance : algebra R (⨁ i, A i) :=
     apply dfinsupp.single_eq_of_sigma_eq (galgebra.commutes r ⟨i, xi⟩),
   end,
   smul_def' := λ r x, begin
-    change const_smul_hom _ r x = add_monoid_hom.mul (direct_sum.of _ _ _) x,
+    change distrib_mul_action.to_add_monoid_hom _ r x = add_monoid_hom.mul (direct_sum.of _ _ _) x,
     apply add_monoid_hom.congr_fun _ x,
     ext i xi : 2,
-    dsimp only [add_monoid_hom.comp_apply, const_smul_hom_apply, add_monoid_hom.mul_apply],
+    dsimp only [add_monoid_hom.comp_apply, distrib_mul_action.to_add_monoid_hom_apply,
+      add_monoid_hom.mul_apply],
     rw [direct_sum.of_mul_of, ←of_smul],
     apply dfinsupp.single_eq_of_sigma_eq (galgebra.smul_def r ⟨i, xi⟩),
   end }

src/algebra/group_ring_action.lean

@@ -50,31 +50,18 @@ mul_semiring_action.smul_mul g x y
 
 variables (M R)
 
-/-- Each element of the monoid defines a additive monoid homomorphism. -/
-@[simps]
-def distrib_mul_action.to_add_monoid_hom [distrib_mul_action M A] (x : M) : A →+ A :=
-{ to_fun   := (•) x,
-  map_zero' := smul_zero x,
-  map_add' := smul_add x }
-
 /-- Each element of the group defines an additive monoid isomorphism. -/
 @[simps]
 def distrib_mul_action.to_add_equiv [distrib_mul_action G A] (x : G) : A ≃+ A :=
-{ .. distrib_mul_action.to_add_monoid_hom G A x,
+{ .. distrib_mul_action.to_add_monoid_hom A x,
   .. mul_action.to_perm_hom G A x }
 
-/-- Each element of the group defines an additive monoid homomorphism. -/
-def distrib_mul_action.hom_add_monoid_hom [distrib_mul_action M A] : M →* add_monoid.End A :=
-{ to_fun := distrib_mul_action.to_add_monoid_hom M A,
-  map_one' := add_monoid_hom.ext $ λ x, one_smul M x,
-  map_mul' := λ x y, add_monoid_hom.ext $ λ z, mul_smul x y z }
-
 /-- Each element of the monoid defines a semiring homomorphism. -/
 @[simps]
 def mul_semiring_action.to_ring_hom [mul_semiring_action M R] (x : M) : R →+* R :=
 { map_one' := smul_one x,
   map_mul' := smul_mul' x,
-  .. distrib_mul_action.to_add_monoid_hom M R x }
+  .. distrib_mul_action.to_add_monoid_hom R x }
 
 theorem to_ring_hom_injective [mul_semiring_action M R] [has_faithful_scalar M R] :
   function.injective (mul_semiring_action.to_ring_hom M R) :=

src/algebra/module/basic.lean

@@ -114,7 +114,7 @@ variables (R) (M)
 
 /-- `(•)` as an `add_monoid_hom`. -/
 def smul_add_hom : R →+ M →+ M :=
-{ to_fun := const_smul_hom M,
+{ to_fun := distrib_mul_action.to_add_monoid_hom M,
   map_zero' := add_monoid_hom.ext $ λ r, by simp,
   map_add' := λ x y, add_monoid_hom.ext $ λ r, by simp [add_smul] }
 
@@ -125,7 +125,7 @@ variables {R M}
 
 @[simp] lemma smul_add_hom_one {R M : Type*} [semiring R] [add_comm_monoid M] [module R M] :
   smul_add_hom R M 1 = add_monoid_hom.id _ :=
-const_smul_hom_one
+(distrib_mul_action.to_add_monoid_End R M).map_one
 
 lemma module.eq_zero_of_zero_eq_one (zero_eq_one : (0 : R) = 1) : x = 0 :=
 by rw [←one_smul R x, ←zero_eq_one, zero_smul]

src/algebra/polynomial/group_ring_action.lean

@@ -27,7 +27,7 @@ lemma smul_eq_map [mul_semiring_action M R] (m : M) :
   ((•) m) = map (mul_semiring_action.to_ring_hom M R m) :=
 begin
   suffices :
-    distrib_mul_action.to_add_monoid_hom M (polynomial R) m =
+    distrib_mul_action.to_add_monoid_hom (polynomial R) m =
       (map_ring_hom (mul_semiring_action.to_ring_hom M R m)).to_add_monoid_hom,
   { ext1 r, exact add_monoid_hom.congr_fun this r, },
   ext n r : 2,

src/group_theory/group_action/basic.lean

@@ -248,7 +248,7 @@ variables [monoid α] [add_monoid β] [distrib_mul_action α β]
 
 lemma list.smul_sum {r : α} {l : list β} :
   r • l.sum = (l.map ((•) r)).sum :=
-(const_smul_hom β r).map_list_sum l
+(distrib_mul_action.to_add_monoid_hom β r).map_list_sum l
 
 /-- `smul` by a `k : M` over a ring is injective, if `k` is not a zero divisor.
 The general theory of such `k` is elaborated by `is_smul_regular`.
@@ -269,10 +269,10 @@ variables [monoid α] [add_comm_monoid β] [distrib_mul_action α β]
 
 lemma multiset.smul_sum {r : α} {s : multiset β} :
   r • s.sum = (s.map ((•) r)).sum :=
-(const_smul_hom β r).map_multiset_sum s
+(distrib_mul_action.to_add_monoid_hom β r).map_multiset_sum s
 
 lemma finset.smul_sum {r : α} {f : γ → β} {s : finset γ} :
   r • ∑ x in s, f x = ∑ x in s, r • f x :=
-(const_smul_hom β r).map_sum f s
+(distrib_mul_action.to_add_monoid_hom β r).map_sum f s
 
 end

src/group_theory/group_action/defs.lean

@@ -378,20 +378,21 @@ See note [reducible non-instances]. -/
   smul_add := λ x, smul_add (f x),
   .. mul_action.comp_hom A f }
 
-/-- Scalar multiplication by `r` as an `add_monoid_hom`. -/
-def const_smul_hom (r : M) : A →+ A :=
-{ to_fun := (•) r,
-  map_zero' := smul_zero r,
-  map_add' := smul_add r }
+/-- Each element of the monoid defines a additive monoid homomorphism. -/
+@[simps]
+def distrib_mul_action.to_add_monoid_hom (x : M) : A →+ A :=
+{ to_fun := (•) x,
+  map_zero' := smul_zero x,
+  map_add' := smul_add x }
 
-variable {A}
-
-@[simp] lemma const_smul_hom_apply (r : M) (x : A) :
-  const_smul_hom A r x = r • x := rfl
+variables (M)
 
-@[simp] lemma const_smul_hom_one :
-  const_smul_hom A (1:M) = add_monoid_hom.id _ :=
-by { ext, rw [const_smul_hom_apply, one_smul, add_monoid_hom.id_apply] }
+/-- Each element of the monoid defines an additive monoid homomorphism. -/
+@[simps]
+def distrib_mul_action.to_add_monoid_End : M →* add_monoid.End A :=
+{ to_fun := distrib_mul_action.to_add_monoid_hom A,
+  map_one' := add_monoid_hom.ext $ one_smul M,
+  map_mul' := λ x y, add_monoid_hom.ext $ mul_smul x y }
 
 end
 

src/topology/algebra/infinite_sum.lean

@@ -759,7 +759,7 @@ variables {R : Type*}
 {f : β → α}
 
 lemma has_sum.smul {a : α} {r : R} (hf : has_sum f a) : has_sum (λ z, r • f z) (r • a) :=
-hf.map (const_smul_hom α r) (continuous_const.smul continuous_id)
+hf.map (distrib_mul_action.to_add_monoid_hom α r) (continuous_const.smul continuous_id)
 
 lemma summable.smul {r : R} (hf : summable f) : summable (λ z, r • f z) :=
 hf.has_sum.smul.summable