# Documentation

Mathlib.Analysis.NormedSpace.Unitization

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

def Unitization.splitMul (𝕜 : Type u_1) (A : Type u_2) [] [] [] :
→ₐ[𝕜] 𝕜 × (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.

Instances For
@[simp]
theorem Unitization.splitMul_apply {𝕜 : Type u_1} {A : Type u_2} [] [] [] (x : ) :
↑() x = (, ↑(algebraMap 𝕜 (A →L[𝕜] A)) () + ↑() ())
theorem Unitization.splitMul_injective_of_clm_mul_injective {𝕜 : Type u_1} {A : Type u_2} [] [] [] (h : ) :

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) [] [] [] [] :
@[reducible]
noncomputable def Unitization.normedRingAux {𝕜 : Type u_1} {A : Type u_2} [] [] [] [] :

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.

Instances For
@[reducible]
noncomputable def Unitization.normedAlgebraAux {𝕜 : Type u_1} {A : Type u_2} [] [] [] [] :

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.

Instances For
theorem Unitization.norm_def {𝕜 : Type u_1} {A : Type u_2} [] [] [] [] (x : ) :
x = ↑() x
theorem Unitization.nnnorm_def {𝕜 : Type u_1} {A : Type u_2} [] [] [] [] (x : ) :
theorem Unitization.norm_eq_sup {𝕜 : Type u_1} {A : Type u_2} [] [] [] [] (x : ) :
x = ↑(algebraMap 𝕜 (A →L[𝕜] A)) () + ↑() ()

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} [] [] [] [] (x : ) :
x‖₊ = ↑(algebraMap 𝕜 (A →L[𝕜] A)) () + ↑() ()‖₊

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} [] [] [] [] :
theorem Unitization.antilipschitzWith_addEquiv {𝕜 : Type u_1} {A : Type u_2} [] [] [] [] :
theorem Unitization.uniformity_eq_aux {𝕜 : Type u_1} {A : Type u_2} [] [] [] [] :
theorem Unitization.cobounded_eq_aux {𝕜 : Type u_1} {A : Type u_2} [] [] [] [] :
instance Unitization.instUniformSpace {𝕜 : Type u_1} {A : Type u_2} :

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

instance Unitization.instBornology {𝕜 : Type u_1} {A : Type u_2} :

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

theorem Unitization.uniformEmbedding_addEquiv {𝕜 : Type u_1} {A : Type u_2} :
instance Unitization.instCompleteSpace {𝕜 : Type u_1} {A : Type u_2} [] [] :

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

noncomputable instance Unitization.instMetricSpace {𝕜 : Type u_1} {A : Type u_2} [] [] [] [] :

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 Unitization.instNormedRing {𝕜 : Type u_1} {A : Type u_2} [] [] [] [] :

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

instance Unitization.instNormedAlgebra {𝕜 : Type u_1} {A : Type u_2} [] [] [] [] :

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

instance Unitization.instNormOneClass {𝕜 : Type u_1} {A : Type u_2} [] [] [] [] :
theorem Unitization.norm_inr {𝕜 : Type u_1} {A : Type u_2} [] [] [] [] (a : A) :
theorem Unitization.nnnorm_inr {𝕜 : Type u_1} {A : Type u_2} [] [] [] [] (a : A) :
theorem Unitization.isometry_inr {𝕜 : Type u_1} {A : Type u_2} [] [] [] [] :
Isometry Unitization.inr
theorem Unitization.dist_inr {𝕜 : Type u_1} {A : Type u_2} [] [] [] [] (a : A) (b : A) :
dist a b = dist a b
theorem Unitization.nndist_inr {𝕜 : Type u_1} {A : Type u_2} [] [] [] [] (a : A) (b : A) :
nndist a b = nndist a b