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:

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 #

Main statements #

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

Instances For
    @[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)) :

    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] :
    @[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.

    Instances For
      @[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.

      Instances For
        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) :
        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) :
        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) :

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

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

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

        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.

        instance Unitization.instCompleteSpace {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [CompleteSpace 𝕜] [CompleteSpace A] :

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

        noncomputable instance Unitization.instMetricSpace {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [RegularNormedAlgebra 𝕜 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.

        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.

        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.

        instance Unitization.instNormOneClass {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [RegularNormedAlgebra 𝕜 A] :
        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) :
        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) :
        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