The Jacobson radical of a ring, elementwise

Ring.jacobson R is the intersection of the maximal left ideals of R. This file records the elementwise description of that ideal over a ring that is not assumed commutative: x lies in the radical exactly when 1 + y * x is a unit for every y, equivalently when 1 + x * y is a unit for every y. Mathlib proves the statement only over a commutative ring (Ring.mem_jacobson_iff); the content of the noncommutative version is that membership in the radical only supplies a left inverse for 1 + y * x, so the argument has to promote that left inverse to a two-sided one.

The two descriptions differ only by the swap TauCeti.isUnit_one_add_mul_comm, and that is the mechanism behind the left-right symmetry of the radical, proved in TauCeti/RingTheory/Jacobson/MulOpposite.lean.

Main results

• TauCeti.Ring.mem_jacobson_iff_isUnit_one_add_mul_left and TauCeti.Ring.mem_jacobson_iff_isUnit_one_add_mul_right: the two elementwise descriptions of the Jacobson radical of a ring.
• TauCeti.Ring.mem_jacobson_of_forall_isNilpotent_mul: an element all of whose left multiples are nilpotent lies in the radical.
• TauCeti.Ring.isLocalHom_mk_jacobson: units lift modulo the Jacobson radical.
• TauCeti.Ring.instNontrivialQuotientJacobson: the quotient of a nontrivial ring by its Jacobson radical is nontrivial.
• Ideal.subsingleton_of_le_jacobson: a commutative ring is trivial if its quotient by some ideal in the Jacobson radical is.

References

• N. Jacobson, Structure of Rings, AMS Colloquium Publications 37 (1956), Chapter I.

theorem TauCeti.Ring.mem_jacobson_iff_isUnit_one_add_mul_left {R : Type u_1} [Ring R] {x : R} : x ∈ Ring.jacobson R ↔ ∀ (y : R), IsUnit (1 + y * x)

The Jacobson radical of a ring is {x | ∀ y, IsUnit (1 + y * x)}.

Mathlib's Ring.mem_jacobson_iff is this statement over a commutative ring.

theorem TauCeti.Ring.mem_jacobson_iff_isUnit_one_add_mul_right {R : Type u_1} [Ring R] {x : R} : x ∈ Ring.jacobson R ↔ ∀ (y : R), IsUnit (1 + x * y)

The right-handed description of the Jacobson radical: it is also {x | ∀ y, IsUnit (1 + x*y)}.

This is where the left-right symmetry enters: the two descriptions differ only by the swap TauCeti.isUnit_one_add_mul_comm.

theorem TauCeti.Ring.mem_jacobson_of_forall_isNilpotent_mul {R : Type u_1} [Ring R] {x : R} (h : ∀ (y : R), IsNilpotent (y * x)) : x ∈ Ring.jacobson R

An element all of whose left multiples are nilpotent lies in the Jacobson radical. In particular, a left ideal consisting of nilpotent elements lies in the radical.

instance TauCeti.Ring.instNontrivialQuotientJacobson (R : Type u_1) [Ring R] [Nontrivial R] : Nontrivial (R ⧸ Ring.jacobson R)

The quotient of a nontrivial ring by its Jacobson radical is nontrivial, the radical being proper by Ring.jacobson_lt_top.

instance TauCeti.Ring.isLocalHom_mk_jacobson (R : Type u_1) [Ring R] : IsLocalHom (Ideal.Quotient.mk (Ring.jacobson R))

Units lift modulo the Jacobson radical: the quotient map R → R ⧸ J(R) is a local homomorphism. If ab ≡ 1 and ba ≡ 1 modulo the radical, then ab and ba are units, so a has a right and a left inverse.

theorem Ideal.subsingleton_of_le_jacobson {R : Type u_1} [CommRing R] {I : Ideal R} (hI : I ≤ Ring.jacobson R) [Subsingleton (R ⧸ I)] : Subsingleton R

If I lies in the Jacobson radical of R and R ⧸ I is trivial, then R is trivial: the ideal I = ⊤ can only lie in the Jacobson radical of the zero ring.