feat: define RegularNormedAlgebra and add the norm on the `Unitizat…

…ion` (#5742)

This constructs a norm on the `Unitization 𝕜 A` of a (possibly non-unital) normed algebra `A`, subject to the condition that `ContinuousLinearMap.mul 𝕜 A` is an isometry. A norm on `A` satisfying this property is said to be regular so we add the class `RegularNormedAlgebra` where this construction makes sense.

This norm is particularly nice because, among norms on the unitization of a `RegularNormedAlgebra`, this norm is minimal. Moreover, it is the (necessarily unique) C⋆-norm on the unitization when the norm on `A` is a C⋆-norm (see #5393)

- [x] depends on: #5741

Mathlib.lean

@@ -772,6 +772,7 @@ import Mathlib.Analysis.NormedSpace.Star.Multiplier
 import Mathlib.Analysis.NormedSpace.Star.Spectrum
 import Mathlib.Analysis.NormedSpace.Star.Unitization
 import Mathlib.Analysis.NormedSpace.TrivSqZeroExt
+import Mathlib.Analysis.NormedSpace.Unitization
 import Mathlib.Analysis.NormedSpace.Units
 import Mathlib.Analysis.NormedSpace.WeakDual
 import Mathlib.Analysis.NormedSpace.WithLp

Mathlib/Algebra/Algebra/Unitization.lean

@@ -137,6 +137,14 @@ theorem inr_injective [Zero R] : Function.Injective ((↑) : A → Unitization R
   Function.LeftInverse.injective <| snd_inr _
 #align unitization.coe_injective Unitization.inr_injective
 
+instance instNontrivialLeft {𝕜 A} [Nontrivial 𝕜] [Nonempty A] :
+    Nontrivial (Unitization 𝕜 A) :=
+  nontrivial_prod_left
+
+instance instNontrivialRight {𝕜 A} [Nonempty 𝕜] [Nontrivial A] :
+    Nontrivial (Unitization 𝕜 A) :=
+  nontrivial_prod_right
+
 end Basic
 
 /-! ### Structures inherited from `Prod`
@@ -208,6 +216,11 @@ instance instModule [Semiring S] [AddCommMonoid R] [AddCommMonoid A] [Module S R
     Module S (Unitization R A) :=
   Prod.instModule
 
+variable (R A) in
+/-- The identity map between `Unitization R A` and `R × A` as an `AddEquiv`. -/
+def addEquiv [Add R] [Add A] : Unitization R A ≃+ R × A :=
+  AddEquiv.refl _
+
 @[simp]
 theorem fst_zero [Zero R] [Zero A] : (0 : Unitization R A).fst = 0 :=
   rfl

Mathlib/Analysis/NormedSpace/OperatorNorm.lean

@@ -1119,6 +1119,24 @@ theorem op_norm_mul_le : ‖mul 𝕜 𝕜'‖ ≤ 1 :=
   LinearMap.mkContinuous₂_norm_le _ zero_le_one _
 #align continuous_linear_map.op_norm_mul_le ContinuousLinearMap.op_norm_mul_le
 
+/-- Multiplication on the left in a non-unital normed algebra `𝕜'` as a non-unital algebra
+homomorphism into the algebra of *continuous* linear maps. This is the left regular representation
+of `A` acting on itself.
+
+This has more algebraic structure than `ContinuousLinearMap.mul`, but there is no longer continuity
+bundled in the first coordinate.  An alternative viewpoint is that this upgrades
+`NonUnitalAlgHom.lmul` from a homomorphism into linear maps to a homomorphism into *continuous*
+linear maps. -/
+def _root_.NonUnitalAlgHom.Lmul : 𝕜' →ₙₐ[𝕜] 𝕜' →L[𝕜] 𝕜' :=
+  { mul 𝕜 𝕜' with
+    map_mul' := fun _ _ ↦ ext fun _ ↦ mul_assoc _ _ _
+    map_zero' := ext fun _ ↦ zero_mul _ }
+
+variable {𝕜 𝕜'} in
+@[simp]
+theorem _root_.NonUnitalAlgHom.coe_Lmul : ⇑(NonUnitalAlgHom.Lmul 𝕜 𝕜') = mul 𝕜 𝕜' :=
+  rfl
+
 /-- Simultaneous left- and right-multiplication in a non-unital normed algebra, considered as a
 continuous trilinear map. This is akin to its non-continuous version `LinearMap.mulLeftRight`,
 but there is a minor difference: `LinearMap.mulLeftRight` is uncurried. -/
@@ -1151,36 +1169,53 @@ theorem op_norm_mulLeftRight_le : ‖mulLeftRight 𝕜 𝕜'‖ ≤ 1 :=
   op_norm_le_bound _ zero_le_one fun x => (one_mul ‖x‖).symm ▸ op_norm_mulLeftRight_apply_le 𝕜 𝕜' x
 #align continuous_linear_map.op_norm_mul_left_right_le ContinuousLinearMap.op_norm_mulLeftRight_le
 
-end NonUnital
+/-- This is a mixin class for non-unital normed algebras which states that the left-regular
+representation of the algebra on itself is isometric. Every unital normed algebra with `‖1‖ = 1` is
+a regular normed algebra (see `NormedAlgebra.instRegularNormedAlgebra`). In addiiton, so is every
+C⋆-algebra, non-unital included (see `CstarRing.instRegularNormedAlgebra`), but there are yet other
+examples. Any algebra with an approximate identity (e.g., $$L^1$$) is also regular.
+
+This is a useful class because it gives rise to a nice norm on the unitization; in particular it is
+a C⋆-norm when the norm on `A` is a C⋆-norm. -/
+class _root_.RegularNormedAlgebra : Prop :=
+  /-- The left regular representation of the algebra on itself is an isometry. -/
+  isometry_mul' : Isometry (mul 𝕜 𝕜')
+
+/-- Every (unital) normed algebra such that `‖1‖ = 1` is a `RegularNormedAlgebra`. -/
+instance _root_.NormedAlgebra.instRegularNormedAlgebra {𝕜 𝕜' : Type _} [NontriviallyNormedField 𝕜]
+    [SeminormedRing 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormOneClass 𝕜'] : RegularNormedAlgebra 𝕜 𝕜'  where
+  isometry_mul' := AddMonoidHomClass.isometry_of_norm (mul 𝕜 𝕜') <|
+    fun x => le_antisymm (op_norm_mul_apply_le _ _ _) <| by
+      convert ratio_le_op_norm ((mul 𝕜 𝕜') x) (1 : 𝕜')
+      simp [norm_one]
+
+variable [RegularNormedAlgebra 𝕜 𝕜']
 
-section Unital
+lemma isometry_mul : Isometry (mul 𝕜 𝕜') :=
+  RegularNormedAlgebra.isometry_mul'
 
-variable (𝕜) (𝕜' : Type*) [SeminormedRing 𝕜']
+@[simp]
+lemma op_norm_mul_apply (x : 𝕜') : ‖mul 𝕜 𝕜' x‖ = ‖x‖ :=
+  (AddMonoidHomClass.isometry_iff_norm (mul 𝕜 𝕜')).mp (isometry_mul 𝕜 𝕜') x
+#align continuous_linear_map.op_norm_mul_apply ContinuousLinearMap.op_norm_mul_applyₓ
 
-variable [NormedAlgebra 𝕜 𝕜'] [NormOneClass 𝕜']
+@[simp]
+lemma op_nnnorm_mul_apply (x : 𝕜') : ‖mul 𝕜 𝕜' x‖₊ = ‖x‖₊ :=
+  Subtype.ext <| op_norm_mul_apply 𝕜 𝕜' x
 
 /-- Multiplication in a normed algebra as a linear isometry to the space of
 continuous linear maps. -/
 def mulₗᵢ : 𝕜' →ₗᵢ[𝕜] 𝕜' →L[𝕜] 𝕜' where
   toLinearMap := mul 𝕜 𝕜'
-  norm_map' x :=
-    le_antisymm (op_norm_mul_apply_le _ _ _)
-      (by
-        convert ratio_le_op_norm ((mul 𝕜 𝕜') x) (1 : 𝕜')
-        simp [norm_one])
-#align continuous_linear_map.mulₗᵢ ContinuousLinearMap.mulₗᵢ
+  norm_map' x := op_norm_mul_apply 𝕜 𝕜' x
+#align continuous_linear_map.mulₗᵢ ContinuousLinearMap.mulₗᵢₓ
 
 @[simp]
 theorem coe_mulₗᵢ : ⇑(mulₗᵢ 𝕜 𝕜') = mul 𝕜 𝕜' :=
   rfl
-#align continuous_linear_map.coe_mulₗᵢ ContinuousLinearMap.coe_mulₗᵢ
-
-@[simp]
-theorem op_norm_mul_apply (x : 𝕜') : ‖mul 𝕜 𝕜' x‖ = ‖x‖ :=
-  (mulₗᵢ 𝕜 𝕜').norm_map x
-#align continuous_linear_map.op_norm_mul_apply ContinuousLinearMap.op_norm_mul_apply
+#align continuous_linear_map.coe_mulₗᵢ ContinuousLinearMap.coe_mulₗᵢₓ
 
-end Unital
+end NonUnital
 
 end MultiplicationLinear
 
@@ -1873,13 +1908,18 @@ variable (𝕜) (𝕜' : Type*)
 
 section
 
-variable [NormedRing 𝕜'] [NormedAlgebra 𝕜 𝕜']
+variable [NonUnitalNormedRing 𝕜'] [NormedSpace 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜']
+variable [SMulCommClass 𝕜 𝕜' 𝕜'] [RegularNormedAlgebra 𝕜 𝕜'] [Nontrivial 𝕜']
 
 @[simp]
-theorem op_norm_mul [NormOneClass 𝕜'] : ‖mul 𝕜 𝕜'‖ = 1 :=
-  haveI := NormOneClass.nontrivial 𝕜'
+theorem op_norm_mul : ‖mul 𝕜 𝕜'‖ = 1 :=
   (mulₗᵢ 𝕜 𝕜').norm_toContinuousLinearMap
-#align continuous_linear_map.op_norm_mul ContinuousLinearMap.op_norm_mul
+#align continuous_linear_map.op_norm_mul ContinuousLinearMap.op_norm_mulₓ
+
+@[simp]
+theorem op_nnnorm_mul : ‖mul 𝕜 𝕜'‖₊ = 1 :=
+  Subtype.ext <| op_norm_mul 𝕜 𝕜'
+#align continuous_linear_map.op_nnnorm_mul ContinuousLinearMap.op_nnnorm_mulₓ
 
 end
 

Mathlib/Analysis/NormedSpace/Star/Multiplier.lean

@@ -691,7 +691,7 @@ instance instCstarRing : CstarRing 𝓜(𝕜, A) where
           _ ≤ ‖a‖₊ * ‖a‖₊ := by simp only [mul_one, nnnorm_fst, le_rfl]
       rw [← nnnorm_snd]
       simp only [mul_snd, ← sSup_closed_unit_ball_eq_nnnorm, star_snd, mul_apply]
-      simp only [← @op_nnnorm_mul 𝕜 A]
+      simp only [← @_root_.op_nnnorm_mul 𝕜 A]
       simp only [← sSup_closed_unit_ball_eq_nnnorm, mul_apply']
       refine' csSup_eq_of_forall_le_of_forall_lt_exists_gt (hball.image _) _ fun r hr => _
       · rintro - ⟨x, hx, rfl⟩