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

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 = AlgHom.prod (Unitization.lift 0) (Unitization.lift (NonUnitalAlgHom.Lmul 𝕜 A))

@[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) : (Unitization.splitMul 𝕜 A) x = (Unitization.fst x, (algebraMap 𝕜 (A →L[𝕜] A)) (Unitization.fst x) + (ContinuousLinearMap.mul 𝕜 A) (Unitization.snd x))

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 ⇑(Unitization.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.

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 ⇑(Unitization.splitMul 𝕜 A)

@[reducible]

noncomputable def 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) ⋯

@[reducible]

noncomputable def 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)

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‖ = ‖(Unitization.splitMul 𝕜 A) x‖

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‖₊ = ‖(Unitization.splitMul 𝕜 A) x‖₊

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‖ = ‖Unitization.fst x‖ ⊔ ‖(algebraMap 𝕜 (A →L[𝕜] A)) (Unitization.fst x) + (ContinuousLinearMap.mul 𝕜 A) (Unitization.snd x)‖

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

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‖₊ = ‖Unitization.fst x‖₊ ⊔ ‖(algebraMap 𝕜 (A →L[𝕜] A)) (Unitization.fst x) + (ContinuousLinearMap.mul 𝕜 A) (Unitization.snd x)‖₊

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

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 ⇑(Unitization.addEquiv 𝕜 A)

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 ⇑(Unitization.addEquiv 𝕜 A)

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)

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)

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

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)

theorem Unitization.uniformEmbedding_addEquiv {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] : UniformEmbedding ⇑(Unitization.addEquiv 𝕜 A)

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

Equations

• ⋯ = ⋯

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 = MetricSpace.replaceBornology (MetricSpace.replaceUniformity NormedRing.toMetricSpace ⋯) ⋯

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 = NormedRing.mk ⋯ ⋯

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 = NormedAlgebra.mk ⋯

noncomputable 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)

Equations

• ⋯ = ⋯

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‖

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‖₊

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 Unitization.inr

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 : A) (b : A) : dist ↑a ↑b = dist a b

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 : A) (b : A) : nndist ↑a ↑b = nndist a b