From 9dd8ec1e5fc3f40aa6b71633d18aadadd171b544 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Mon, 7 Mar 2022 10:15:46 +0000
Subject: [PATCH] feat(analysis/normed/group/hom): add a module instance
 (#12465)

---
 src/analysis/normed/group/hom.lean | 49 ++++++++++++++++++++++++++++++
 1 file changed, 49 insertions(+)

diff --git a/src/analysis/normed/group/hom.lean b/src/analysis/normed/group/hom.lean
index ac8d2dc8384dd..6033e77614327 100644
--- a/src/analysis/normed/group/hom.lean
+++ b/src/analysis/normed/group/hom.lean
@@ -367,6 +367,43 @@ instance : has_sub (normed_group_hom V₁ V₂) :=
 @[simp] lemma sub_apply (f g : normed_group_hom V₁ V₂) (v : V₁) :
   (f - g : normed_group_hom V₁ V₂) v = f v - g v := rfl
 
+/-! ### Scalar actions on normed group homs -/
+
+section has_scalar
+
+variables {R R' : Type*}
+  [monoid_with_zero R] [distrib_mul_action R V₂] [pseudo_metric_space R] [has_bounded_smul R V₂]
+  [monoid_with_zero R'] [distrib_mul_action R' V₂] [pseudo_metric_space R'] [has_bounded_smul R' V₂]
+
+instance : has_scalar R (normed_group_hom V₁ V₂) :=
+{ smul := λ r f,
+  { to_fun := r • f,
+    map_add' := (r • f.to_add_monoid_hom).map_add',
+    bound' := let ⟨b, hb⟩ := f.bound' in  ⟨dist r 0 * b, λ x, begin
+      have := dist_smul_pair r (f x) (f 0),
+      rw [f.map_zero, smul_zero, dist_zero_right, dist_zero_right] at this,
+      rw mul_assoc,
+      refine this.trans _,
+      refine mul_le_mul_of_nonneg_left _ dist_nonneg,
+      exact hb x
+    end⟩ } }
+
+@[simp] lemma coe_smul (r : R) (f : normed_group_hom V₁ V₂) : ⇑(r • f) = r • f := rfl
+@[simp] lemma smul_apply (r : R) (f : normed_group_hom V₁ V₂) (v : V₁) : (r • f) v = r • f v := rfl
+
+instance [smul_comm_class R R' V₂] : smul_comm_class R R' (normed_group_hom V₁ V₂) :=
+{ smul_comm := λ r r' f, ext $ λ v, smul_comm _ _ _ }
+
+instance [has_scalar R R'] [is_scalar_tower R R' V₂] :
+  is_scalar_tower R R' (normed_group_hom V₁ V₂) :=
+{ smul_assoc := λ r r' f, ext $ λ v, smul_assoc _ _ _ }
+
+instance [distrib_mul_action Rᵐᵒᵖ V₂] [is_central_scalar R V₂] :
+  is_central_scalar R (normed_group_hom V₁ V₂) :=
+{ op_smul_eq_smul := λ r f, ext $ λ v, op_smul_eq_smul _ _ }
+
+end has_scalar
+
 /-! ### Normed group structure on normed group homs -/
 
 /-- Homs between two given normed groups form a commutative additive group. -/
@@ -397,6 +434,18 @@ lemma sum_apply {ι : Type*} (s : finset ι) (f : ι → normed_group_hom V₁ V
   (∑ i in s, f i) v = ∑ i in s, (f i v) :=
 by simp only [coe_sum, finset.sum_apply]
 
+/-! ### Module structure on normed group homs -/
+
+instance {R : Type*} [monoid_with_zero R] [distrib_mul_action R V₂]
+  [pseudo_metric_space R] [has_bounded_smul R V₂] :
+  distrib_mul_action R (normed_group_hom V₁ V₂) :=
+function.injective.distrib_mul_action coe_fn_add_hom coe_injective coe_smul
+
+instance {R : Type*} [semiring R] [module R V₂]
+  [pseudo_metric_space R] [has_bounded_smul R V₂] :
+  module R (normed_group_hom V₁ V₂) :=
+function.injective.module _ coe_fn_add_hom coe_injective coe_smul
+
 /-! ### Composition of normed group homs -/
 
 /-- The composition of continuous normed group homs. -/