feat(topology/algebra/module/basic): add continuous_linear_map.apply_module (#14223)

This matches `linear_map.apply_module`, but additionally provides `has_continuous_const_smul`.

This also adds the missing `continuous_linear_map.semiring` and `continuous_linear_map.monoid_with_zero` instances.

Author: eric-wieser

src/topology/algebra/module/basic.lean

@@ -620,6 +620,59 @@ lemma mul_def (f g : M₁ →L[R₁] M₁) : f * g = f.comp g := rfl
 
 lemma mul_apply (f g : M₁ →L[R₁] M₁) (x : M₁) : (f * g) x = f (g x) := rfl
 
+instance : monoid_with_zero (M₁ →L[R₁] M₁) :=
+{ mul := (*),
+  one := 1,
+  zero := 0,
+  mul_zero := λ f, ext $ λ _, map_zero f,
+  zero_mul := λ _, ext $ λ _, rfl,
+  mul_one := λ _, ext $ λ _, rfl,
+  one_mul := λ _, ext $ λ _, rfl,
+  mul_assoc := λ _ _ _, ext $ λ _, rfl, }
+
+instance [has_continuous_add M₁] : semiring (M₁ →L[R₁] M₁) :=
+{ mul := (*),
+  one := 1,
+  left_distrib := λ f g h, ext $ λ x, map_add f (g x) (h x),
+  right_distrib := λ _ _ _, ext $ λ _, linear_map.add_apply _ _ _,
+  ..continuous_linear_map.monoid_with_zero,
+  ..continuous_linear_map.add_comm_monoid }
+
+/-- `continuous_linear_map.to_linear_map` as a `ring_hom`.-/
+@[simps]
+def to_linear_map_ring_hom [has_continuous_add M₁] : (M₁ →L[R₁] M₁) →+* (M₁ →ₗ[R₁] M₁) :=
+{ to_fun := to_linear_map,
+  map_zero' := rfl,
+  map_one' := rfl,
+  map_add' := λ _ _, rfl,
+  map_mul' := λ _ _, rfl }
+
+section apply_action
+variables [has_continuous_add M₁]
+
+/-- The tautological action by `M₁ →L[R₁] M₁` on `M`.
+
+This generalizes `function.End.apply_mul_action`. -/
+instance apply_module : module (M₁ →L[R₁] M₁) M₁ :=
+module.comp_hom _ to_linear_map_ring_hom
+
+@[simp] protected lemma smul_def (f : M₁ →L[R₁] M₁) (a : M₁) : f • a = f a := rfl
+
+/-- `continuous_linear_map.apply_module` is faithful. -/
+instance apply_has_faithful_scalar : has_faithful_scalar (M₁ →L[R₁] M₁) M₁ :=
+⟨λ _ _, continuous_linear_map.ext⟩
+
+instance apply_smul_comm_class : smul_comm_class R₁ (M₁ →L[R₁] M₁) M₁ :=
+{ smul_comm := λ r e m, (e.map_smul r m).symm }
+
+instance apply_smul_comm_class' : smul_comm_class (M₁ →L[R₁] M₁) R₁ M₁ :=
+{ smul_comm := continuous_linear_map.map_smul }
+
+instance : has_continuous_const_smul (M₁ →L[R₁] M₁) M₁ :=
+⟨continuous_linear_map.continuous⟩
+
+end apply_action
+
 /-- The cartesian product of two bounded linear maps, as a bounded linear map. -/
 protected def prod [module R₁ M₂] [module R₁ M₃] (f₁ : M₁ →L[R₁] M₂) (f₂ : M₁ →L[R₁] M₃) :
   M₁ →L[R₁] (M₂ × M₃) :=
@@ -984,11 +1037,7 @@ end
 instance [topological_add_group M] : ring (M →L[R] M) :=
 { mul := (*),
   one := 1,
-  mul_one := λ _, ext $ λ _, rfl,
-  one_mul := λ _, ext $ λ _, rfl,
-  mul_assoc := λ _ _ _, ext $ λ _, rfl,
-  left_distrib := λ f g h, ext $ λ x, map_add f (g x) (h x),
-  right_distrib := λ _ _ _, ext $ λ _, linear_map.add_apply _ _ _,
+  ..continuous_linear_map.semiring,
   ..continuous_linear_map.add_comm_group }
 
 lemma smul_right_one_pow [topological_space R] [topological_ring R] (c : R) (n : ℕ) :