Jacobson Rings #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. 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_quotientsays that the quotient of a Jacobson ring is Jacobson.is_jacobson_localizationsays the localization of a Jacobson ring to a single element is Jacobson.is_jacobson_polynomial_iff_is_jacobsonsays 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 Ris the proposition thatRis a Jacobson ring. It is a class, implemented as the predicate that for any ideal,I.is_radicalimpliesI.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 ringis_jacobson_mv_polynomialsays 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 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 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.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 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