Documentation

Mathlib.Analysis.Normed.Algebra.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). This is implemented for the type synonym WithLp 1 (Unitization ๐•œ A) in WithLp.instUnitizationNormedAddCommGroup, and it is shown there that this is a Banach algebra. 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. Of course, this means that WithLp.equiv : WithLp 1 (Unitization ๐•œ A) โ†’ Unitization ๐•œ A can be upgraded to a continuous linear equivalence (when ๐•œ and A are complete).

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.

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

Equations
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 = (x.fst, (algebraMap ๐•œ (A โ†’L[๐•œ] A)) x.fst + (ContinuousLinearMap.mul ๐•œ A) x.snd)
    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] :

    In a RegularNormedAlgebra, the map Unitization.splitMul ๐•œ A is injective. We will use this to pull back the norm from ๐•œ ร— (A โ†’L[๐•œ] A) to Unitization ๐•œ A.

    @[reducible, inline]
    noncomputable abbrev 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.

    Equations
    Instances For
      @[reducible, inline]
      noncomputable abbrev 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.

      Equations
      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) :
        โ€–xโ€– = โ€–x.fstโ€– โŠ” โ€–(algebraMap ๐•œ (A โ†’L[๐•œ] A)) x.fst + (ContinuousLinearMap.mul ๐•œ A) x.sndโ€–

        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] :
        noncomputable instance Unitization.instUniformSpace {๐•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField ๐•œ] [NonUnitalNormedRing A] :

        The uniformity on Unitization ๐•œ A is inherited from ๐•œ ร— A.

        Equations
        noncomputable def Unitization.uniformEquivProd {๐•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField ๐•œ] [NonUnitalNormedRing A] :
        Unitization ๐•œ A โ‰ƒแตค ๐•œ ร— A

        The natural equivalence between Unitization ๐•œ A and ๐•œ ร— A as a uniform equivalence.

        Equations
        • Unitization.uniformEquivProd = (โ†‘(Unitization.addEquiv ๐•œ A)).toUniformEquivOfUniformInducing โ‹ฏ
        Instances For
          noncomputable 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.

          Equations
          noncomputable 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.

          Equations
          • โ‹ฏ = โ‹ฏ
          noncomputable instance Unitization.instMetricSpace {๐•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField ๐•œ] [NonUnitalNormedRing A] [NormedSpace ๐•œ A] [IsScalarTower ๐•œ A A] [SMulCommClass ๐•œ A A] [RegularNormedAlgebra ๐•œ A] :
          MetricSpace (Unitization ๐•œ 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.

          Equations
          • Unitization.instMetricSpace = (NormedRing.toMetricSpace.replaceUniformity โ‹ฏ).replaceBornology โ‹ฏ
          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.

          Equations
          noncomputable 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.

          Equations
          noncomputable instance Unitization.instNormOneClass {๐•œ : Type u_1} {A : Type u_2} [NontriviallyNormedField ๐•œ] [NonUnitalNormedRing A] [NormedSpace ๐•œ A] [IsScalarTower ๐•œ A A] [SMulCommClass ๐•œ A A] [RegularNormedAlgebra ๐•œ A] :
          Equations
          • โ‹ฏ = โ‹ฏ
          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