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
-
jacobson I
is the jacobson radical, i.e. the infimum of all maximal ideals containing I. -
is_local 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 -
is_local_of_is_maximal_radical
: if the radical of I is maximal then so is the jacobson radical
Tags #
Jacobson, Jacobson radical, Local Ideal
The Jacobson radical of I
is the infimum of all maximal (left) ideals containing I
.
Equations
- I.jacobson = has_Inf.Inf {J : ideal R | I ≤ J ∧ J.is_maximal}
Instances for ideal.jacobson
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.
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