# 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.`isJacobson_quotient`

says that the quotient of a Jacobson ring is Jacobson.`isJacobson_localization`

says the localization of a Jacobson ring to a single element is Jacobson.`isJacobson_polynomial_iff_isJacobson`

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

`IsJacobson R`

is the proposition that`R`

is a Jacobson ring. It is a class, implemented as the predicate that for any ideal,`I.isRadical`

implies`I.jacobson = I`

.

## Main statements #

`isJacobson_iff_prime_eq`

is the equivalence between conditions 1 and 3 above.`isJacobson_iff_sInf_maximal`

is the equivalence between conditions 1 and 2 above.`isJacobson_of_surjective`

says that if`R`

is a Jacobson ring and`f : R →+* S`

is surjective, then`S`

is also a Jacobson ring`MvPolynomial.isJacobson`

says that multi-variate polynomials over a Jacobson ring are Jacobson.

## Tags #

Jacobson, Jacobson Ring

- out' : ∀ (I : Ideal R), Ideal.IsRadical I → Ideal.jacobson I = I

A ring is a Jacobson ring if for every radical ideal `I`

,
the Jacobson radical of `I`

is equal to `I`

.
See `isJacobson_iff_prime_eq`

and `isJacobson_iff_sInf_maximal`

for equivalent definitions.

## Instances

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_relIso_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_relIso_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`

## Instances For

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 `R[X]`

and `pX ∈ I`

is a non-constant polynomial,
then the map `R →+* R[x]/I`

descends to an integral map when localizing at `pX.leadingCoeff`

.
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 `R[X]`

,
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`