Spectral characterization of the Jacobson radical

For an algebra over a semifield, an element a lies in the Jacobson radical exactly when every left multiple b * a has spectrum contained in {0}. In a complex Banach algebra this says that the radical consists of the elements all of whose left multiples are quasinilpotent.

For a nonunital algebra over a field, with the radical TauCeti.nonUnitalJacobson defined through the external unitization, the same holds with the quasispectrum and with b ranging over the algebra itself rather than over its unitization. The reduction squares a left multiple x * a by an element x of the unitization: the square is a left multiple of a by an element of the original algebra.

Main results

• TauCeti.Ring.mem_jacobson_iff_forall_spectrum_mul_subset_singleton_zero: the unital characterization.
• TauCeti.Ring.le_jacobson_of_forall_spectrum_subset_singleton_zero: the radical contains every left ideal consisting of elements with spectrum in {0}.
• TauCeti.mem_nonUnitalJacobson_iff_forall_quasispectrum_mul_subset_singleton_zero: the nonunital characterization.
• AlgHom.apply_eq_zero_of_mem_jacobson, NonUnitalAlgHom.apply_eq_zero_of_mem_nonUnitalJacobson: characters, unital or nonunital, kill the radical.

References

• Dales, Banach Algebras and Automatic Continuity, §1.5.

theorem TauCeti.Ring.mem_jacobson_iff_forall_spectrum_mul_subset_singleton_zero {𝕜 : Type u_1} {A : Type u_2} [Semifield 𝕜] [Ring A] [Algebra 𝕜 A] {a : A} : a ∈ Ring.jacobson A ↔ ∀ (b : A), spectrum 𝕜 (b * a) ⊆ {0}

An element of an algebra over a semifield lies in the Jacobson radical exactly when every left multiple of it has spectrum contained in {0}.

theorem TauCeti.Ring.spectrum_subset_singleton_zero_of_mem_jacobson {𝕜 : Type u_1} {A : Type u_2} [Semifield 𝕜] [Ring A] [Algebra 𝕜 A] {a : A} (ha : a ∈ Ring.jacobson A) : spectrum 𝕜 a ⊆ {0}

Every element of the Jacobson radical of an algebra over a semifield has spectrum contained in {0}.

theorem TauCeti.Ring.le_jacobson_of_forall_spectrum_subset_singleton_zero {𝕜 : Type u_1} {A : Type u_2} [Semifield 𝕜] [Ring A] [Algebra 𝕜 A] {I : Ideal A} (h : ∀ x ∈ I, spectrum 𝕜 x ⊆ {0}) : I ≤ Ring.jacobson A

A left ideal all of whose elements have spectrum contained in {0} lies in the Jacobson radical. Together with spectrum_subset_singleton_zero_of_mem_jacobson, the radical is the largest such left ideal.

theorem TauCeti.mem_nonUnitalJacobson_iff_forall_quasispectrum_mul_subset_singleton_zero {𝕜 : Type u_1} {A : Type u_2} [Field 𝕜] [NonUnitalRing A] [Module 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] {a : A} : a ∈ nonUnitalJacobson 𝕜 A ↔ ∀ (b : A), quasispectrum 𝕜 (b * a) ⊆ {0}

An element of a nonunital algebra over a field lies in its Jacobson radical exactly when every left multiple of it by an element of the algebra has quasispectrum contained in {0}. Left multiples by scalars need not be tested separately.

theorem AlgHom.apply_eq_zero_of_mem_jacobson {𝕜 : Type u_1} {A : Type u_2} [Field 𝕜] [Ring A] [Algebra 𝕜 A] (φ : A →ₐ[𝕜] 𝕜) {a : A} (ha : a ∈ Ring.jacobson A) : φ a = 0

Every character of an algebra over a field kills the Jacobson radical.

theorem NonUnitalAlgHom.apply_eq_zero_of_mem_nonUnitalJacobson {𝕜 : Type u_1} {A : Type u_2} [Field 𝕜] [NonUnitalRing A] [Module 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] (φ : A →ₙₐ[𝕜] 𝕜) {a : A} (ha : a ∈ TauCeti.nonUnitalJacobson 𝕜 A) : φ a = 0

Every nonunital character of a nonunital algebra over a field kills its Jacobson radical.