Jacobson radical #
The Jacobson radical of a ring R
is defined to be the intersection of all maximal ideals of R
.
This is similar to how the nilradical is equal to the intersection of all prime ideals of R
.
We can extend the idea of the nilradical to ideals of R
,
by letting the radical of an ideal I
be the intersection of prime ideals containing I
.
Under this extension, the original nilradical is the radical of the zero ideal ⊥
.
Here we define the Jacobson radical of an ideal I
in a similar way,
as the intersection of maximal ideals containing I
.
Main definitions #
Let R
be a commutative ring, and I
be an ideal of R

Ideal.jacobson I
is the jacobson radical, i.e. the infimum of all maximal ideals containing I. 
Ideal.IsLocal I
is the proposition that the jacobson radical ofI
is itself a maximal ideal
Main statements #

mem_jacobson_iff
gives a characterization of members of the jacobson of I 
Ideal.isLocal_of_isMaximal_radical
: if the radical of I is maximal then so is the jacobson radical
Tags #
Jacobson, Jacobson radical, Local Ideal
An ideal equals its Jacobson radical iff it is the intersection of a set of maximal ideals. Allowing the set to include ⊤ is equivalent, and is included only to simplify some proofs.
An ideal I
of R
is equal to its Jacobson radical if and only if
the Jacobson radical of the quotient ring R/I
is the zero ideal
The standard radical and Jacobson radical of an ideal I
of R
are equal if and only if
the nilradical and Jacobson radical of the quotient ring R/I
coincide
 out : Ideal.IsMaximal (Ideal.jacobson I)
A ring
R
is local if and only if its jacobson radical is maximal
An ideal I
is local iff its Jacobson radical is maximal.