Automatic continuity of derivations on semisimple Banach algebras

A derivation of an algebra B is a linear map D : B → B satisfying the Leibniz rule D (x * y) = x * D y + D x * y; here B need not be commutative, so Mathlib's Derivation, which requires a commutative algebra, does not apply, and the Leibniz rule is a hypothesis on a linear map. This file proves the theorem of Johnson and Sinclair: every derivation of a semisimple complex Banach algebra is continuous, with no continuity assumption on D.

The separating space S(D) of a derivation is a separating ideal, because the commutators of D with left and right multiplication by b are multiplications by D b. In a semisimple algebra a separating ideal is finite-dimensional. A finite-dimensional separating space squares to zero: if q, s ∈ S(D), take x n → 0 with D (x n) → s. Then q * x n lies in the finite-dimensional space S(D), on which D is continuous, so q * D (x n) = D (q * x n) - D q * x n → 0, while q * D (x n) → q * s. Consequently every product b * s with s ∈ S(D) is nilpotent, so S(D) lies in the Jacobson radical, which is zero.

The algebra need not be unital. A derivation D of B extends to the derivation (r, b) ↦ (0, D b) of the ℓ¹ unitization WithLp 1 (Unitization ℂ B), which is semisimple when B is, and B sits isometrically inside it.

Main results

• LinearMap.isSeparatingIdeal_separatingSpace_of_derivation: the separating space of a derivation of a Banach algebra is a separating ideal.
• LinearMap.mul_eq_zero_of_derivation_of_mem_separatingSpace: a finite-dimensional separating space of a derivation squares to zero.
• LinearMap.continuous_of_derivation_of_jacobson_eq_bot: a derivation of a unital semisimple complex Banach algebra is continuous.
• LinearMap.continuous_of_derivation_of_nonUnitalJacobson_eq_bot: a derivation of a semisimple complex Banach algebra, possibly without unit, is continuous.

References

• B. E. Johnson and A. M. Sinclair, Continuity of derivations and a problem of Kaplansky, Amer. J. Math. 90 (1968), 1067–1073.
• H. G. Dales, Banach Algebras and Automatic Continuity, §5.2: separating ideals and the automatic continuity of derivations.

theorem LinearMap.isSeparatingIdeal_separatingSpace_of_derivation {𝕜 : Type u_1} {B : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing B] [NormedSpace 𝕜 B] [IsScalarTower 𝕜 B B] [SMulCommClass 𝕜 B B] [CompleteSpace B] (D : B →ₗ[𝕜] B) (hD : ∀ (x y : B), D (x * y) = x * D y + D x * y) : D.separatingSpace.IsSeparatingIdeal

The separating space of a derivation is a separating ideal. If D : B → B is a linear map on a Banach algebra satisfying the Leibniz rule D (x * y) = x * D y + D x * y, not assumed continuous, then the separating space of D is a separating ideal of B.

theorem LinearMap.mul_eq_zero_of_derivation_of_mem_separatingSpace {𝕜 : Type u_1} {B : Type u_2} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing B] [NormedSpace 𝕜 B] [IsScalarTower 𝕜 B B] [SMulCommClass 𝕜 B B] [CompleteSpace 𝕜] (D : B →ₗ[𝕜] B) (hD : ∀ (x y : B), D (x * y) = x * D y + D x * y) [FiniteDimensional 𝕜 ↥D.separatingSpace] {q s : B} (hq : q ∈ D.separatingSpace) (hs : s ∈ D.separatingSpace) : q * s = 0

A finite-dimensional separating space of a derivation squares to zero. If D : B → B is a linear map on a normed algebra over a complete field satisfying the Leibniz rule, not assumed continuous, and its separating space is finite-dimensional, then q * s = 0 for all q and s in the separating space.

theorem LinearMap.continuous_of_derivation_of_jacobson_eq_bot {B : Type u_1} [NormedRing B] [NormedAlgebra ℂ B] [CompleteSpace B] (D : B →ₗ[ℂ] B) (hD : ∀ (x y : B), D (x * y) = x * D y + D x * y) (hB : Ring.jacobson B = ⊥) : Continuous ⇑D

Johnson–Sinclair theorem: derivations of semisimple Banach algebras are continuous. Let B be a unital complex Banach algebra with zero Jacobson radical. Every linear map D : B → B satisfying the Leibniz rule D (x * y) = x * D y + D x * y is continuous.

theorem LinearMap.continuous_of_derivation_of_nonUnitalJacobson_eq_bot {B : Type u_1} [NonUnitalNormedRing B] [NormedSpace ℂ B] [IsScalarTower ℂ B B] [SMulCommClass ℂ B B] [CompleteSpace B] (D : B →ₗ[ℂ] B) (hD : ∀ (x y : B), D (x * y) = x * D y + D x * y) (hB : TauCeti.nonUnitalJacobson ℂ B = ⊥) : Continuous ⇑D

Johnson–Sinclair theorem, nonunital form. Let B be a complex Banach algebra, not necessarily unital, with zero Jacobson radical. Every linear map D : B → B satisfying the Leibniz rule D (x * y) = x * D y + D x * y is continuous.