Unitization equipped with the $L^1$ norm

In another file, the Unitization 𝕜 A of a non-unital normed 𝕜-algebra A is equipped with the norm inherited as the pullback via a map (closely related to) the left-regular representation of the algebra on itself (see Unitization.instNormedRing).

However, this construction is only valid (and an isometry) when A is a RegularNormedAlgebra. Sometimes it is useful to consider the unitization of a non-unital algebra with the $L^1$ norm instead. This file provides that norm on the type synonym WithLp 1 (Unitization 𝕜 A), along with the algebra isomomorphism between Unitization 𝕜 A and WithLp 1 (Unitization 𝕜 A). Note that TrivSqZeroExt is also equipped with the $L^1$ norm in the analogous way, but it is registered as an instance without the type synonym.

One application of this is a straightforward proof that the quasispectrum of an element in a non-unital Banach algebra is compact, which can be established by passing to the unitization.

noncomputable def WithLp.unitization_addEquiv_prod (𝕜 : Type u_1) (A : Type u_2) [NormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] : WithLp 1 (Unitization 𝕜 A) ≃+ WithLp 1 (𝕜 × A)

The natural map between Unitization 𝕜 A and 𝕜 × A, transferred to their WithLp 1 synonyms.

noncomputable instance WithLp.instUnitizationNormedAddCommGroup (𝕜 : Type u_1) (A : Type u_2) [NormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] : NormedAddCommGroup (WithLp 1 (Unitization 𝕜 A))

noncomputable def WithLp.uniformEquiv_unitization_addEquiv_prod (𝕜 : Type u_1) (A : Type u_2) [NormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] : WithLp 1 (Unitization 𝕜 A) ≃ᵤ WithLp 1 (𝕜 × A)

Bundle WithLp.unitization_addEquiv_prod as a UniformEquiv.

instance WithLp.instCompleteSpace (𝕜 : Type u_1) (A : Type u_2) [NormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [CompleteSpace 𝕜] [CompleteSpace A] : CompleteSpace (WithLp 1 (Unitization 𝕜 A))

theorem WithLp.unitization_norm_def {𝕜 : Type u_1} {A : Type u_2} [NormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] (x : WithLp 1 (Unitization 𝕜 A)) : ‖x‖ = ‖x.ofLp.fst‖ + ‖x.ofLp.snd‖

theorem WithLp.unitization_nnnorm_def {𝕜 : Type u_1} {A : Type u_2} [NormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] (x : WithLp 1 (Unitization 𝕜 A)) : ‖x‖₊ = ‖x.ofLp.fst‖₊ + ‖x.ofLp.snd‖₊

theorem WithLp.unitization_norm_inr {𝕜 : Type u_1} {A : Type u_2} [NormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] (x : A) : ‖toLp 1 ↑x‖ = ‖x‖

theorem WithLp.unitization_nnnorm_inr {𝕜 : Type u_1} {A : Type u_2} [NormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] (x : A) : ‖toLp 1 ↑x‖₊ = ‖x‖₊

theorem WithLp.unitization_isometry_inr {𝕜 : Type u_1} {A : Type u_2} [NormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] : Isometry fun (x : A) => toLp 1 ↑x

instance WithLp.instUnitizationRing {𝕜 : Type u_1} {A : Type u_2} [NormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] : Ring (WithLp 1 (Unitization 𝕜 A))

@[simp]

theorem WithLp.unitization_mul {𝕜 : Type u_1} {A : Type u_2} [NormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] (x y : WithLp 1 (Unitization 𝕜 A)) : (x * y).ofLp = x.ofLp * y.ofLp

instance WithLp.instAlgebraOfNatENNRealUnitizationOfIsScalarTower {𝕜 : Type u_1} {A : Type u_2} [NormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] {R : Type u_3} [CommSemiring R] [Algebra R 𝕜] [DistribMulAction R A] [IsScalarTower R 𝕜 A] : Algebra R (WithLp 1 (Unitization 𝕜 A))

@[simp]

theorem WithLp.unitization_algebraMap {𝕜 : Type u_1} {A : Type u_2} [NormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] (r : 𝕜) : ((algebraMap 𝕜 (WithLp 1 (Unitization 𝕜 A))) r).ofLp = (algebraMap 𝕜 (Unitization 𝕜 A)) r

def WithLp.unitizationAlgEquiv {𝕜 : Type u_1} {A : Type u_2} [NormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] (R : Type u_3) [CommSemiring R] [Algebra R 𝕜] [DistribMulAction R A] [IsScalarTower R 𝕜 A] : WithLp 1 (Unitization 𝕜 A) ≃ₐ[R] Unitization 𝕜 A

equiv bundled as an algebra isomorphism with Unitization 𝕜 A.

@[simp]

theorem WithLp.unitizationAlgEquiv_apply {𝕜 : Type u_1} {A : Type u_2} [NormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] (R : Type u_3) [CommSemiring R] [Algebra R 𝕜] [DistribMulAction R A] [IsScalarTower R 𝕜 A] (a✝ : WithLp 1 (Unitization 𝕜 A)) : (unitizationAlgEquiv R) a✝ = a✝.ofLp

@[simp]

theorem WithLp.unitizationAlgEquiv_symm_apply {𝕜 : Type u_1} {A : Type u_2} [NormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] (R : Type u_3) [CommSemiring R] [Algebra R 𝕜] [DistribMulAction R A] [IsScalarTower R 𝕜 A] (a✝ : Unitization 𝕜 A) : (unitizationAlgEquiv R).symm a✝ = toLp 1 a✝

noncomputable instance WithLp.instUnitizationNormedRing {𝕜 : Type u_1} {A : Type u_2} [NormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] : NormedRing (WithLp 1 (Unitization 𝕜 A))

noncomputable instance WithLp.instUnitizationNormedAlgebra {𝕜 : Type u_1} {A : Type u_2} [NormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] : NormedAlgebra 𝕜 (WithLp 1 (Unitization 𝕜 A))