Unitization.splitMul_injective_of_clm_mul_injective
theorem Unitization.splitMul_injective_of_clm_mul_injective :
β {π : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField π] [inst_1 : NonUnitalNormedRing A]
[inst_2 : NormedSpace π A] [inst_3 : IsScalarTower π A A] [inst_4 : SMulCommClass π A A],
Function.Injective β(ContinuousLinearMap.mul π A) β Function.Injective β(Unitization.splitMul π A)
This theorem states that for any non-trivially normed field `π` and any non-unital normed ring `A` with `A` being a normed space over `π` and `A` being a scalar tower and a commutative left `π`-module, if the multiplication operation in `A` as a continuous linear map on `π`, denoted `ContinuousLinearMap.mul π A`, is injective (meaning that different inputs produce different outputs), then the split multiplication operation in the unitization of `A`, denoted `Unitization.splitMul π A`, is also injective. When `A` is a RegularNormedAlgebra, then `ContinuousLinearMap.mul π A` is an isometry and is therefore automatically injective.
More concisely: If `π` is a non-trivially normed field, `A` is a non-unital normed ring over `π` that is a scalar tower, commutative left `π`-module, and the multiplication operation in `A` as a continuous linear map is injective, then the split multiplication operation in the unitization of `A` is also injective.
|
Unitization.norm_eq_sup
theorem Unitization.norm_eq_sup :
β {π : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField π] [inst_1 : NonUnitalNormedRing A]
[inst_2 : NormedSpace π A] [inst_3 : IsScalarTower π A A] [inst_4 : SMulCommClass π A A]
[inst_5 : RegularNormedAlgebra π A] (x : Unitization π A),
βxβ = βx.fstβ β β(algebraMap π (A βL[π] A)) x.fst + (ContinuousLinearMap.mul π A) x.sndβ
The theorem `Unitization.norm_eq_sup` states that for any non-trivially normed field `π` and a non-unitual normed ring `A` which is a normed space over `π` and forms a normed algebra regular over `π`, the norm of any element `x` in the unitization of `π` and `A` equals the supremum of the norm of the first component of `x` and the norm of the sum of the algebra map of the first component of `x` and the multiplication of the second component of `x` under the continuous linear map. This lemma is often used to rewrite the norm in unitization, and is more useful than `Unitization.norm_def`.
More concisely: For any non-trivially normed field `π`, normed ring `A` over `π` that is a normed algebra and regular over `π`, the norm of an element `x` in the unitization of `π` and `A` is equal to the supremum of the norm of `x`'s first component and the norm of `x`'s first component multiplied by the algebra map of `π` plus the norm of `x`'s second component multiplied by the algebra map.
|
Unitization.nnnorm_eq_sup
theorem Unitization.nnnorm_eq_sup :
β {π : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField π] [inst_1 : NonUnitalNormedRing A]
[inst_2 : NormedSpace π A] [inst_3 : IsScalarTower π A A] [inst_4 : SMulCommClass π A A]
[inst_5 : RegularNormedAlgebra π A] (x : Unitization π A),
βxββ = βx.fstββ β β(algebraMap π (A βL[π] A)) x.fst + (ContinuousLinearMap.mul π A) x.sndββ
This theorem states that for any non-trivially normed field `π` and a non-unital normed ring `A` that is a normed space over `π` and also forms a scalar tower and a commutative multiplication, and assuming that `A` is a regular normed algebra over `π`, the non-negative norm of any element `x` from the minimal unitization of `π` and `A` is equal to the supremum of the non-negative norm of the first element of `x` and the non-negative norm of the sum of the algebra embedding of the first element of `x` and the continuous bilinear multiplication of the second element of `x`.
More concisely: For a regularly normed algebra over a non-trivially normed field, the norm of an element in the minimal unitization is equal to the supremum of the norms of its first component and the algebra product of its first component and second component.
|