Jacobson Rings #
The following conditions are equivalent for a ring R
:
- Every radical ideal
I
is equal to its Jacobson radical - Every radical ideal
I
can be written as an intersection of maximal ideals - Every prime ideal
I
is 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.is_jacobson_polynomial_iff_is_jacobson
says polynomials over a Jacobson ring form a Jacobson ring.
Main definitions #
Let R
be a commutative ring. Jacobson Rings are defined using the first of the above conditions
is_jacobson R
is the proposition thatR
is a Jacobson ring. It is a class, implemented as the predicate that for any ideal,I.radical = I
impliesI.jacobson = I
.
Main statements #
is_jacobson_iff_prime_eq
is the equivalence between conditions 1 and 3 above.is_jacobson_iff_Inf_maximal
is the equivalence between conditions 1 and 2 above.is_jacobson_of_surjective
says that ifR
is a Jacobson ring andf : R →+* S
is surjective, thenS
is also a Jacobson ringis_jacobson_mv_polynomial
says that multi-variate polynomials over a Jacobson ring are Jacobson.
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.
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 y = {to_equiv := {to_fun := λ (p : {p // p.is_maximal}), ⟨ideal.comap (algebra_map R S) p.val, _⟩, inv_fun := λ (p : {p // p.is_maximal ∧ y ∉ p}), ⟨ideal.map (algebra_map R S) 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.
If I
is a prime ideal of polynomial R
and pX ∈ I
is a non-constant polynomial,
then the map R →+* R[x]/I
descends to an integral map when localizing at pX.leading_coeff
.
In particular X
is integral because it satisfies pX
, and constants are trivially integral,
so integrality of the entire extension follows by closure under addition and multiplication.
If f : R → S
descends to an integral map in the localization at x
,
and R
is a Jacobson ring, then the intersection of all maximal ideals in S
is trivial
If R
is a Jacobson ring, and P
is a maximal ideal of polynomial R
,
then R → R[X]/P
is an integral map.
General form of the nullstellensatz for Jacobson rings, since in a Jacobson ring we have
Inf {P maximal | P ≥ I} = Inf {P prime | P ≥ I} = I.radical
. Fields are always Jacobson,
and in that special case this is (most of) the classical Nullstellensatz,
since I(V(I))
is the intersection of maximal ideals containing I
, which is then I.radical