Bounded approximate identities on essential left modules

Let A be a possibly nonunital normed algebra acting on a normed 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). A left approximate identity of A is a 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. This file proves that a bounded left approximate identity converges to the identity pointwise on the essential part, and that, for a proper filter, the essential part consists exactly of the points where it does.

Main results

• ContinuousLinearMap.tendsto_apply_of_mem_topologicalClosure_span: convergence on the essential part.
• ContinuousLinearMap.tendsto_apply_iff_mem_topologicalClosure_span: the essential part is the set of points of convergence.

References

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

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

A bounded left approximate identity of A converges to the identity at every point of the essential part closure (span (A · E)) of a left A-module E.

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

The essential part closure (span (A · E)) of a left A-module E consists exactly of the points at which a bounded left approximate identity of A converges to the identity.