Banach norms on algebraic simple modules

Every algebraic simple module over a unital Banach algebra admits a complete norm with contractive algebra action. No topology on the module is assumed in advance. The norm is transported from the quotient by a maximal left ideal; maximal left ideals are closed, so the quotient seminorm is a norm. Scalar multiplication by the base field has its usual norm equality.

This realization allows results about simple Banach modules to be applied to algebraic simple modules, for instance when testing the Jacobson radical through annihilators. The construction retains the given scalar and algebra actions.

References

• Dales, Banach Algebras and Automatic Continuity, §§1.3–1.5 and §2.6.
• The algebraic realization is Mathlib's isSimpleModule_iff_quot_maximal; closedness is Ideal.IsMaximal.isClosed.

theorem IsSimpleModule.exists_complete_norm {𝕜 : Type u_1} {A : Type u_2} {M : Type u_3} [NormedField 𝕜] [NormedRing A] [NormedAlgebra 𝕜 A] [CompleteSpace A] [AddCommGroup M] [Module A M] [Module 𝕜 M] [IsScalarTower 𝕜 A M] (h : IsSimpleModule A M) : ∃ (p : AddGroupNorm M), NormSMulClass 𝕜 M ∧ CompleteSpace M ∧ IsBoundedSMul A M

Every algebraic simple module over a Banach algebra admits a complete norm compatible with its given vector-space structure and making the algebra action contractive. Neither a normalized identity norm nor a topology on the module is required.