Closedness and quasinilpotence of Jacobson radicals

We compare membership in the nonunital Jacobson radical with membership in the Jacobson radical of the external unitization with its ℓ¹ norm; in particular one is semisimple exactly when the other is, so automatic-continuity theorems for unital semisimple targets transfer to nonunital ones. Pulling back TauCeti.Ring.isClosed_jacobson from TauCeti.Analysis.Normed.Ring.Units then proves closedness of the nonunital radical and its underlying scalar submodule.

The statements use summability of geometric series instead of completeness wherever possible. No normalization of the norm of the identity is assumed.

The radical also consists of the elements all of whose left multiples are quasinilpotent. Over any normed field this is the vanishing of the spectral radius of every left multiple, in the unital and the nonunital setting. In a complex Banach algebra, Gelfand's formula turns it into the vanishing of every gelfandRadius (b * a), the limit of ‖(b * a) ^ n‖ ^ (1 / n).

References

• Dales, Banach Algebras and Automatic Continuity, §§1.3–1.5.
• We use Mathlib's WithLp.unitizationAlgEquiv and Module.comap_jacobson_of_bijective, and Gelfand's formula spectrum.spectralRadius_eq_gelfandRadius.

theorem TauCeti.mem_nonUnitalJacobson_iff_toLp_mem_jacobson (𝕜 : Type u_1) (A : Type u_2) [NormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] {a : A} : a ∈ nonUnitalJacobson 𝕜 A ↔ WithLp.toLp 1 ↑a ∈ Ring.jacobson (WithLp 1 (Unitization 𝕜 A))

The radical defined with the algebraic unitization can equally be tested in its ℓ¹-normed version.

theorem TauCeti.jacobson_withLp_unitization_eq_bot_iff (𝕜 : Type u_1) (A : Type u_2) [NormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] : Ring.jacobson (WithLp 1 (Unitization 𝕜 A)) = ⊥ ↔ nonUnitalJacobson 𝕜 A = ⊥

The ℓ¹ unitization of a nonunital normed algebra has zero Jacobson radical exactly when the algebra does.

theorem TauCeti.isClosed_nonUnitalJacobson (𝕜 : Type u_1) (A : Type u_2) [NormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [HasSummableGeomSeries A] : IsClosed ↑(nonUnitalJacobson 𝕜 A)

The Jacobson radical of a nonunital normed algebra with summable geometric series is closed. In particular this applies to every nonunital Banach algebra.

theorem TauCeti.isClosed_nonUnitalJacobsonSubmodule (𝕜 : Type u_1) (A : Type u_2) [NormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [HasSummableGeomSeries A] : IsClosed ↑(nonUnitalJacobsonSubmodule 𝕜 A)

The scalar submodule underlying the nonunital radical is closed.

theorem TauCeti.mem_nonUnitalJacobson_iff_forall_spectralRadius_mul_eq_zero {𝕜 : Type u_1} {A : Type u_2} [NormedField 𝕜] [NonUnitalRing A] [Module 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] {a : A} : a ∈ nonUnitalJacobson 𝕜 A ↔ ∀ (b : A), spectralRadius 𝕜 (b * a) = 0

An element of a nonunital algebra lies in its Jacobson radical exactly when every left multiple of it by an element of the algebra has spectral radius zero.

theorem TauCeti.Ring.mem_jacobson_iff_forall_spectralRadius_mul_eq_zero {𝕜 : Type u_1} [NormedField 𝕜] {B : Type u_3} [Ring B] [Algebra 𝕜 B] {a : B} : a ∈ Ring.jacobson B ↔ ∀ (b : B), spectralRadius 𝕜 (b * a) = 0

An element of a unital algebra lies in its Jacobson radical exactly when every left multiple of it has spectral radius zero.

theorem TauCeti.Ring.mem_jacobson_iff_forall_gelfandRadius_mul_eq_zero {B : Type u_3} [NormedRing B] [NormedAlgebra ℂ B] [CompleteSpace B] {a : B} : a ∈ Ring.jacobson B ↔ ∀ (b : B), gelfandRadius (b * a) = 0

An element of a complex Banach algebra lies in its Jacobson radical exactly when every left multiple b * a is quasinilpotent, that is, ‖(b * a) ^ n‖ ^ (1 / n) tends to zero.