refactor(analysis/normed_space/operator_norm): generalize `continuous…

…_linear_map.lmul` to non-unital algebras (#15868)

After the recent refactor in #15310 of `algebra.lmul` (resulting in `linear_map.mul` in particular) the type class restrictions on `continuous_linear_map.lmul` (and `continuous_linear_map.lmul_right` and `continuous_linear_map.lmul_right_left`) can be weakened to non-unital normed algebras, which we do here.

`continuous_linear_map.lmulₗᵢ` and `continuous_linear_map.lmul_rightₗᵢ` have not had their type class requirements weakened because they require `norm_one_class`, and hence unital algebras. In many non-unital algebras (including all non-unital normed algebras with an approximate unit, and hence all C⋆-algebras), the maps `continuous_linear_map.lmul` (and `lmul_right`) are nevertheless isometric, but this requires other properties so they are not implemented here.

src/analysis/normed_space/operator_norm.lean

@@ -819,7 +819,10 @@ end prod
 variables {𝕜 E Fₗ Gₗ}
 
 section multiplication_linear
-variables (𝕜) (𝕜' : Type*) [normed_ring 𝕜'] [normed_algebra 𝕜 𝕜']
+
+section non_unital
+variables (𝕜) (𝕜' : Type*) [non_unital_semi_normed_ring 𝕜'] [normed_space 𝕜 𝕜']
+  [is_scalar_tower 𝕜 𝕜' 𝕜'] [smul_comm_class 𝕜 𝕜' 𝕜']
 
 /-- Left multiplication in a normed algebra as a continuous bilinear map. -/
 def lmul : 𝕜' →L[𝕜] 𝕜' →L[𝕜] 𝕜' :=
@@ -831,19 +834,6 @@ def lmul : 𝕜' →L[𝕜] 𝕜' →L[𝕜] 𝕜' :=
 @[simp] lemma op_norm_lmul_apply_le (x : 𝕜') : ∥lmul 𝕜 𝕜' x∥ ≤ ∥x∥ :=
 (op_norm_le_bound _ (norm_nonneg x) (norm_mul_le x))
 
-/-- Left multiplication in a normed algebra as a linear isometry to the space of
-continuous linear maps. -/
-def lmulₗᵢ [norm_one_class 𝕜'] : 𝕜' →ₗᵢ[𝕜] 𝕜' →L[𝕜] 𝕜' :=
-{ to_linear_map := lmul 𝕜 𝕜',
-  norm_map' := λ x, le_antisymm (op_norm_lmul_apply_le _ _ _)
-    (by { convert ratio_le_op_norm _ (1 : 𝕜'), simp [norm_one],
-          apply_instance }) }
-
-@[simp] lemma coe_lmulₗᵢ [norm_one_class 𝕜'] : ⇑(lmulₗᵢ 𝕜 𝕜') = lmul 𝕜 𝕜' := rfl
-
-@[simp] lemma op_norm_lmul_apply [norm_one_class 𝕜'] (x : 𝕜') : ∥lmul 𝕜 𝕜' x∥ = ∥x∥ :=
-(lmulₗᵢ 𝕜 𝕜').norm_map x
-
 /-- Right-multiplication in a normed algebra, considered as a continuous linear map. -/
 def lmul_right : 𝕜' →L[𝕜] 𝕜' →L[𝕜] 𝕜' := (lmul 𝕜 𝕜').flip
 
@@ -852,20 +842,6 @@ def lmul_right : 𝕜' →L[𝕜] 𝕜' →L[𝕜] 𝕜' := (lmul 𝕜 𝕜').fl
 @[simp] lemma op_norm_lmul_right_apply_le (x : 𝕜') : ∥lmul_right 𝕜 𝕜' x∥ ≤ ∥x∥ :=
 op_norm_le_bound _ (norm_nonneg x) (λ y, (norm_mul_le y x).trans_eq (mul_comm _ _))
 
-@[simp] lemma op_norm_lmul_right_apply [norm_one_class 𝕜'] (x : 𝕜') : ∥lmul_right 𝕜 𝕜' x∥ = ∥x∥ :=
-le_antisymm
-  (op_norm_lmul_right_apply_le _ _ _)
-  (by { convert ratio_le_op_norm _ (1 : 𝕜'), simp [norm_one],
-        apply_instance })
-
-/-- Right-multiplication in a normed algebra, considered as a linear isometry to the space of
-continuous linear maps. -/
-def lmul_rightₗᵢ [norm_one_class 𝕜'] : 𝕜' →ₗᵢ[𝕜] 𝕜' →L[𝕜] 𝕜' :=
-{ to_linear_map := lmul_right 𝕜 𝕜',
-  norm_map' := op_norm_lmul_right_apply 𝕜 𝕜' }
-
-@[simp] lemma coe_lmul_rightₗᵢ [norm_one_class 𝕜'] : ⇑(lmul_rightₗᵢ 𝕜 𝕜') = lmul_right 𝕜 𝕜' := rfl
-
 /-- Simultaneous left- and right-multiplication in a normed algebra, considered as a continuous
 trilinear map. -/
 def lmul_left_right : 𝕜' →L[𝕜] 𝕜' →L[𝕜] 𝕜' →L[𝕜] 𝕜' :=
@@ -888,6 +864,40 @@ lemma op_norm_lmul_left_right_le :
   ∥lmul_left_right 𝕜 𝕜'∥ ≤ 1 :=
 op_norm_le_bound _ zero_le_one (λ x, (one_mul ∥x∥).symm ▸ op_norm_lmul_left_right_apply_le 𝕜 𝕜' x)
 
+end non_unital
+
+section unital
+variables (𝕜) (𝕜' : Type*) [semi_normed_ring 𝕜'] [normed_algebra 𝕜 𝕜'] [norm_one_class 𝕜']
+
+/-- Left multiplication in a normed algebra as a linear isometry to the space of
+continuous linear maps. -/
+def lmulₗᵢ : 𝕜' →ₗᵢ[𝕜] 𝕜' →L[𝕜] 𝕜' :=
+{ to_linear_map := lmul 𝕜 𝕜',
+  norm_map' := λ x, le_antisymm (op_norm_lmul_apply_le _ _ _)
+    (by { convert ratio_le_op_norm _ (1 : 𝕜'), simp [norm_one],
+          apply_instance }) }
+
+@[simp] lemma coe_lmulₗᵢ : ⇑(lmulₗᵢ 𝕜 𝕜') = lmul 𝕜 𝕜' := rfl
+
+@[simp] lemma op_norm_lmul_apply (x : 𝕜') : ∥lmul 𝕜 𝕜' x∥ = ∥x∥ :=
+(lmulₗᵢ 𝕜 𝕜').norm_map x
+
+@[simp] lemma op_norm_lmul_right_apply (x : 𝕜') : ∥lmul_right 𝕜 𝕜' x∥ = ∥x∥ :=
+le_antisymm
+  (op_norm_lmul_right_apply_le _ _ _)
+  (by { convert ratio_le_op_norm _ (1 : 𝕜'), simp [norm_one],
+        apply_instance })
+
+/-- Right-multiplication in a normed algebra, considered as a linear isometry to the space of
+continuous linear maps. -/
+def lmul_rightₗᵢ : 𝕜' →ₗᵢ[𝕜] 𝕜' →L[𝕜] 𝕜' :=
+{ to_linear_map := lmul_right 𝕜 𝕜',
+  norm_map' := op_norm_lmul_right_apply 𝕜 𝕜' }
+
+@[simp] lemma coe_lmul_rightₗᵢ : ⇑(lmul_rightₗᵢ 𝕜 𝕜') = lmul_right 𝕜 𝕜' := rfl
+
+end unital
+
 end multiplication_linear
 
 section smul_linear
@@ -1649,7 +1659,7 @@ variables [normed_ring 𝕜'] [normed_algebra 𝕜 𝕜']
 by haveI := norm_one_class.nontrivial 𝕜'; exact (lmulₗᵢ 𝕜 𝕜').norm_to_continuous_linear_map
 
 @[simp] lemma op_norm_lmul_right [norm_one_class 𝕜'] : ∥lmul_right 𝕜 𝕜'∥ = 1 :=
-(op_norm_flip (@lmul 𝕜 _ 𝕜' _ _)).trans (op_norm_lmul _ _)
+(op_norm_flip (lmul 𝕜 𝕜')).trans (op_norm_lmul _ _)
 end
 
 /-- The norm of `lsmul` equals 1 in any nontrivial normed group.