Jacobson Rings
The following conditions are equivalent for a ring R:
- Every radical ideal
Iis equal to its jacobson radical - Every radical ideal
Ican be written as an intersection of maximal ideals - Every prime ideal
Iis equal to its jacobson radical
Any ring satisfying any of these equivalent conditions is said to be Jacobson.
Some particular examples of Jacobson rings are also proven.
is_jacobson_quotient says that the quotient of a Jacobson ring is Jacobson.
is_jacobson_localization says the localization of a Jacobson ring to a single element is Jacobson.
Main definitions
Let R be a commutative ring. Jacobson Rings are defined using the first of the above conditions
is_jacobson Ris the proposition thatRis a Jacobson ring. It is a class, implemented as the predicate that for any ideal,I.radical = IimpliesI.jacobson = I.
Main statements
is_jacobson_iff_prime_eqis the equivalence between conditions 1 and 3 above.is_jacobson_iff_Inf_maximalis the equivalence between conditions 1 and 2 above.is_jacobson_of_surjectivesays that ifRis a Jacobson ring andf : R →+* Sis surjective, thenSis also a Jacobson ring
Tags
Jacobson, Jacobson Ring
A ring is a Jacobson ring if for every radical ideal I,
the Jacobson radical of I is equal to I.
See is_jacobson_iff_prime_eq and is_jacobson_iff_Inf_maximal for equivalent definitions.
A ring is a Jacobson ring if and only if for all prime ideals P,
the Jacobson radical of P is equal to P.
A ring R is Jacobson if and only if for every prime ideal I,
I can be written as the infimum of some collection of maximal ideals.
Allowing ⊤ in the set M of maximal ideals is equivalent, but makes some proofs cleaner.
Fields have only two ideals, and the condition holds for both of them
Equations
Equations
If R is a Jacobson ring, then maximal ideals in the localization at y
correspond to maximal ideals in the original ring R that don't contain y.
This lemma gives the correspondence in the particular case of an ideal and its comap.
See le_rel_iso_of_maximal for the more general relation isomorphism
If R is a Jacobson ring, then maximal ideals in the localization at y
correspond to maximal ideals in the original ring R that don't contain y.
This lemma gives the correspondence in the particular case of an ideal and its map.
See le_rel_iso_of_maximal for the more general statement, and the reverse of this implication
If R is a Jacobson ring, then maximal ideals in the localization at y
correspond to maximal ideals in the original ring R that don't contain y
Equations
- ideal.order_iso_of_maximal f = {to_equiv := {to_fun := λ (p : {p // p.is_maximal}), ⟨ideal.comap f.to_map p.val, _⟩, inv_fun := λ (p : {p // p.is_maximal ∧ y ∉ p}), ⟨ideal.map f.to_map p.val, _⟩, left_inv := _, right_inv := _}, map_rel_iff' := _}
If S is the localization of the Jacobson ring R at the submonoid generated by y : R, then S is Jacobson.