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 Iis the jacobson radical, i.e. the infimum of all maximal ideals containing I.is_local Iis the proposition that the jacobson radical ofIis itself a maximal ideal
Main statements
mem_jacobson_iffgives a characterization of members of the jacobson of Iis_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 ideals containing I.
Equations
- I.jacobson = has_Inf.Inf {J : ideal R | I ≤ J ∧ J.is_maximal}
Equations
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 equals its Jacobson radical if and only if every element outside I
also lies outside of a maximal ideal containing I.
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
An ideal I is local iff its Jacobson radical is maximal.
Equations
- I.is_local = I.jacobson.is_maximal