Cohen–Hewitt factorization for Banach left modules

Let A be a possibly nonunital Banach algebra acting on a Banach space E on the left through a bounded bilinear map L : A →L[𝕜] E →L[𝕜] E with L (a * b) x = L a (L b x). The action need not be contractive or unital. A left approximate identity of A is a proper filter l on A with e * a → a along l for every a; it is bounded by C when ‖e‖ ≤ C eventually along l.

The essential part of E is the closed linear span of A · E; a bounded left approximate identity converges to the identity on it (TauCeti.Analysis.Normed.Module.Essential). This file proves:

• the Cohen–Hewitt factorization theorem: every x in the essential part factors as x = a · y with ‖a‖ ≤ C, y in the closure of A · x, and y arbitrarily close to x;
• consequently A · E is already a closed linear subspace: it equals the essential part;
• in particular, every element of A is a product of two elements of A.

Implementation notes

The proof is the classical one. Fix 0 < t with t * (1 + C) = 1 / 2. In the ℓ¹ unitization A⁺ = WithLp 1 (Unitization 𝕜 A) put aₙ = (1 - t) ^ n + ∑_{k < n} t (1 - t) ^ k eₖ, with eₖ chosen inductively from the approximate identity. The identity aₙ₊₁ = ((1 - t) + t eₙ) aₙ + t (fₙ - eₙ fₙ), where fₙ is the A-part of aₙ, shows that each aₙ is invertible with ‖aₙ⁻¹‖ ≤ 4 ^ n, once eₙ nearly fixes fₙ. Choosing eₙ to nearly fix aₙ⁻¹ · x as well makes yₙ = aₙ⁻¹ · x a Cauchy sequence. Its limit y satisfies a · y = x, where a = ∑ₖ t (1 - t) ^ k eₖ has norm at most C.

Main results

• ContinuousLinearMap.exists_apply_eq_of_mem_topologicalClosure_span: the Cohen–Hewitt factorization theorem.
• ContinuousLinearMap.coe_topologicalClosure_span_range_eq: the essential part is A · E.
• TauCeti.exists_mul_eq_of_tendsto_mul_right: every element of A factors as a * y with ‖a‖ ≤ C.

References

• H. G. Dales, Banach Algebras and Automatic Continuity, Theorem 2.9.24.
• E. Hewitt, The ranges of certain convolution operators, Math. Scand. 15 (1964), 147–155.
• P. J. Cohen, Factorization in group algebras, Duke Math. J. 26 (1959), 199–205.

The Cohen–Hewitt construction

theorem ContinuousLinearMap.exists_apply_eq_of_mem_topologicalClosure_span {𝕜 : Type u_1} {A : Type u_2} {E : Type u_3} [RCLike 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [CompleteSpace A] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace 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] {C : ℝ} (hC : ∀ᶠ (e : A) in l, ‖e‖ ≤ C) (hl : ∀ (a : A), Filter.Tendsto (fun (x : A) => x * a) l (nhds a)) {x : E} (hx : x ∈ (Submodule.span 𝕜 (Set.range fun (p : A × E) => (L p.1) p.2)).topologicalClosure) {ε : ℝ} (hε : 0 < ε) : ∃ (a : A) (y : E), ‖a‖ ≤ C ∧ y ∈ closure (Set.range fun (b : A) => (L b) x) ∧ ‖y - x‖ < ε ∧ (L a) y = x

Cohen–Hewitt factorization. Let A be a Banach algebra with a left approximate identity l bounded by C, acting boundedly on the left of a Banach space E through L. Every x in the essential part closure (span (A · E)) factors as x = L a y with ‖a‖ ≤ C, where y lies in the closure of A · x and within any prescribed distance ε of x.

theorem ContinuousLinearMap.coe_topologicalClosure_span_range_eq {𝕜 : Type u_1} {A : Type u_2} {E : Type u_3} [RCLike 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [CompleteSpace A] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace 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] {C : ℝ} (hC : ∀ᶠ (e : A) in l, ‖e‖ ≤ C) (hl : ∀ (a : A), Filter.Tendsto (fun (x : A) => x * a) l (nhds a)) : ↑(Submodule.span 𝕜 (Set.range fun (p : A × E) => (L p.1) p.2)).topologicalClosure = Set.range fun (p : A × E) => (L p.1) p.2

Over a Banach algebra with a bounded left approximate identity, the set A · E of products is already a closed linear subspace of a Banach left module E: it equals the essential part closure (span (A · E)).

theorem TauCeti.exists_mul_eq_of_tendsto_mul_right {A : Type u_1} [NonUnitalNormedRing A] [CompleteSpace A] (𝕜 : Type u_2) [RCLike 𝕜] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] {l : Filter A} [l.NeBot] {C : ℝ} (hC : ∀ᶠ (e : A) in l, ‖e‖ ≤ C) (hl : ∀ (a : A), Filter.Tendsto (fun (x : A) => x * a) l (nhds a)) (x : A) : ∃ (a : A) (y : A), ‖a‖ ≤ C ∧ a * y = x

Cohen's factorization theorem for Banach algebras: if A has a left approximate identity bounded by C, then every element of A is a product a * y with ‖a‖ ≤ C.