Unitizations of closed nonunital subalgebras

For a closed nonunital subalgebra B of a Banach algebra A which does not contain 1, the map (r, b) ↦ r • 1 + b identifies its external ℓ¹ unitization with the closed unital subalgebra Algebra.adjoin 𝕜 (B : Set A) = B + 𝕜 1 inside A. The identification and its inverse are bounded; the inherited norm need not equal the ℓ¹ norm.

The ℓ¹ unitization of a commutative normed algebra is moreover a commutative normed ring (WithLp.instUnitizationNormedCommRing).

The canonical inclusion and nonunital coordinate projection of the ℓ¹ unitization are also bundled as bounded linear maps.

No normalization of the norm of the identity is assumed. The forward map is bounded by max ‖(1 : A)‖ 1, so the results apply to any complete nontrivially normed scalar field.

References

• Dales, Banach Algebras and Automatic Continuity, §§1.3–1.5.
• The algebraic identification is Mathlib's NonUnitalSubalgebra.unitizationAlgEquiv; the ℓ¹ norm is Mathlib's WithLp.unitization_norm_def.

theorem NonUnitalSubalgebra.norm_unitization_le {𝕜 : Type u_1} {A : Type u_2} [NormedField 𝕜] [NormedRing A] [NormedAlgebra 𝕜 A] (B : NonUnitalSubalgebra 𝕜 A) (x : WithLp 1 (Unitization 𝕜 ↥B)) : ‖(unitization B) x.ofLp‖ ≤ max ‖1‖ 1 * ‖x‖

The natural unitization map is bounded for the ℓ¹ norm, without normalizing ‖1‖.

theorem NonUnitalSubalgebra.continuous_unitization {𝕜 : Type u_1} {A : Type u_2} [NormedField 𝕜] [NormedRing A] [NormedAlgebra 𝕜 A] (B : NonUnitalSubalgebra 𝕜 A) : Continuous fun (x : WithLp 1 (Unitization 𝕜 ↥B)) => (unitization B) x.ofLp

Continuity of the natural map from the external ℓ¹ unitization into the ambient algebra.

theorem NonUnitalSubalgebra.isClosed_adjoin {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [Ring A] [TopologicalSpace A] [IsTopologicalAddGroup A] [Algebra 𝕜 A] [ContinuousSMul 𝕜 A] (B : NonUnitalSubalgebra 𝕜 A) (hB : IsClosed ↑B) : IsClosed ↑(Algebra.adjoin 𝕜 ↑B)

Adjoining the identity to a closed nonunital subalgebra gives a closed subalgebra. Its underlying vector subspace is B.toSubmodule ⊔ 𝕜 ∙ (1 : A).

noncomputable def NonUnitalSubalgebra.unitizationContinuousAlgEquiv {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [NormedRing A] [NormedAlgebra 𝕜 A] [CompleteSpace A] (B : NonUnitalSubalgebra 𝕜 A) (hB : IsClosed ↑B) (h1 : 1 ∉ B) : WithLp 1 (Unitization 𝕜 ↥B) ≃A[𝕜] ↥(Algebra.adjoin 𝕜 ↑B)

A closed nonunital subalgebra omitting the ambient identity has its external ℓ¹ unitization boundedly isomorphic to its unital closure with the inherited norm.

theorem NonUnitalSubalgebra.unitizationContinuousAlgEquiv_toAlgEquiv {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [NormedRing A] [NormedAlgebra 𝕜 A] [CompleteSpace A] (B : NonUnitalSubalgebra 𝕜 A) (hB : IsClosed ↑B) (h1 : 1 ∉ B) : (B.unitizationContinuousAlgEquiv hB h1).toAlgEquiv = (WithLp.unitizationAlgEquiv 𝕜).trans (unitizationAlgEquiv B h1)

The continuous unitization identification has the standard algebraic identification as its underlying algebra equivalence, so its inverse is the same algebraic inverse.

@[simp]

theorem NonUnitalSubalgebra.unitizationContinuousAlgEquiv_apply_coe {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [NormedRing A] [NormedAlgebra 𝕜 A] [CompleteSpace A] (B : NonUnitalSubalgebra 𝕜 A) (hB : IsClosed ↑B) (h1 : 1 ∉ B) (x : WithLp 1 (Unitization 𝕜 ↥B)) : ↑((B.unitizationContinuousAlgEquiv hB h1) x) = (algebraMap 𝕜 A) x.ofLp.toProd.1 + ↑x.ofLp.toProd.2

The bounded identification sends the two unitization coordinates to their sum in A.

@[simp]

theorem NonUnitalSubalgebra.unitizationContinuousAlgEquiv_symm_apply {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [NormedRing A] [NormedAlgebra 𝕜 A] [CompleteSpace A] (B : NonUnitalSubalgebra 𝕜 A) (hB : IsClosed ↑B) (h1 : 1 ∉ B) (r : 𝕜) (b : ↥B) {h : (algebraMap 𝕜 A) r + ↑b ∈ Algebra.adjoin 𝕜 ↑B} : (B.unitizationContinuousAlgEquiv hB h1).symm ⟨(algebraMap 𝕜 A) r + ↑b, h⟩ = WithLp.toLp 1 (Unitization.inl r + ↑b)

The inverse bounded identification recovers the scalar and nonunital coordinates.

noncomputable def WithLp.unitizationInrL (𝕜 : Type u_1) (A : Type u_2) [NormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] : A →L[𝕜] WithLp 1 (Unitization 𝕜 A)

The isometric inclusion into the external ℓ¹ unitization as a bounded linear map.

@[simp]

theorem WithLp.unitizationInrL_apply (𝕜 : Type u_1) (A : Type u_2) [NormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] (a : A) : (unitizationInrL 𝕜 A) a = toLp 1 ↑a

The bounded inclusion is the usual inclusion into the ℓ¹ unitization.

noncomputable def WithLp.unitizationSndL (𝕜 : Type u_1) (A : Type u_2) [NormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] : WithLp 1 (Unitization 𝕜 A) →L[𝕜] A

The projection onto the nonunital summand of the external ℓ¹ unitization.

@[simp]

theorem WithLp.unitizationSndL_apply (𝕜 : Type u_1) (A : Type u_2) [NormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] (u : WithLp 1 (Unitization 𝕜 A)) : (unitizationSndL 𝕜 A) u = u.ofLp.toProd.2

The bounded projection recovers the nonunital coordinate.

theorem WithLp.unitizationInrL_mul (𝕜 : Type u_1) (A : Type u_2) [NormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] (a b : A) : (unitizationInrL 𝕜 A) (a * b) = (unitizationInrL 𝕜 A) a * (unitizationInrL 𝕜 A) b

The bounded inclusion into the ℓ¹ unitization preserves multiplication.

theorem WithLp.unitization_eq_fst_smul_one_add_inr {𝕜 : Type u_1} {A : Type u_2} [NormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] (u : WithLp 1 (Unitization 𝕜 A)) : u = u.ofLp.toProd.1 • 1 + toLp 1 ↑u.ofLp.toProd.2

Every element of the ℓ¹ unitization is the sum of its scalar and nonunital parts.

@[instance_reducible]

noncomputable instance WithLp.instUnitizationNormedCommRing {𝕜 : Type u_3} {A : Type u_4} [NormedField 𝕜] [NonUnitalNormedCommRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] : NormedCommRing (WithLp 1 (Unitization 𝕜 A))

The ℓ¹ unitization of a commutative normed algebra is a commutative normed ring.

theorem ContinuousLinearMap.unitization_apply_eq_fst_smul_add {𝕜 : Type u_1} {A : Type u_2} {E : Type u_3} [NormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (M : WithLp 1 (Unitization 𝕜 A) →L[𝕜] E) (u : WithLp 1 (Unitization 𝕜 A)) : M u = u.ofLp.toProd.1 • M 1 + M (WithLp.toLp 1 ↑u.ofLp.toProd.2)

A bounded linear map on the ℓ¹ unitization splits into its scalar and nonunital parts.

theorem ContinuousLinearMap.norm_comp_unitizationSndL_le {𝕜 : Type u_1} {A : Type u_2} {E : Type u_3} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (D : A →L[𝕜] E) : ‖D ∘SL WithLp.unitizationSndL 𝕜 A‖ ≤ ‖D‖

Extension through the nonunital coordinate projection does not increase the norm.