Uniqueness of the complete norm on a semisimple Banach algebra

Johnson's uniqueness-of-norm theorem: a complex algebra with zero Jacobson radical carries at most one complete algebra norm up to equivalence. If f and g are submultiplicative norms on A with f (c • x) ≤ ‖c‖ * f x for scalars c (and so ℂ-homogeneous), under which A is complete, then there are positive constants with f x ≤ C₁ * g x and g x ≤ C₂ * f x for every x. The algebra A need not be unital, and semisimplicity is the purely algebraic condition that the Jacobson radical of A, defined through its unitization when A has no unit, is zero.

The two norms are placed on two copies of A, which are complex Banach algebras. The identity map between the copies is a surjective algebra homomorphism onto a semisimple Banach algebra, so it is continuous by Johnson's automatic-continuity theorem. Applying this in both directions gives the two norm bounds.

The norm-indexed copy of A follows the construction of AlgebraNorm.copy in Mathlib's Mathlib.Analysis.Normed.Unbundled.IsPowMulUnique, where a norm is placed on a type synonym and the identity map between two such copies is bounded to compare the norms.

Main results

• RingNorm.exists_le_mul_and_le_mul_of_nonUnitalJacobson_eq_bot: two complete scalar-compatible ring norms on a possibly nonunital semisimple complex algebra are equivalent.
• AlgebraNorm.exists_le_mul_and_le_mul_of_jacobson_eq_bot: two complete algebra norms on a unital semisimple complex algebra are equivalent.

References

• B. E. Johnson, The uniqueness of the (complete) norm topology, Bull. Amer. Math. Soc. 73 (1967), 537–539.
• H. G. Dales, Banach Algebras and Automatic Continuity, §5.2.

theorem RingNorm.exists_le_mul_and_le_mul_of_nonUnitalJacobson_eq_bot {A : Type u_1} [NonUnitalRing A] [Module ℂ A] [IsScalarTower ℂ A A] [SMulCommClass ℂ A A] (f g : RingNorm A) (hfs : ∀ (c : ℂ) (x : A), f (c • x) ≤ ‖c‖ * f x) (hgs : ∀ (c : ℂ) (x : A), g (c • x) ≤ ‖c‖ * g x) (hf : CompleteSpace A) (hg : CompleteSpace A) (hA : TauCeti.nonUnitalJacobson ℂ A = ⊥) : ∃ (C₁ : ℝ) (C₂ : ℝ) (_ : 0 < C₁) (_ : 0 < C₂), ∀ (x : A), f x ≤ C₁ * g x ∧ g x ≤ C₂ * f x

Johnson's uniqueness-of-norm theorem. On a complex algebra A with zero Jacobson radical, not necessarily unital, any two ring norms compatible with scalars, under which A is complete, are equivalent.

theorem AlgebraNorm.exists_le_mul_and_le_mul_of_jacobson_eq_bot {A : Type u_1} [Ring A] [Algebra ℂ A] (f g : AlgebraNorm ℂ A) (hf : CompleteSpace A) (hg : CompleteSpace A) (hA : Ring.jacobson A = ⊥) : ∃ (C₁ : ℝ) (C₂ : ℝ) (_ : 0 < C₁) (_ : 0 < C₂), ∀ (x : A), f x ≤ C₁ * g x ∧ g x ≤ C₂ * f x

Johnson's uniqueness-of-norm theorem. On a unital complex algebra A with zero Jacobson radical, any two algebra norms under which A is complete are equivalent.