Documentation

Mathlib.Analysis.Normed.Algebra.UnitizationL1

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
Instances For
    noncomputable instance WithLp.instUnitizationNormedAddCommGroup (๐•œ : Type u_1) (A : Type u_2) [NormedField ๐•œ] [NonUnitalNormedRing A] [NormedSpace ๐•œ A] :
    Equations
    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
    Instances For
      instance WithLp.instCompleteSpace (๐•œ : Type u_1) (A : Type u_2) [NormedField ๐•œ] [NonUnitalNormedRing A] [NormedSpace ๐•œ A] [CompleteSpace ๐•œ] [CompleteSpace A] :
      CompleteSpace (WithLp 1 (Unitization ๐•œ A))
      Equations
      • โ‹ฏ = โ‹ฏ
      theorem WithLp.unitization_norm_def {๐•œ : Type u_1} {A : Type u_2} [NormedField ๐•œ] [NonUnitalNormedRing A] [NormedSpace ๐•œ A] (x : WithLp 1 (Unitization ๐•œ A)) :
      theorem WithLp.unitization_nnnorm_def {๐•œ : Type u_1} {A : Type u_2} [NormedField ๐•œ] [NonUnitalNormedRing A] [NormedSpace ๐•œ A] (x : WithLp 1 (Unitization ๐•œ A)) :
      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) :
      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
      @[simp]
      theorem WithLp.unitization_mul {๐•œ : Type u_1} {A : Type u_2} [NormedField ๐•œ] [NonUnitalNormedRing A] [NormedSpace ๐•œ A] [IsScalarTower ๐•œ A A] [SMulCommClass ๐•œ A A] (x : WithLp 1 (Unitization ๐•œ A)) (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
      @[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
      @[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)) :
      @[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)) :
      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
      Instances For
        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
        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