Jacobson Rings

The following conditions are equivalent for a ring R:

1. Every radical ideal I is equal to its Jacobson radical
2. Every radical ideal I can be written as an intersection of maximal ideals
3. 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

class Ideal.IsJacobson (R : Type u_3) [CommRing R] : Prop

• 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.

theorem Ideal.isJacobson_iff {R : Type u_3} [CommRing R] : Ideal.IsJacobson R ↔ ∀ (I : Ideal R), Ideal.IsRadical I → Ideal.jacobson I = I

theorem Ideal.IsJacobson.out {R : Type u_3} [CommRing R] : Ideal.IsJacobson R → ∀ {I : Ideal R}, Ideal.IsRadical I → Ideal.jacobson I = I

theorem Ideal.isJacobson_iff_prime_eq {R : Type u_1} [CommRing R] : Ideal.IsJacobson R ↔ ∀ (P : Ideal R), Ideal.IsPrime P → Ideal.jacobson P = P

A ring is a Jacobson ring if and only if for all prime ideals P, the Jacobson radical of P is equal to P.

theorem Ideal.isJacobson_iff_sInf_maximal {R : Type u_1} [CommRing R] : Ideal.IsJacobson R ↔ ∀ {I : Ideal R}, Ideal.IsPrime I → ∃ M, (∀ (J : Ideal R), J ∈ M → Ideal.IsMaximal J ∨ J = ⊤) ∧ I = sInf M

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.

theorem Ideal.isJacobson_iff_sInf_maximal' {R : Type u_1} [CommRing R] : Ideal.IsJacobson R ↔ ∀ {I : Ideal R}, Ideal.IsPrime I → ∃ M, (∀ (J : Ideal R), J ∈ M → ∀ (K : Ideal R), J < K → K = ⊤) ∧ I = sInf M

theorem Ideal.radical_eq_jacobson {R : Type u_1} [CommRing R] [H : Ideal.IsJacobson R] (I : Ideal R) : Ideal.radical I = Ideal.jacobson I

instance Ideal.isJacobson_field {K : Type u_3} [Field K] : Ideal.IsJacobson K

Fields have only two ideals, and the condition holds for both of them.

theorem Ideal.isJacobson_of_surjective {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [H : Ideal.IsJacobson R] : (∃ f, Function.Surjective ↑f) → Ideal.IsJacobson S

instance Ideal.isJacobson_quotient {R : Type u_1} [CommRing R] {I : Ideal R} [Ideal.IsJacobson R] : Ideal.IsJacobson (R ⧸ I)

theorem Ideal.isJacobson_iso {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (e : R ≃+* S) : Ideal.IsJacobson R ↔ Ideal.IsJacobson S

theorem Ideal.isJacobson_of_isIntegral {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (hRS : Algebra.IsIntegral R S) (hR : Ideal.IsJacobson R) : Ideal.IsJacobson S

theorem Ideal.isJacobson_of_isIntegral' {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (f : R →+* S) (hf : RingHom.IsIntegral f) (hR : Ideal.IsJacobson R) : Ideal.IsJacobson S

theorem Ideal.disjoint_powers_iff_not_mem {R : Type u_1} [CommRing R] {I : Ideal R} (y : R) (hI : Ideal.IsRadical I) : Disjoint ↑(Submonoid.powers y) ↑I ↔ ¬y ∈ I.toAddSubmonoid

theorem Ideal.isMaximal_iff_isMaximal_disjoint {R : Type u_1} (S : Type u_2) [CommRing R] [CommRing S] (y : R) [Algebra R S] [IsLocalization.Away y S] [H : Ideal.IsJacobson R] (J : Ideal S) : Ideal.IsMaximal J ↔ Ideal.IsMaximal (Ideal.comap (algebraMap R S) J) ∧ ¬y ∈ Ideal.comap (algebraMap R S) J

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

theorem Ideal.isMaximal_of_isMaximal_disjoint {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (y : R) [Algebra R S] [IsLocalization.Away y S] [Ideal.IsJacobson R] (I : Ideal R) (hI : Ideal.IsMaximal I) (hy : ¬y ∈ I) : Ideal.IsMaximal (Ideal.map (algebraMap R S) I)

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

def Ideal.orderIsoOfMaximal {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (y : R) [Algebra R S] [IsLocalization.Away y S] [Ideal.IsJacobson R] : { p // Ideal.IsMaximal p } ≃o { p // Ideal.IsMaximal p ∧ ¬y ∈ p }

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

theorem Ideal.isJacobson_localization {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (y : R) [Algebra R S] [IsLocalization.Away y S] [H : Ideal.IsJacobson R] : Ideal.IsJacobson S

If S is the localization of the Jacobson ring R at the submonoid generated by y : R, then S is Jacobson.

theorem Ideal.Polynomial.Subring.mem_closure_image_of {S : Type u_1} {T : Type u_2} [CommRing S] [CommRing T] (g : S →+* T) (u : Set S) (x : S) (hx : x ∈ Subring.closure u) : ↑g x ∈ Subring.closure (↑g '' u)

theorem Ideal.Polynomial.mem_closure_X_union_C {R : Type u_1} [Ring R] (p : Polynomial R) : p ∈ Subring.closure (insert Polynomial.X {f | Polynomial.degree f ≤ 0})

theorem Ideal.Polynomial.isIntegral_isLocalization_polynomial_quotient {R : Type u_1} [CommRing R] {Rₘ : Type u_3} {Sₘ : Type u_4} [CommRing Rₘ] [CommRing Sₘ] (P : Ideal (Polynomial R)) (pX : Polynomial R) (hpX : pX ∈ P) [Algebra (R ⧸ Ideal.comap Polynomial.C P) Rₘ] [IsLocalization.Away (Polynomial.leadingCoeff (Polynomial.map (Ideal.Quotient.mk (Ideal.comap Polynomial.C P)) pX)) Rₘ] [Algebra (Polynomial R ⧸ P) Sₘ] [IsLocalization (Submonoid.map (Ideal.quotientMap P Polynomial.C (_ : Ideal.comap Polynomial.C P ≤ Ideal.comap Polynomial.C P)) (Submonoid.powers (Polynomial.leadingCoeff (Polynomial.map (Ideal.Quotient.mk (Ideal.comap Polynomial.C P)) pX)))) Sₘ] : RingHom.IsIntegral (IsLocalization.map Sₘ (Ideal.quotientMap P Polynomial.C (_ : Ideal.comap Polynomial.C P ≤ Ideal.comap Polynomial.C P)) (_ : Submonoid.powers (Polynomial.leadingCoeff (Polynomial.map (Ideal.Quotient.mk (Ideal.comap Polynomial.C P)) pX)) ≤ Submonoid.comap (Ideal.quotientMap P Polynomial.C (_ : Ideal.comap Polynomial.C P ≤ Ideal.comap Polynomial.C P)) (Submonoid.map (Ideal.quotientMap P Polynomial.C (_ : Ideal.comap Polynomial.C P ≤ Ideal.comap Polynomial.C P)) (Submonoid.powers (Polynomial.leadingCoeff (Polynomial.map (Ideal.Quotient.mk (Ideal.comap Polynomial.C P)) pX))))))

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.

theorem Ideal.Polynomial.jacobson_bot_of_integral_localization {S : Type u_2} [CommRing S] [IsDomain S] {R : Type u_5} [CommRing R] [IsDomain R] [Ideal.IsJacobson R] (Rₘ : Type u_6) (Sₘ : Type u_7) [CommRing Rₘ] [CommRing Sₘ] (φ : R →+* S) (hφ : Function.Injective ↑φ) (x : R) (hx : x ≠ 0) [Algebra R Rₘ] [IsLocalization.Away x Rₘ] [Algebra S Sₘ] [IsLocalization (Submonoid.map φ (Submonoid.powers x)) Sₘ] (hφ' : RingHom.IsIntegral (IsLocalization.map Sₘ φ (_ : Submonoid.powers x ≤ Submonoid.comap φ (Submonoid.map φ (Submonoid.powers x))))) : Ideal.jacobson ⊥ = ⊥

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

theorem Ideal.Polynomial.isJacobson_polynomial_of_isJacobson {R : Type u_1} [CommRing R] (hR : Ideal.IsJacobson R) : Ideal.IsJacobson (Polynomial R)

theorem Ideal.Polynomial.isJacobson_polynomial_iff_isJacobson {R : Type u_1} [CommRing R] : Ideal.IsJacobson (Polynomial R) ↔ Ideal.IsJacobson R

instance Ideal.Polynomial.instIsJacobsonPolynomialToSemiringToCommSemiringCommRing {R : Type u_1} [CommRing R] [Ideal.IsJacobson R] : Ideal.IsJacobson (Polynomial R)

theorem Ideal.Polynomial.isMaximal_comap_C_of_isMaximal {R : Type u_1} [CommRing R] [Ideal.IsJacobson R] (P : Ideal (Polynomial R)) [hP : Ideal.IsMaximal P] [Nontrivial R] (hP' : ∀ (x : R), ↑Polynomial.C x ∈ P → x = 0) : Ideal.IsMaximal (Ideal.comap Polynomial.C P)

theorem Ideal.Polynomial.quotient_mk_comp_C_isIntegral_of_jacobson {R : Type u_1} [CommRing R] [Ideal.IsJacobson R] (P : Ideal (Polynomial R)) [hP : Ideal.IsMaximal P] : RingHom.IsIntegral (RingHom.comp (Ideal.Quotient.mk P) Polynomial.C)

If R is a Jacobson ring, and P is a maximal ideal of R[X], then R → R[X]/P is an integral map.

theorem Ideal.Polynomial.isMaximal_comap_C_of_isJacobson {R : Type u_1} [CommRing R] [Ideal.IsJacobson R] (P : Ideal (Polynomial R)) [hP : Ideal.IsMaximal P] : Ideal.IsMaximal (Ideal.comap Polynomial.C P)

theorem Ideal.Polynomial.isMaximal_comap_C_of_isJacobson' {R : Type u_1} [CommRing R] [Ideal.IsJacobson R] {P : Ideal (Polynomial R)} (hP : Ideal.IsMaximal P) : Ideal.IsMaximal (Ideal.comap Polynomial.C P)

theorem Ideal.Polynomial.comp_C_integral_of_surjective_of_jacobson {R : Type u_1} [CommRing R] [Ideal.IsJacobson R] {S : Type u_2} [Field S] (f : Polynomial R →+* S) (hf : Function.Surjective ↑f) : RingHom.IsIntegral (RingHom.comp f Polynomial.C)

theorem Ideal.MvPolynomial.isJacobson_MvPolynomial_fin {R : Type u} [CommRing R] [H : Ideal.IsJacobson R] (n : ℕ) : Ideal.IsJacobson (MvPolynomial (Fin n) R)

instance Ideal.MvPolynomial.isJacobson {R : Type u_1} [CommRing R] {ι : Type u_2} [Finite ι] [Ideal.IsJacobson R] : Ideal.IsJacobson (MvPolynomial ι R)

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

theorem Ideal.MvPolynomial.quotient_mk_comp_C_isIntegral_of_jacobson {n : ℕ} {R : Type u_1} [CommRing R] [Ideal.IsJacobson R] (P : Ideal (MvPolynomial (Fin n) R)) [hP : Ideal.IsMaximal P] : RingHom.IsIntegral (RingHom.comp (Ideal.Quotient.mk P) MvPolynomial.C)

theorem Ideal.MvPolynomial.comp_C_integral_of_surjective_of_jacobson {R : Type u_1} [CommRing R] [Ideal.IsJacobson R] {σ : Type u_2} [Finite σ] {S : Type u_3} [Field S] (f : MvPolynomial σ R →+* S) (hf : Function.Surjective ↑f) : RingHom.IsIntegral (RingHom.comp f MvPolynomial.C)