# 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). This is implemented for the type synonym `WithLp 1 (Unitization 𝕜 A)` in `WithLp.instUnitizationNormedAddCommGroup`, and it is shown there that this is a Banach algebra. 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. Of course, this means that `WithLp.equiv : WithLp 1 (Unitization 𝕜 A) → Unitization 𝕜 A` can be upgraded to a continuous linear equivalence (when `𝕜` and `A` are complete).

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.

source
noncomputable def Unitization.splitMul (𝕜 : Type u_1) (A : Type u_2) [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] :
Unitization 𝕜 A →ₐ[𝕜] 𝕜 × (A →L[𝕜] A)

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.

Equations

- Unitization.splitMul 𝕜 A = (Unitization.lift 0).prod (Unitization.lift (NonUnitalAlgHom.Lmul 𝕜 A))

Instances For

source
@[simp]
theorem Unitization.splitMul_apply {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] (x : Unitization 𝕜 A) :
(splitMul 𝕜 A) x = (x.fst, (algebraMap 𝕜 (A →L[𝕜] A)) x.fst + (ContinuousLinearMap.mul 𝕜 A) x.snd)
source
theorem Unitization.splitMul_injective_of_clm_mul_injective {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] (h : Function.Injective ⇑(ContinuousLinearMap.mul 𝕜 A)) :
Function.Injective ⇑(splitMul 𝕜 A)

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.

source
theorem Unitization.splitMul_injective (𝕜 : Type u_1) (A : Type u_2) [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [RegularNormedAlgebra 𝕜 A] :
Function.Injective ⇑(splitMul 𝕜 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`.

source
@[reducible, inline]
noncomputable abbrev Unitization.normedRingAux {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [RegularNormedAlgebra 𝕜 A] :
NormedRing (Unitization 𝕜 A)

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.

Equations

- Unitization.normedRingAux = NormedRing.induced (Unitization 𝕜 A) (𝕜 × (A →L[𝕜] A)) (Unitization.splitMul 𝕜 A) ⋯

Instances For

source
@[reducible, inline]
noncomputable abbrev Unitization.normedAlgebraAux {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [RegularNormedAlgebra 𝕜 A] :
NormedAlgebra 𝕜 (Unitization 𝕜 A)

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.

Equations

- Unitization.normedAlgebraAux = NormedAlgebra.induced 𝕜 (Unitization 𝕜 A) (𝕜 × (A →L[𝕜] A)) (Unitization.splitMul 𝕜 A)

Instances For

source
theorem Unitization.norm_def {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [RegularNormedAlgebra 𝕜 A] (x : Unitization 𝕜 A) :
‖x‖ = ‖(splitMul 𝕜 A) x‖
source
theorem Unitization.nnnorm_def {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [RegularNormedAlgebra 𝕜 A] (x : Unitization 𝕜 A) :
‖x‖₊ = ‖(splitMul 𝕜 A) x‖₊
source
theorem Unitization.norm_eq_sup {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [RegularNormedAlgebra 𝕜 A] (x : Unitization 𝕜 A) :
‖x‖ = max ‖x.fst‖ ‖(algebraMap 𝕜 (A →L[𝕜] A)) x.fst + (ContinuousLinearMap.mul 𝕜 A) x.snd‖

This is often the more useful lemma to rewrite the norm as opposed to `Unitization.norm_def`.

source
theorem Unitization.nnnorm_eq_sup {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [RegularNormedAlgebra 𝕜 A] (x : Unitization 𝕜 A) :
‖x‖₊ = max ‖x.fst‖₊ ‖(algebraMap 𝕜 (A →L[𝕜] A)) x.fst + (ContinuousLinearMap.mul 𝕜 A) x.snd‖₊

This is often the more useful lemma to rewrite the norm as opposed to `Unitization.nnnorm_def`.

source
theorem Unitization.lipschitzWith_addEquiv {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [RegularNormedAlgebra 𝕜 A] :
LipschitzWith 2 ⇑(addEquiv 𝕜 A)
source
theorem Unitization.antilipschitzWith_addEquiv {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [RegularNormedAlgebra 𝕜 A] :
AntilipschitzWith 2 ⇑(addEquiv 𝕜 A)
source
theorem Unitization.uniformity_eq_aux {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [RegularNormedAlgebra 𝕜 A] :
uniformity (Unitization 𝕜 A) = uniformity (Unitization 𝕜 A)
source
theorem Unitization.cobounded_eq_aux {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [RegularNormedAlgebra 𝕜 A] :
Bornology.cobounded (Unitization 𝕜 A) = Bornology.cobounded (Unitization 𝕜 A)
source
noncomputable instance Unitization.instUniformSpace {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] :
UniformSpace (Unitization 𝕜 A)

The uniformity on `Unitization 𝕜 A` is inherited from `𝕜 × A`.

Equations

- Unitization.instUniformSpace = UniformSpace.comap (⇑(Unitization.addEquiv 𝕜 A)) instUniformSpaceProd

source
noncomputable def Unitization.uniformEquivProd {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] :
Unitization 𝕜 A ≃ᵤ 𝕜 × A

The natural equivalence between `Unitization 𝕜 A` and `𝕜 × A` as a uniform equivalence.

Equations

- Unitization.uniformEquivProd = (↑(Unitization.addEquiv 𝕜 A)).toUniformEquivOfIsUniformInducing ⋯

Instances For

source
noncomputable instance Unitization.instBornology {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] :
Bornology (Unitization 𝕜 A)

The bornology on `Unitization 𝕜 A` is inherited from `𝕜 × A`.

Equations

- Unitization.instBornology = Bornology.induced ⇑(Unitization.addEquiv 𝕜 A)

source
theorem Unitization.isUniformEmbedding_addEquiv {A : Type u_2} [NonUnitalNormedRing A] {𝕜 : Type u_3} [NontriviallyNormedField 𝕜] :
IsUniformEmbedding ⇑(addEquiv 𝕜 A)
source
instance Unitization.instCompleteSpace {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [CompleteSpace 𝕜] [CompleteSpace A] :
CompleteSpace (Unitization 𝕜 A)

`Unitization 𝕜 A` is complete whenever `𝕜` and `A` are also.

source
noncomputable instance Unitization.instMetricSpace {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [RegularNormedAlgebra 𝕜 A] :
MetricSpace (Unitization 𝕜 A)

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`.

Equations

- Unitization.instMetricSpace = (Unitization.normedRingAux.replaceUniformity ⋯).replaceBornology ⋯

source
noncomputable instance Unitization.instNormedRing {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [RegularNormedAlgebra 𝕜 A] :
NormedRing (Unitization 𝕜 A)

Pull back the normed ring structure from `𝕜 × (A →L[𝕜] A)` to `Unitization 𝕜 A` using the algebra homomorphism `Unitization.splitMul 𝕜 A`.

Equations

- Unitization.instNormedRing = { toNorm := Unitization.normedRingAux.toNorm, toRing := Unitization.instRing, toMetricSpace := Unitization.instMetricSpace, dist_eq := ⋯, norm_mul_le := ⋯ }

source
noncomputable instance Unitization.instNormedAlgebra {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [RegularNormedAlgebra 𝕜 A] :
NormedAlgebra 𝕜 (Unitization 𝕜 A)

Pull back the normed algebra structure from `𝕜 × (A →L[𝕜] A)` to `Unitization 𝕜 A` using the algebra homomorphism `Unitization.splitMul 𝕜 A`.

Equations

- Unitization.instNormedAlgebra = { toAlgebra := Unitization.instAlgebra 𝕜 𝕜 A, norm_smul_le := ⋯ }

source
instance Unitization.instNormOneClass {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [RegularNormedAlgebra 𝕜 A] :
NormOneClass (Unitization 𝕜 A)
source
theorem Unitization.norm_inr {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [RegularNormedAlgebra 𝕜 A] (a : A) :
‖↑a‖ = ‖a‖
source
theorem Unitization.nnnorm_inr {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [RegularNormedAlgebra 𝕜 A] (a : A) :
‖↑a‖₊ = ‖a‖₊
source
theorem Unitization.isometry_inr {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [RegularNormedAlgebra 𝕜 A] :
Isometry inr
source
theorem Unitization.continuous_inr {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [RegularNormedAlgebra 𝕜 A] :
Continuous inr
source
theorem Unitization.dist_inr {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [RegularNormedAlgebra 𝕜 A] (a b : A) :
dist ↑a ↑b = dist a b
source
theorem Unitization.nndist_inr {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [RegularNormedAlgebra 𝕜 A] (a b : A) :
nndist ↑a ↑b = nndist a b