Unitized bounded actions and Banach left modules

A bounded bilinear action M : A →L[𝕜] E →L[𝕜] E of a possibly nonunital normed algebra extends to the ℓ¹ unitization A⁺ = WithLp 1 (Unitization 𝕜 A) without an associativity assumption via ContinuousLinearMap.unitizationActionL, sending (λ, a) to λ • id + M a. This file records its apply formula, identity action, norm bound 1 + ‖M‖, and uniqueness, and characterizes intertwining maps and left associativity by iff statements. For associative left actions, ContinuousLinearMap.unitizationAction is the algebra-homomorphism form of the same extension, with an explicit comparison lemma. The approximate-identity lemmas show that the points where a left approximate identity converges are invariant under A⁺, and that each unitized orbit lies in the closure of the original orbit at such a point. Composing a bounded derivation with the nonunital coordinate projection extends its Leibniz rule to unital bimodule actions.

Main declarations

• ContinuousLinearMap.unitizationActionL: the bounded unital extension of a bilinear action.
• ContinuousLinearMap.eq_unitizationActionL: uniqueness of the unital extension.
• ContinuousLinearMap.unitizationActionL_mul_iff: preservation and reflection of associativity.
• ContinuousLinearMap.intertwines_unitizationActionL_iff: characterization of intertwining maps.
• ContinuousLinearMap.unitizationAction: the unital action of A⁺ extending L.
• ContinuousLinearMap.unitizationAction_apply: (λ, a) · z = λ • z + L a z.
• ContinuousLinearMap.norm_unitizationAction_apply_le: ‖u · z‖ ≤ (1 + ‖L‖) * ‖u‖ * ‖z‖.
• ContinuousLinearMap.tendsto_apply_unitizationAction, ContinuousLinearMap.unitizationAction_apply_mem_closure: if a left approximate identity converges at x, it converges at every u · x, and u · x lies in the closure of A · x.

References

• H. G. Dales, Banach Algebras and Automatic Continuity, §§1.3 and 2.8.

noncomputable def ContinuousLinearMap.unitizationActionL {𝕜 : 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] (M : A →L[𝕜] E →L[𝕜] E) : WithLp 1 (Unitization 𝕜 A) →L[𝕜] E →L[𝕜] E

Extend a bounded bilinear action to the ℓ¹ unitization by letting its new identity act as the identity on E. The algebra argument comes first, also for right actions.

@[simp]

theorem ContinuousLinearMap.unitizationActionL_apply {𝕜 : 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] (M : A →L[𝕜] E →L[𝕜] E) (u : WithLp 1 (Unitization 𝕜 A)) (x : E) : (M.unitizationActionL u) x = u.ofLp.toProd.1 • x + (M u.ofLp.toProd.2) x

The coordinate formula for the unitized bounded action.

@[simp]

theorem ContinuousLinearMap.unitizationActionL_toLp_inr {𝕜 : 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] (M : A →L[𝕜] E →L[𝕜] E) (a : A) : M.unitizationActionL (WithLp.toLp 1 ↑a) = M a

Restricting the unitized action to the original algebra recovers the action.

@[simp]

theorem ContinuousLinearMap.unitizationActionL_one {𝕜 : 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] (M : A →L[𝕜] E →L[𝕜] E) : M.unitizationActionL 1 = ContinuousLinearMap.id 𝕜 E

The new identity acts as the identity, even if the original action was degenerate.

theorem ContinuousLinearMap.norm_unitizationActionL_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] (M : A →L[𝕜] E →L[𝕜] E) : ‖M.unitizationActionL‖ ≤ 1 + ‖M‖

The bounded extension need not be contractive; its norm is at most 1 + ‖M‖.

theorem ContinuousLinearMap.eq_unitizationActionL {𝕜 : 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] (Φ : WithLp 1 (Unitization 𝕜 A) →L[𝕜] E →L[𝕜] E) (M : A →L[𝕜] E →L[𝕜] E) (h1 : Φ 1 = ContinuousLinearMap.id 𝕜 E) (hM : ∀ (a : A), Φ (WithLp.toLp 1 ↑a) = M a) : Φ = M.unitizationActionL

A unital bounded action is uniquely determined by its restriction to A.

theorem ContinuousLinearMap.intertwines_unitizationActionL_iff {𝕜 : 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] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (T : E →L[𝕜] F) (M : A →L[𝕜] E →L[𝕜] E) (N : A →L[𝕜] F →L[𝕜] F) : (∀ (u : WithLp 1 (Unitization 𝕜 A)) (x : E), T ((M.unitizationActionL u) x) = (N.unitizationActionL u) (T x)) ↔ ∀ (a : A) (x : E), T ((M a) x) = (N a) (T x)

A bounded linear map intertwines the unitized actions exactly when it intertwines the original actions. Apply this separately to the left and right actions of a bimodule.

noncomputable def ContinuousLinearMap.unitizationAction {𝕜 : 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] (L : A →L[𝕜] E →L[𝕜] E) (hL : ∀ (a b : A) (z : E), (L (a * b)) z = (L a) ((L b) z)) : WithLp 1 (Unitization 𝕜 A) →ₐ[𝕜] E →L[𝕜] E

The unital action on E of the ℓ¹ unitization of A extending the left action L.

@[simp]

theorem ContinuousLinearMap.unitizationAction_apply {𝕜 : 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] (L : A →L[𝕜] E →L[𝕜] E) (hL : ∀ (a b : A) (z : E), (L (a * b)) z = (L a) ((L b) z)) (u : WithLp 1 (Unitization 𝕜 A)) (z : E) : ((L.unitizationAction hL) u) z = u.ofLp.toProd.1 • z + (L u.ofLp.toProd.2) z

The unitized action of (λ, a) is λ • id + L a.

@[simp]

theorem ContinuousLinearMap.unitizationAction_toLp_inr {𝕜 : 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] (L : A →L[𝕜] E →L[𝕜] E) (hL : ∀ (a b : A) (z : E), (L (a * b)) z = (L a) ((L b) z)) (a : A) : (L.unitizationAction hL) (WithLp.toLp 1 ↑a) = L a

The unitized action agrees with L on A.

theorem ContinuousLinearMap.unitizationActionL_eq_unitizationAction {𝕜 : 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] (L : A →L[𝕜] E →L[𝕜] E) (hL : ∀ (a b : A) (x : E), (L (a * b)) x = (L a) ((L b) x)) (u : WithLp 1 (Unitization 𝕜 A)) : L.unitizationActionL u = (L.unitizationAction hL) u

For an associative left action, the bounded extension agrees with its unital algebra-homomorphism extension.

theorem ContinuousLinearMap.unitizationActionL_mul_iff {𝕜 : 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] (L : A →L[𝕜] E →L[𝕜] E) : (∀ (u v : WithLp 1 (Unitization 𝕜 A)) (x : E), (L.unitizationActionL (u * v)) x = (L.unitizationActionL u) ((L.unitizationActionL v) x)) ↔ ∀ (a b : A) (x : E), (L (a * b)) x = (L a) ((L b) x)

Left associativity is preserved and reflected by unitization.

theorem ContinuousLinearMap.norm_unitizationAction_apply_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] (L : A →L[𝕜] E →L[𝕜] E) (hL : ∀ (a b : A) (z : E), (L (a * b)) z = (L a) ((L b) z)) (u : WithLp 1 (Unitization 𝕜 A)) (z : E) : ‖((L.unitizationAction hL) u) z‖ ≤ (1 + ‖L‖) * ‖u‖ * ‖z‖

The unitized action is bounded: ‖u · z‖ ≤ (1 + ‖L‖) * ‖u‖ * ‖z‖.

theorem ContinuousLinearMap.tendsto_apply_unitizationAction {𝕜 : 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] (L : A →L[𝕜] E →L[𝕜] E) (hL : ∀ (a b : A) (z : E), (L (a * b)) z = (L a) ((L b) z)) {l : Filter A} (hl : ∀ (a : A), Filter.Tendsto (fun (x : A) => x * a) l (nhds a)) {x : E} (hlx : Filter.Tendsto (fun (e : A) => (L e) x) l (nhds x)) (u : WithLp 1 (Unitization 𝕜 A)) : Filter.Tendsto (fun (e : A) => (L e) (((L.unitizationAction hL) u) x)) l (nhds (((L.unitizationAction hL) u) x))

If a left approximate identity converges at x, it converges at every u · x with u in the unitization.

theorem ContinuousLinearMap.unitizationAction_apply_mem_closure {𝕜 : 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] (L : A →L[𝕜] E →L[𝕜] E) (hL : ∀ (a b : A) (z : E), (L (a * b)) z = (L a) ((L b) z)) {l : Filter A} [l.NeBot] {x : E} (hlx : Filter.Tendsto (fun (e : A) => (L e) x) l (nhds x)) (u : WithLp 1 (Unitization 𝕜 A)) : ((L.unitizationAction hL) u) x ∈ closure (Set.range fun (b : A) => (L b) x)

If a left approximate identity converges at x, then every u · x with u in the unitization lies in the closure of A · x.

theorem ContinuousLinearMap.comp_unitizationSndL_mul {𝕜 : 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) (L R : WithLp 1 (Unitization 𝕜 A) →L[𝕜] E →L[𝕜] E) (h1L : ∀ (x : E), (L 1) x = x) (h1R : ∀ (x : E), (R 1) x = x) (hD : ∀ (a b : A), D (a * b) = (L (WithLp.toLp 1 ↑a)) (D b) + (R (WithLp.toLp 1 ↑b)) (D a)) (u v : WithLp 1 (Unitization 𝕜 A)) : (D ∘SL WithLp.unitizationSndL 𝕜 A) (u * v) = (L u) ((D ∘SL WithLp.unitizationSndL 𝕜 A) v) + (R v) ((D ∘SL WithLp.unitizationSndL 𝕜 A) u)

Composing a bounded derivation with the nonunital coordinate projection extends its Leibniz rule to unital actions of the ℓ¹ unitization.