The Jacobson radical of a nonunital algebra

The radical is the inverse image of the Jacobson radical of the external unitization. We provide both its two-sided ring ideal and its scalar submodule, so scalar closure is retained even without an identity. Quasiregularity characterizes membership and shows that this construction agrees with Ring.jacobson when the algebra already has a unit.

For a two-sided ideal J of A, given as a NonUnitalSubalgebra closed under multiplication by A on both sides, the radical of J, viewed as a nonunital algebra in its own right, is J ∩ rad A. This is the identity rad J = J ∩ rad A used in the structure theory of ideals of Banach algebras; in particular ideals of semisimple algebras are semisimple, and an ideal is a radical algebra exactly when it lies in rad A.

These constructions are algebraic; no completeness or norm is required.

Main results

• TauCeti.mem_nonUnitalJacobson_iff_isQuasiregular_smul_add_mul: radical membership by quasiregularity.
• TauCeti.jacobson_unitization_eq_bot_iff: over a base ring with zero radical, the unitization is semisimple exactly when the algebra is.
• NonUnitalSubalgebra.coe_mem_nonUnitalJacobson_iff: an element of a two-sided ideal J lies in rad A exactly when it lies in rad J.
• NonUnitalSubalgebra.image_coe_nonUnitalJacobson: rad J = J ∩ rad A, as subsets of A.

References

• Dales, Banach Algebras and Automatic Continuity, §§1.3–1.5.
• The unitization and quasiregularity interfaces are Mathlib's Unitization and isQuasiregular_iff_isUnit'. Radical membership uses TauCeti.Ring.mem_jacobson_iff_isUnit_one_add_mul_left.

def TauCeti.nonUnitalJacobson (R : Type u_1) (A : Type u_2) [CommRing R] [NonUnitalRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : TwoSidedIdeal A

The Jacobson radical of a nonunital algebra, defined through its external unitization.

@[simp]

theorem TauCeti.mem_nonUnitalJacobson (R : Type u_1) (A : Type u_2) [CommRing R] [NonUnitalRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {a : A} : a ∈ nonUnitalJacobson R A ↔ ↑a ∈ Ring.jacobson (Unitization R A)

def TauCeti.nonUnitalJacobsonSubmodule (R : Type u_1) (A : Type u_2) [CommRing R] [NonUnitalRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : Submodule R A

The scalar submodule underlying the nonunital Jacobson radical.

@[simp]

theorem TauCeti.mem_nonUnitalJacobsonSubmodule (R : Type u_1) (A : Type u_2) [CommRing R] [NonUnitalRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {a : A} : a ∈ nonUnitalJacobsonSubmodule R A ↔ a ∈ nonUnitalJacobson R A

@[simp]

theorem TauCeti.coe_nonUnitalJacobsonSubmodule (R : Type u_1) (A : Type u_2) [CommRing R] [NonUnitalRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : ↑(nonUnitalJacobsonSubmodule R A) = ↑(nonUnitalJacobson R A)

The two carriers of the radical have exactly the same elements.

theorem TauCeti.smul_mem_nonUnitalJacobson (R : Type u_1) (A : Type u_2) [CommRing R] [NonUnitalRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (r : R) {a : A} (ha : a ∈ nonUnitalJacobson R A) : r • a ∈ nonUnitalJacobson R A

The nonunital Jacobson radical is closed under scalar multiplication.

theorem TauCeti.mem_nonUnitalJacobson_iff_isQuasiregular_smul_add_mul (R : Type u_1) (A : Type u_2) [CommRing R] [NonUnitalRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {a : A} : a ∈ nonUnitalJacobson R A ↔ ∀ (r : R) (b : A), IsQuasiregular (r • a + b * a)

Membership in the nonunital radical is equivalent to quasiregularity of all scalar-plus-left multiples. The scalar term comes from reading left multiplication in the external unitization.

theorem TauCeti.jacobson_unitization_eq_bot_iff {R : Type u_1} {A : Type u_2} [CommRing R] [NonUnitalRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (hR : Ring.jacobson R = ⊥) : Ring.jacobson (Unitization R A) = ⊥ ↔ nonUnitalJacobson R A = ⊥

Over a base ring with zero Jacobson radical, the external unitization of a nonunital algebra has zero Jacobson radical exactly when the algebra does. The radical of the unitization lies in the kernel of the augmentation Unitization.fst, because its image under the augmentation lies in the radical of the base ring.

@[simp]

theorem TauCeti.nonUnitalJacobson_eq_toTwoSided_jacobson (R : Type u_1) [CommRing R] (B : Type u_3) [Ring B] [Algebra R B] : nonUnitalJacobson R B = (Ring.jacobson B).toTwoSided

For an algebra that already has an identity, the external-unitization definition recovers its ordinary Jacobson radical. The external unitization itself is not identified with the original algebra.

theorem NonUnitalSubringClass.isQuasiregular_coe_iff {S : Type u_1} {A : Type u_2} [NonUnitalRing A] [SetLike S A] [NonUnitalSubringClass S A] {s : S} (hr : ∀ (b : A) {y : A}, y ∈ s → y * b ∈ s) {x : ↥s} : IsQuasiregular ↑x ↔ IsQuasiregular x

Quasiregularity of an element of a right ideal may be tested in the ambient ring: its quasi-inverse y satisfies y = -(x + x * y), so it lies in the ideal again.

theorem NonUnitalSubalgebra.mem_nonUnitalJacobson_of_coe_mem {R : Type u_1} {A : Type u_2} [CommRing R] [NonUnitalRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {S : NonUnitalSubalgebra R A} (hr : ∀ (b : A) {y : A}, y ∈ S → y * b ∈ S) {a : ↥S} (ha : ↑a ∈ TauCeti.nonUnitalJacobson R A) : a ∈ TauCeti.nonUnitalJacobson R ↥S

An element of a right ideal S that lies in the radical of the ambient algebra lies in the radical of S, viewed as a nonunital algebra.

theorem NonUnitalSubalgebra.coe_mem_nonUnitalJacobson_iff {R : Type u_1} {A : Type u_2} [CommRing R] [NonUnitalRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {S : NonUnitalSubalgebra R A} (hl : ∀ (b : A) {y : A}, y ∈ S → b * y ∈ S) (hr : ∀ (b : A) {y : A}, y ∈ S → y * b ∈ S) {a : ↥S} : ↑a ∈ TauCeti.nonUnitalJacobson R A ↔ a ∈ TauCeti.nonUnitalJacobson R ↥S

For a two-sided ideal S, an element of S lies in the radical of the ambient algebra exactly when it lies in the radical of S, viewed as a nonunital algebra.

theorem NonUnitalSubalgebra.image_coe_nonUnitalJacobson {R : Type u_1} {A : Type u_2} [CommRing R] [NonUnitalRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {S : NonUnitalSubalgebra R A} (hl : ∀ (b : A) {y : A}, y ∈ S → b * y ∈ S) (hr : ∀ (b : A) {y : A}, y ∈ S → y * b ∈ S) : Subtype.val '' ↑(TauCeti.nonUnitalJacobson R ↥S) = ↑S ∩ ↑(TauCeti.nonUnitalJacobson R A)

The radical of an ideal. For a two-sided ideal S, the radical of S, viewed as a nonunital algebra, is S ∩ rad A.

theorem NonUnitalSubalgebra.nonUnitalJacobson_eq_top_iff {R : Type u_1} {A : Type u_2} [CommRing R] [NonUnitalRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {S : NonUnitalSubalgebra R A} (hl : ∀ (b : A) {y : A}, y ∈ S → b * y ∈ S) (hr : ∀ (b : A) {y : A}, y ∈ S → y * b ∈ S) : TauCeti.nonUnitalJacobson R ↥S = ⊤ ↔ ↑S ⊆ ↑(TauCeti.nonUnitalJacobson R A)

A two-sided ideal is a radical algebra exactly when it is contained in the radical of the ambient algebra.

theorem NonUnitalSubalgebra.nonUnitalJacobson_eq_bot_of_eq_bot {R : Type u_1} {A : Type u_2} [CommRing R] [NonUnitalRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {S : NonUnitalSubalgebra R A} (hl : ∀ (b : A) {y : A}, y ∈ S → b * y ∈ S) (hr : ∀ (b : A) {y : A}, y ∈ S → y * b ∈ S) (h : TauCeti.nonUnitalJacobson R A = ⊥) : TauCeti.nonUnitalJacobson R ↥S = ⊥

Every two-sided ideal of a semisimple algebra is semisimple as a nonunital algebra.