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.

Equations

• WithLp.unitization_addEquiv_prod 𝕜 A = (WithLp.linearEquiv 1 𝕜 (Unitization 𝕜 A)).toAddEquiv.trans ((Unitization.addEquiv 𝕜 A).trans (WithLp.linearEquiv 1 𝕜 (𝕜 × A)).symm.toAddEquiv)

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

Equations

• WithLp.instUnitizationNormedAddCommGroup 𝕜 A = NormedAddCommGroup.induced (WithLp 1 (Unitization 𝕜 A)) (WithLp 1 (𝕜 × A)) (WithLp.unitization_addEquiv_prod 𝕜 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.

Equations

• WithLp.uniformEquiv_unitization_addEquiv_prod 𝕜 A = { toEquiv := (WithLp.unitization_addEquiv_prod 𝕜 A).toEquiv, uniformContinuous_toFun := ⋯, uniformContinuous_invFun := ⋯ }

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‖ = ‖((WithLp.equiv 1 (Unitization 𝕜 A)) x).fst‖ + ‖((WithLp.equiv 1 (Unitization 𝕜 A)) x).snd‖

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

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

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

theorem WithLp.unitization_isometry_inr {𝕜 : Type u_1} {A : Type u_2} [NormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] : Isometry fun (x : A) => (WithLp.equiv 1 (Unitization 𝕜 A)).symm ↑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))

Equations

• WithLp.instUnitizationRing = inferInstanceAs (Ring (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)) : (WithLp.equiv 1 (Unitization 𝕜 A)) (x * y) = (WithLp.equiv 1 (Unitization 𝕜 A)) x * (WithLp.equiv 1 (Unitization 𝕜 A)) y

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

Equations

• WithLp.instAlgebraOfNatENNRealUnitizationOfIsScalarTower = inferInstanceAs (Algebra R (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 : 𝕜) : (WithLp.equiv 1 (Unitization 𝕜 A)) ((algebraMap 𝕜 (WithLp 1 (Unitization 𝕜 A))) r) = (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

WithLp.equiv bundled as an algebra isomorphism with Unitization 𝕜 A.

Equations

• WithLp.unitizationAlgEquiv R = { toEquiv := WithLp.equiv 1 (Unitization 𝕜 A), map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

@[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)) : (WithLp.unitizationAlgEquiv R) a = a

@[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 : WithLp 1 (Unitization 𝕜 A)) : (WithLp.unitizationAlgEquiv R).symm a = 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))

Equations

• WithLp.instUnitizationNormedRing = NormedRing.mk ⋯ ⋯

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

Equations

• WithLp.instUnitizationNormedAlgebra = NormedAlgebra.mk ⋯