From be7fa69be8901a2513db032a54d3750936510caf Mon Sep 17 00:00:00 2001
From: Jireh Loreaux <loreaujy@gmail.com>
Date: Fri, 18 Aug 2023 07:22:47 +0000
Subject: [PATCH] feat: define `RegularNormedAlgebra` and add the norm on the
 `Unitization` (#5742)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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                                  |   1 +
 Mathlib/Algebra/Algebra/Unitization.lean      |  13 +
 .../Analysis/NormedSpace/OperatorNorm.lean    |  82 ++++--
 .../Analysis/NormedSpace/Star/Multiplier.lean |   2 +-
 Mathlib/Analysis/NormedSpace/Unitization.lean | 262 ++++++++++++++++++
 5 files changed, 338 insertions(+), 22 deletions(-)
 create mode 100644 Mathlib/Analysis/NormedSpace/Unitization.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index 95b46b62da8e7..1bf8d114d1aa0 100644
--- a/Mathlib.lean
+++ b/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
diff --git a/Mathlib/Algebra/Algebra/Unitization.lean b/Mathlib/Algebra/Algebra/Unitization.lean
index c25c80890ee2c..8a419177f154e 100644
--- a/Mathlib/Algebra/Algebra/Unitization.lean
+++ b/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
diff --git a/Mathlib/Analysis/NormedSpace/OperatorNorm.lean b/Mathlib/Analysis/NormedSpace/OperatorNorm.lean
index 67f03d179db58..a112711a681d7 100644
--- a/Mathlib/Analysis/NormedSpace/OperatorNorm.lean
+++ b/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
 
diff --git a/Mathlib/Analysis/NormedSpace/Star/Multiplier.lean b/Mathlib/Analysis/NormedSpace/Star/Multiplier.lean
index ab356908a1ad4..7a83c547599c6 100644
--- a/Mathlib/Analysis/NormedSpace/Star/Multiplier.lean
+++ b/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⟩
diff --git a/Mathlib/Analysis/NormedSpace/Unitization.lean b/Mathlib/Analysis/NormedSpace/Unitization.lean
new file mode 100644
index 0000000000000..62a6f112b523b
--- /dev/null
+++ b/Mathlib/Analysis/NormedSpace/Unitization.lean
@@ -0,0 +1,262 @@
+/-
+Copyright (c) 2023 Jireh Loreaux. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jireh Loreaux
+-/
+
+import Mathlib.Algebra.Algebra.Unitization
+import Mathlib.Analysis.NormedSpace.OperatorNorm
+
+/-!
+# Unitization norms
+
+Given a not-necessarily-unital normed `𝕜`-algebra `A`, it is frequently of interest to equip its
+`Unitization` with a norm which simultaneously makes it into a normed algebra and also satisfies
+two properties:
+
+- `‖1‖ = 1` (i.e., `NormOneClass`)
+- The embedding of `A` in `Unitization 𝕜 A` is an isometry. (i.e., `Isometry Unitization.inr`)
+
+One way to do this is to pull back the norm from `WithLp 1 (𝕜 × A)`, that is,
+`‖(k, a)‖ = ‖k‖ + ‖a‖` using `Unitization.addEquiv` (i.e., the identity map). However, when the norm
+on `A` is *regular* (i.e., `ContinuousLinearMap.mul` is an isometry), there is another natural
+choice: the pullback of the norm on `𝕜 × (A →L[𝕜] A)` under the map
+`(k, a) ↦ (k, k • 1 + ContinuousLinearMap.mul 𝕜 A a)`. It turns out that among all norms on the
+unitization satisfying the properties specified above, the norm inherited from
+`WithLp 1 (𝕜 × A)` is maximal, and the norm inherited from this pullback is minimal.
+
+For possibly non-unital `RegularNormedAlgebra`s  `A` (over `𝕜`), we construct a `NormedAlgebra`
+structure on `Unitization 𝕜 A` using the pullback described above. The reason for choosing this norm
+is that for a C⋆-algebra `A` its norm is always regular, and the pullback norm on `Unitization 𝕜 A`
+is then also a C⋆-norm.
+
+## Main definitions
+
+- `Unitization.splitMul : Unitization 𝕜 A →ₐ[𝕜] (𝕜 × (A →L[𝕜] A))`: The first coordinate of this
+  map is just `Unitization.fst` and the second is the `Unitization.lift` of the left regular
+  representation of `A` (i.e., `NonUnitalAlgHom.Lmul`). We use this map to pull back the
+  `NormedRing` and `NormedAlgebra` structures.
+
+## Main statements
+
+- `Unitization.instNormedRing`, `Unitization.instNormedAlgebra`, `Unitization.instNormOneClass`,
+  `Unitization.instCompleteSpace`: when `A` is a non-unital Banach `𝕜`-algebra with a regular norm,
+  then `Unitization 𝕜 A` is a unital Banach `𝕜`-algebra with `‖1‖ = 1`.
+- `Unitization.norm_inr`, `Unitization.isometry_inr`: the natural inclusion `A → Unitization 𝕜 A`
+  is an isometry, or in mathematical parlance, the norm on `A` extends to a norm on
+  `Unitization 𝕜 A`.
+
+## Implementation details
+
+We ensure that the uniform structure, and hence also the topological structure, is definitionally
+equal to the pullback of `instUniformSpaceProd` along `Unitization.addEquiv` (this is essentially
+viewing `Unitization 𝕜 A` as `𝕜 × A`) by means of forgetful inheritance. The same is true of the
+bornology.
+
+-/
+
+variable (𝕜 A : Type*) [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A]
+variable [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A]
+
+open ContinuousLinearMap
+
+namespace Unitization
+
+/-- Given `(k, a) : Unitization 𝕜 A`, the second coordinate of `Unitization.splitMul (k, a)` is
+the natural representation of `Unitization 𝕜 A` on `A` given by multiplication on the left in
+`A →L[𝕜] A`; note that this is not just `NonUnitalAlgHom.Lmul` for a few reasons: (a) that would
+either be `A` acting on `A`, or (b) `Unitization 𝕜 A` acting on `Unitization 𝕜 A`, and (c) that's a
+`NonUnitalAlgHom` but here we need an `AlgHom`. In addition, the first coordinate of
+`Unitization.splitMul (k, a)` should just be `k`. See `Unitization.splitMul_apply` also. -/
+def splitMul : Unitization 𝕜 A →ₐ[𝕜] 𝕜 × (A →L[𝕜] A) :=
+  (lift 0).prod (lift <| NonUnitalAlgHom.Lmul 𝕜 A)
+
+variable {𝕜 A}
+
+@[simp]
+theorem splitMul_apply (x : Unitization 𝕜 A) :
+    splitMul 𝕜 A x = (x.fst, algebraMap 𝕜 (A →L[𝕜] A) x.fst + mul 𝕜 A x.snd) :=
+  show (x.fst + 0, _) = (x.fst, _) by rw [add_zero]; rfl
+
+/-- this lemma establishes that if `ContinuousLinearMap.mul 𝕜 A` is injective, then so is
+`Unitization.splitMul 𝕜 A`. When `A` is a `RegularNormedAlgebra`, then
+`ContinuousLinearMap.mul 𝕜 A` is an isometry, and is therefore automatically injective. -/
+theorem splitMul_injective_of_clm_mul_injective
+    (h : Function.Injective (mul 𝕜 A)) :
+    Function.Injective (splitMul 𝕜 A) := by
+  rw [injective_iff_map_eq_zero]
+  intro x hx
+  induction x using Unitization.ind
+  rw [map_add] at hx
+  simp only [splitMul_apply, fst_inl, snd_inl, map_zero, add_zero, fst_inr, snd_inr,
+    zero_add, Prod.mk_add_mk, Prod.mk_eq_zero] at hx
+  obtain ⟨rfl, hx⟩ := hx
+  simp only [map_zero, zero_add, inl_zero] at hx ⊢
+  rw [← map_zero (mul 𝕜 A)] at hx
+  rw [h hx, inr_zero]
+
+variable [RegularNormedAlgebra 𝕜 A]
+variable (𝕜 A)
+
+/- In a `RegularNormedAlgebra`, the map `Unitization.splitMul 𝕜 A` is injective. We will use this
+to pull back the norm from `𝕜 × (A →L[𝕜] A)` to `Unitization 𝕜 A`. -/
+theorem splitMul_injective : Function.Injective (splitMul 𝕜 A) :=
+  splitMul_injective_of_clm_mul_injective (isometry_mul 𝕜 A).injective
+
+variable {𝕜 A}
+
+section Aux
+
+/-- Pull back the normed ring structure from `𝕜 × (A →L[𝕜] A)` to `Unitization 𝕜 A` using the
+algebra homomorphism `Unitization.splitMul 𝕜 A`. This does not give us the desired topology,
+uniformity or bornology on `Unitization 𝕜 A` (which we want to agree with `Prod`), so we only use
+it as a local instance to build the real one. -/
+@[reducible]
+noncomputable def normedRingAux : NormedRing (Unitization 𝕜 A) :=
+  @NormedRing.induced _ (Unitization 𝕜 A) (𝕜 × (A →L[𝕜] A)) Unitization.instRing
+    Prod.normedRing _ (splitMul 𝕜 A) (splitMul_injective 𝕜 A)
+-- todo: why does Lean need these instances explictly?
+
+attribute [local instance] Unitization.normedRingAux
+
+/-- Pull back the normed algebra structure from `𝕜 × (A →L[𝕜] A)` to `Unitization 𝕜 A` using the
+algebra homomorphism `Unitization.splitMul 𝕜 A`. This uses the wrong `NormedRing` instance (i.e.,
+`Unitization.normedRingAux`), so we only use it as a local instance to build the real one.-/
+@[reducible]
+noncomputable def normedAlgebraAux : NormedAlgebra 𝕜 (Unitization 𝕜 A) :=
+  NormedAlgebra.induced 𝕜 (Unitization 𝕜 A) (𝕜 × (A →L[𝕜] A)) (splitMul 𝕜 A)
+
+attribute [local instance] Unitization.normedAlgebraAux
+
+theorem norm_def (x : Unitization 𝕜 A) : ‖x‖ = ‖splitMul 𝕜 A x‖ :=
+  rfl
+
+theorem nnnorm_def (x : Unitization 𝕜 A) : ‖x‖₊ = ‖splitMul 𝕜 A x‖₊ :=
+  rfl
+
+/-- This is often the more useful lemma to rewrite the norm as opposed to `Unitization.norm_def`. -/
+theorem norm_eq_sup (x : Unitization 𝕜 A) :
+    ‖x‖ = ‖x.fst‖ ⊔ ‖algebraMap 𝕜 (A →L[𝕜] A) x.fst + mul 𝕜 A x.snd‖ := by
+  rw [norm_def, splitMul_apply, Prod.norm_def, sup_eq_max]
+
+/-- This is often the more useful lemma to rewrite the norm as opposed to
+`Unitization.nnnorm_def`. -/
+theorem nnnorm_eq_sup (x : Unitization 𝕜 A) :
+    ‖x‖₊ = ‖x.fst‖₊ ⊔ ‖algebraMap 𝕜 (A →L[𝕜] A) x.fst + mul 𝕜 A x.snd‖₊ :=
+  NNReal.eq <| norm_eq_sup x
+
+
+theorem lipschitzWith_addEquiv :
+    LipschitzWith 2 (Unitization.addEquiv 𝕜 A) := by
+  rw [← Real.toNNReal_ofNat]
+  refine AddMonoidHomClass.lipschitz_of_bound (Unitization.addEquiv 𝕜 A) 2 fun x => ?_
+  rw [norm_eq_sup, Prod.norm_def]
+  refine' max_le ?_ ?_
+  · rw [sup_eq_max, mul_max_of_nonneg _ _ (zero_le_two : (0 : ℝ) ≤ 2)]
+    exact le_max_of_le_left ((le_add_of_nonneg_left (norm_nonneg _)).trans_eq (two_mul _).symm)
+  · nontriviality A
+    rw [two_mul]
+    calc
+      ‖x.snd‖ = ‖mul 𝕜 A x.snd‖ :=
+        .symm <| (isometry_mul 𝕜 A).norm_map_of_map_zero (map_zero _) _
+      _ ≤ ‖algebraMap 𝕜 _ x.fst + mul 𝕜 A x.snd‖ + ‖x.fst‖ := by
+        simpa only [add_comm _ (mul 𝕜 A x.snd), norm_algebraMap'] using
+          norm_le_add_norm_add (mul 𝕜 A x.snd) (algebraMap 𝕜 _ x.fst)
+      _ ≤ _ := add_le_add le_sup_right le_sup_left
+
+theorem antilipschitzWith_addEquiv :
+    AntilipschitzWith 2 (addEquiv 𝕜 A) := by
+  refine AddMonoidHomClass.antilipschitz_of_bound (addEquiv 𝕜 A) fun x => ?_
+  rw [norm_eq_sup, Prod.norm_def, NNReal.coe_two]
+  refine max_le ?_ ?_
+  · rw [mul_max_of_nonneg _ _ (zero_le_two : (0 : ℝ) ≤ 2)]
+    exact le_max_of_le_left ((le_add_of_nonneg_left (norm_nonneg _)).trans_eq (two_mul _).symm)
+  · nontriviality A
+    calc
+      ‖algebraMap 𝕜 _ x.fst + mul 𝕜 A x.snd‖ ≤ ‖algebraMap 𝕜 _ x.fst‖ + ‖mul 𝕜 A x.snd‖ :=
+        norm_add_le _ _
+      _ = ‖x.fst‖ + ‖x.snd‖ := by
+        rw [norm_algebraMap', (AddMonoidHomClass.isometry_iff_norm (mul 𝕜 A)).mp (isometry_mul 𝕜 A)]
+      _ ≤ _ := (add_le_add (le_max_left _ _) (le_max_right _ _)).trans_eq (two_mul _).symm
+
+open Bornology Filter
+open scoped Uniformity Topology
+
+theorem uniformity_eq_aux :
+    𝓤[instUniformSpaceProd.comap <| addEquiv 𝕜 A] = 𝓤 (Unitization 𝕜 A) := by
+  have key : UniformInducing (addEquiv 𝕜 A) :=
+    antilipschitzWith_addEquiv.uniformInducing lipschitzWith_addEquiv.uniformContinuous
+  rw [← key.comap_uniformity]
+  rfl
+
+theorem cobounded_eq_aux :
+    @cobounded _ (Bornology.induced <| addEquiv 𝕜 A) = cobounded (Unitization 𝕜 A) :=
+  le_antisymm lipschitzWith_addEquiv.comap_cobounded_le
+    antilipschitzWith_addEquiv.tendsto_cobounded.le_comap
+
+end Aux
+
+/-- The uniformity on `Unitization 𝕜 A` is inherited from `𝕜 × A`. -/
+instance instUniformSpace : UniformSpace (Unitization 𝕜 A) :=
+  instUniformSpaceProd.comap (addEquiv 𝕜 A)
+
+/-- The bornology on `Unitization 𝕜 A` is inherited from `𝕜 × A`. -/
+instance instBornology : Bornology (Unitization 𝕜 A) :=
+  Bornology.induced <| addEquiv 𝕜 A
+
+theorem uniformEmbedding_addEquiv : UniformEmbedding (addEquiv 𝕜 A) where
+  comap_uniformity := rfl
+  inj := (addEquiv 𝕜 A).injective
+
+/-- `Unitization 𝕜 A` is complete whenever `𝕜` and `A` are also.  -/
+instance instCompleteSpace [CompleteSpace 𝕜] [CompleteSpace A] :
+    CompleteSpace (Unitization 𝕜 A) :=
+  (completeSpace_congr uniformEmbedding_addEquiv).mpr CompleteSpace.prod
+
+/-- Pull back the metric structure from `𝕜 × (A →L[𝕜] A)` to `Unitization 𝕜 A` using the
+algebra homomorphism `Unitization.splitMul 𝕜 A`, but replace the bornology and the uniformity so
+that they coincide with `𝕜 × A`. -/
+noncomputable instance instMetricSpace : MetricSpace (Unitization 𝕜 A) :=
+  (normedRingAux.toMetricSpace.replaceUniformity uniformity_eq_aux).replaceBornology
+    fun s => Filter.ext_iff.1 cobounded_eq_aux (sᶜ)
+
+/-- Pull back the normed ring structure from `𝕜 × (A →L[𝕜] A)` to `Unitization 𝕜 A` using the
+algebra homomorphism `Unitization.splitMul 𝕜 A`. -/
+noncomputable instance instNormedRing : NormedRing (Unitization 𝕜 A)
+    where
+  dist_eq := normedRingAux.dist_eq
+  norm_mul := normedRingAux.norm_mul
+  norm := normedRingAux.norm
+
+/-- Pull back the normed algebra structure from `𝕜 × (A →L[𝕜] A)` to `Unitization 𝕜 A` using the
+algebra homomorphism `Unitization.splitMul 𝕜 A`. -/
+instance instNormedAlgebra : NormedAlgebra 𝕜 (Unitization 𝕜 A) where
+  norm_smul_le k x := by
+    rw [norm_def, map_smul, norm_smul, ← norm_def]
+
+instance instNormOneClass : NormOneClass (Unitization 𝕜 A) where
+  norm_one := by simpa only [norm_eq_sup, fst_one, norm_one, snd_one, map_one, map_zero,
+      add_zero, ge_iff_le, sup_eq_left] using op_norm_le_bound _ zero_le_one fun x => by simp
+
+lemma norm_inr (a : A) : ‖(a : Unitization 𝕜 A)‖ = ‖a‖ := by
+  simp [norm_eq_sup]
+
+lemma nnnorm_inr (a : A) : ‖(a : Unitization 𝕜 A)‖₊ = ‖a‖₊ :=
+  NNReal.eq <| norm_inr a
+
+lemma isometry_inr : Isometry ((↑) : A → Unitization 𝕜 A) :=
+  AddMonoidHomClass.isometry_of_norm (inrNonUnitalAlgHom 𝕜 A) norm_inr
+
+lemma dist_inr (a b : A) : dist (a : Unitization 𝕜 A) (b : Unitization 𝕜 A) = dist a b :=
+  isometry_inr.dist_eq a b
+
+lemma nndist_inr (a b : A) : nndist (a : Unitization 𝕜 A) (b : Unitization 𝕜 A) = nndist a b :=
+  isometry_inr.nndist_eq a b
+
+/- These examples verify that the bornology and uniformity (hence also the topology) are the
+correct ones. -/
+example : (instNormedRing (𝕜 := 𝕜) (A := A)).toMetricSpace = instMetricSpace := rfl
+example : (instMetricSpace (𝕜 := 𝕜) (A := A)).toBornology = instBornology := rfl
+example : (instMetricSpace (𝕜 := 𝕜) (A := A)).toUniformSpace = instUniformSpace := rfl
+
+end Unitization