Simple Banach modules

Every algebraic module map out of a simple Banach module over a Banach algebra is continuous, provided the target action is continuous. In particular, algebraic isomorphisms between such modules are homeomorphisms: a compatible complete module norm is unique up to equivalence.

Over the complex numbers every module endomorphism is a scalar. This is the scalar-commutant form of Rickart's theorem, used to turn algebraic Jacobson density into density over the complex scalars. The finite interpolation theorem LinearIndependent.exists_smul_eq_of_completeSpace makes this specialization using the algebraic LinearIndependent.exists_smul_eq. Simplicity here is algebraic: having no proper closed invariant subspace alone is not the hypothesis.

Every element acting with infinite-dimensional range has a left multiple that kills a vector it does not kill while keeping infinite-dimensional range, IsSimpleModule.exists_mul_smul_eq_zero. Iterating this gives sequences of products with strictly increasing kernels, as used for separating ideals.

The automatic-continuity argument uses Mathlib's open mapping theorem on the surjective orbit map at a nonzero vector. The scalar conclusion then uses nonemptiness of the spectrum of a bounded complex operator and Schur's lemma.

References

• C. E. Rickart, General Theory of Banach Algebras, Theorem 2.6.26.
• H. G. Dales, Banach Algebras and Automatic Continuity, simple Banach modules.

theorem LinearMap.continuous_of_isSimpleModule {𝕜 : Type u_1} {A : Type u_2} {E : Type u_3} {F : Type u_4} [NontriviallyNormedField 𝕜] [NormedRing A] [NormedAlgebra 𝕜 A] [CompleteSpace A] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] [Module A E] [IsScalarTower 𝕜 A E] [ContinuousSMul A E] [IsSimpleModule A E] [TopologicalSpace F] [AddCommGroup F] [Module A F] [ContinuousSMul A F] (f : E →ₗ[A] F) : Continuous ⇑f

An algebraic module map from a simple Banach module over a Banach algebra into a topological module on which the algebra acts continuously is continuous. The target need not be complete, normed or simple.

theorem LinearEquiv.isHomeomorph_of_isSimpleModule {𝕜 : Type u_1} {A : Type u_2} {E : Type u_3} {F : Type u_4} [NontriviallyNormedField 𝕜] [NormedRing A] [NormedAlgebra 𝕜 A] [CompleteSpace A] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] [Module A E] [IsScalarTower 𝕜 A E] [ContinuousSMul A E] [IsSimpleModule A E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] [Module A F] [IsScalarTower 𝕜 A F] [ContinuousSMul A F] (f : E ≃ₗ[A] F) : IsHomeomorph ⇑f

An algebraic equivalence of simple Banach modules is a homeomorphism. In particular, compatible Banach module norms on the same module are equivalent.

theorem LinearMap.existsUnique_eq_smul_of_isSimpleModule {A : Type u_1} {E : Type u_2} [NormedRing A] [NormedAlgebra ℂ A] [CompleteSpace A] [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] [Module A E] [IsScalarTower ℂ A E] [ContinuousSMul A E] [IsSimpleModule A E] (f : E →ₗ[A] E) : ∃! c : ℂ, ∀ (x : E), f x = c • x

Rickart's scalar-commutant theorem: every algebraic endomorphism of a simple complex Banach module is multiplication by a unique complex scalar.

theorem IsSimpleModule.algebraMap_end_bijective_of_completeSpace {A : Type u_1} {E : Type u_2} [NormedRing A] [NormedAlgebra ℂ A] [CompleteSpace A] [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] [Module A E] [IsScalarTower ℂ A E] [ContinuousSMul A E] [IsSimpleModule A E] : Function.Bijective ⇑(algebraMap ℂ (Module.End A E))

Rickart's scalar-commutant theorem: the scalar map from the complex numbers to the algebraic endomorphism ring of a simple Banach module is bijective.

theorem LinearIndependent.exists_smul_eq_of_completeSpace {A : Type u_1} {E : Type u_2} [NormedRing A] [NormedAlgebra ℂ A] [CompleteSpace A] [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] [Module A E] [IsScalarTower ℂ A E] [ContinuousSMul A E] [IsSimpleModule A E] {ι : Type u_3} [Finite ι] {v : ι → E} (hv : LinearIndependent ℂ v) (w : ι → E) : ∃ (a : A), ∀ (i : ι), a • v i = w i

Complex Jacobson density: one algebra element prescribes arbitrary values on any finite complex-linearly independent family in a simple Banach module.

theorem IsSimpleModule.exists_mul_smul_eq_zero {A : Type u_1} {E : Type u_2} [NormedRing A] [NormedAlgebra ℂ A] [CompleteSpace A] [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] [Module A E] [IsScalarTower ℂ A E] [ContinuousSMul A E] [IsSimpleModule A E] (p : A) (hp : ¬FiniteDimensional ℂ ↥(LinearMap.range ((Algebra.lsmul ℂ ℂ E) p))) : ∃ (b : A) (x : E), p • x ≠ 0 ∧ (b * p) • x = 0 ∧ ¬FiniteDimensional ℂ ↥(LinearMap.range ((Algebra.lsmul ℂ ℂ E) (b * p)))

If p acts on a simple complex Banach module with infinite-dimensional range, then some left multiple b * p kills a vector that p does not kill, and b * p still acts with infinite-dimensional range. The factor b is 1 - f for a finite-rank action f when some element acts with nonzero finite rank, and otherwise comes from complex Jacobson density.