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. isJacobsonRing_quotient says that the quotient of a Jacobson ring is Jacobson. isJacobsonRing_localization says the localization of a Jacobson ring to a single element is Jacobson. isJacobsonRing_polynomial_iff_isJacobsonRing 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

IsJacobsonRing 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 #

isJacobsonRing_iff_prime_eq is the equivalence between conditions 1 and 3 above.
isJacobsonRing_iff_sInf_maximal is the equivalence between conditions 1 and 2 above.
isJacobsonRing_of_surjective says that if R is a Jacobson ring and f : R →+* S is surjective, then S is also a Jacobson ring
MvPolynomial.isJacobsonRing says that multi-variate polynomials over a Jacobson ring are Jacobson.

Tags #

Jacobson, Jacobson Ring

source

class IsJacobsonRing (R : Type u_3) [CommRing R] :

Prop

A ring is a Jacobson ring if for every radical ideal I, the Jacobson radical of I is equal to I. See isJacobsonRing_iff_prime_eq and isJacobsonRing_iff_sInf_maximal for equivalent definitions.

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

Instances

source

theorem isJacobsonRing_iff {R : Type u_3} [CommRing R] :

IsJacobsonRing R ↔ ∀ (I : Ideal R), I.IsRadical → I.jacobson = I

source

theorem IsJacobsonRing.out {R : Type u_3} [CommRing R] :

IsJacobsonRing R → ∀ {I : Ideal R}, I.IsRadical → I.jacobson = I

source

theorem isJacobsonRing_iff_prime_eq {R : Type u_1} [CommRing R] :

IsJacobsonRing R ↔ ∀ (P : Ideal R), P.IsPrime → P.jacobson = 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.

source

theorem isJacobsonRing_iff_sInf_maximal {R : Type u_1} [CommRing R] :

IsJacobsonRing R ↔ ∀ {I : Ideal R}, I.IsPrime → ∃ (M : Set (Ideal R)), (∀ J ∈ M, J.IsMaximal ∨ 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.

source

theorem isJacobsonRing_iff_sInf_maximal' {R : Type u_1} [CommRing R] :

IsJacobsonRing R ↔ ∀ {I : Ideal R}, I.IsPrime → ∃ (M : Set (Ideal R)), (∀ J ∈ M, ∀ (K : Ideal R), J < K → K = ⊤) ∧ I = sInf M

A variant of isJacobsonRing_iff_sInf_maximal with a different spelling of "maximal or ⊤".

source

theorem Ideal.radical_eq_jacobson {R : Type u_1} [CommRing R] [H : IsJacobsonRing R] (I : Ideal R) :

I.radical = I.jacobson

source

@[instance 100]

instance instIsJacobsonRingOfIsArtinianRing {R : Type u_1} [CommRing R] [IsArtinianRing R] :

IsJacobsonRing R

Equations

⋯ = ⋯

source

theorem isJacobsonRing_of_surjective {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [H : IsJacobsonRing R] :

(∃ (f : R →+* S), Function.Surjective ⇑f) → IsJacobsonRing S

source

@[instance 100]

instance isJacobsonRing_quotient {R : Type u_1} [CommRing R] {I : Ideal R} [IsJacobsonRing R] :

IsJacobsonRing (R ⧸ I)

Equations

⋯ = ⋯

source

theorem isJacobsonRing_iso {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (e : R ≃+* S) :

IsJacobsonRing R ↔ IsJacobsonRing S

source

theorem isJacobsonRing_of_isIntegral {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [Algebra.IsIntegral R S] [IsJacobsonRing R] :

IsJacobsonRing S

source

theorem isJacobsonRing_of_isIntegral' {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (f : R →+* S) (hf : f.IsIntegral) [IsJacobsonRing R] :

IsJacobsonRing S

A variant of isJacobsonRing_of_isIntegral that takes RingHom.IsIntegral instead.

source

theorem IsLocalization.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 : IsJacobsonRing R] (J : Ideal S) :

J.IsMaximal ↔ (Ideal.comap (algebraMap R S) J).IsMaximal ∧ 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

source

theorem IsLocalization.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] [IsJacobsonRing R] (I : Ideal R) (hI : I.IsMaximal) (hy : y ∉ I) :

(Ideal.map (algebraMap R S) I).IsMaximal

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

source

def IsLocalization.orderIsoOfMaximal {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (y : R) [Algebra R S] [IsLocalization.Away y S] [IsJacobsonRing R] :

{ p : Ideal S // p.IsMaximal } ≃o { p : Ideal R // p.IsMaximal ∧ 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

Equations

One or more equations did not get rendered due to their size.

Instances For

source

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

IsJacobsonRing S

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

source

theorem 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)

source

theorem Polynomial.mem_closure_X_union_C {R : Type u_1} [Ring R] (p : Polynomial R) :

p ∈ Subring.closure (insert Polynomial.X {f : Polynomial R | f.degree ≤ 0})

source

theorem 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.map (Ideal.Quotient.mk (Ideal.comap Polynomial.C P)) pX).leadingCoeff Rₘ] [Algebra (Polynomial R ⧸ P) Sₘ] [IsLocalization (Submonoid.map (Ideal.quotientMap P Polynomial.C ⋯) (Submonoid.powers (Polynomial.map (Ideal.Quotient.mk (Ideal.comap Polynomial.C P)) pX).leadingCoeff)) Sₘ] :

(IsLocalization.map Sₘ (Ideal.quotientMap P Polynomial.C ⋯) ⋯).IsIntegral

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.

source

theorem Polynomial.jacobson_bot_of_integral_localization {S : Type u_2} [CommRing S] [IsDomain S] {R : Type u_5} [CommRing R] [IsDomain R] [IsJacobsonRing 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φ' : (IsLocalization.map Sₘ φ ⋯).IsIntegral) :

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

source

theorem Polynomial.isJacobsonRing_polynomial_of_isJacobsonRing {R : Type u_1} [CommRing R] (hR : IsJacobsonRing R) :

IsJacobsonRing (Polynomial R)

source

theorem Polynomial.isJacobsonRing_polynomial_iff_isJacobsonRing {R : Type u_1} [CommRing R] :

IsJacobsonRing (Polynomial R) ↔ IsJacobsonRing R

source

instance Polynomial.instIsJacobsonRing {R : Type u_1} [CommRing R] [IsJacobsonRing R] :

IsJacobsonRing (Polynomial R)

Equations

⋯ = ⋯

source

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

(Ideal.comap Polynomial.C P).IsMaximal

source

theorem Polynomial.quotient_mk_comp_C_isIntegral_of_isJacobsonRing {R : Type u_1} [CommRing R] (P : Ideal (Polynomial R)) [hP : P.IsMaximal] [IsJacobsonRing R] :

((Ideal.Quotient.mk P).comp Polynomial.C).IsIntegral

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

source

theorem Polynomial.isMaximal_comap_C_of_isJacobsonRing {R : Type u_1} [CommRing R] (P : Ideal (Polynomial R)) [hP : P.IsMaximal] [IsJacobsonRing R] :

(Ideal.comap Polynomial.C P).IsMaximal

source

theorem Polynomial.comp_C_integral_of_surjective_of_isJacobsonRing {R : Type u_1} [CommRing R] [IsJacobsonRing R] {S : Type u_2} [Field S] (f : Polynomial R →+* S) (hf : Function.Surjective ⇑f) :

(f.comp Polynomial.C).IsIntegral

source

theorem MvPolynomial.isJacobsonRing_MvPolynomial_fin {R : Type u} [CommRing R] [H : IsJacobsonRing R] (n : ℕ) :

IsJacobsonRing (MvPolynomial (Fin n) R)

source

instance MvPolynomial.isJacobsonRing {R : Type u_1} [CommRing R] {ι : Type u_2} [Finite ι] [IsJacobsonRing R] :

IsJacobsonRing (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

Equations

⋯ = ⋯

source

theorem MvPolynomial.quotient_mk_comp_C_isIntegral_of_isJacobsonRing {n : ℕ} {R : Type u_1} [CommRing R] [IsJacobsonRing R] (P : Ideal (MvPolynomial (Fin n) R)) [hP : P.IsMaximal] :

((Ideal.Quotient.mk P).comp MvPolynomial.C).IsIntegral

source

theorem MvPolynomial.comp_C_integral_of_surjective_of_isJacobsonRing {R : Type u_1} [CommRing R] [IsJacobsonRing R] {σ : Type u_2} [Finite σ] {S : Type u_3} [Field S] (f : MvPolynomial σ R →+* S) (hf : Function.Surjective ⇑f) :

(f.comp MvPolynomial.C).IsIntegral

source

theorem isJacobsonRing_of_finiteType {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] [IsJacobsonRing A] [Algebra.FiniteType A B] :

IsJacobsonRing B

source

theorem RingHom.FiniteType.isJacobsonRing {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] {f : A →+* B} [IsJacobsonRing A] (H : f.FiniteType) :

IsJacobsonRing B

source

theorem finite_of_finite_type_of_isJacobsonRing (R : Type u_1) (S : Type u_2) [CommRing R] [Field S] [Algebra R S] [IsJacobsonRing R] [Algebra.FiniteType R S] :

Module.Finite R S

source

theorem RingHom.finite_iff_finiteType_of_isJacobsonRing {R : Type u_1} {S : Type u_2} [CommRing R] [IsJacobsonRing R] [Field S] {f : R →+* S} :

f.Finite ↔ f.FiniteType

If f : R →+* S is a ring homomorphism from a jacobson ring to a field, then it is finite if and only if it is finite type.

source

@[deprecated IsJacobsonRing]

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

Prop

Alias of IsJacobsonRing.

Equations

Ideal.IsJacobson = IsJacobsonRing

Instances For

source

@[deprecated isJacobsonRing_iff]

theorem Ideal.isJacobson_iff {R : Type u_3} [CommRing R] :

IsJacobsonRing R ↔ ∀ (I : Ideal R), I.IsRadical → I.jacobson = I

Alias of isJacobsonRing_iff.

source

@[deprecated IsJacobsonRing.out]

theorem Ideal.IsJacobson.out {R : Type u_3} [CommRing R] :

IsJacobsonRing R → ∀ {I : Ideal R}, I.IsRadical → I.jacobson = I

Alias of IsJacobsonRing.out.

source

@[deprecated isJacobsonRing_iff_prime_eq]

theorem Ideal.isJacobson_iff_prime_eq {R : Type u_1} [CommRing R] :

IsJacobsonRing R ↔ ∀ (P : Ideal R), P.IsPrime → P.jacobson = P

Alias of isJacobsonRing_iff_prime_eq.

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

source

@[deprecated isJacobsonRing_iff_sInf_maximal]

theorem Ideal.isJacobson_iff_sInf_maximal {R : Type u_1} [CommRing R] :

IsJacobsonRing R ↔ ∀ {I : Ideal R}, I.IsPrime → ∃ (M : Set (Ideal R)), (∀ J ∈ M, J.IsMaximal ∨ J = ⊤) ∧ I = sInf M

Alias of isJacobsonRing_iff_sInf_maximal.

source

@[deprecated isJacobsonRing_iff_sInf_maximal']

theorem Ideal.isJacobson_iff_sInf_maximal' {R : Type u_1} [CommRing R] :

IsJacobsonRing R ↔ ∀ {I : Ideal R}, I.IsPrime → ∃ (M : Set (Ideal R)), (∀ J ∈ M, ∀ (K : Ideal R), J < K → K = ⊤) ∧ I = sInf M

Alias of isJacobsonRing_iff_sInf_maximal'.

A variant of isJacobsonRing_iff_sInf_maximal with a different spelling of "maximal or ⊤".

source

@[deprecated isJacobsonRing_of_surjective]

theorem Ideal.isJacobson_of_surjective {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [H : IsJacobsonRing R] :

(∃ (f : R →+* S), Function.Surjective ⇑f) → IsJacobsonRing S

Alias of isJacobsonRing_of_surjective.

source

@[deprecated isJacobsonRing_iso]

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

IsJacobsonRing R ↔ IsJacobsonRing S

Alias of isJacobsonRing_iso.

source

@[deprecated isJacobsonRing_of_isIntegral]

theorem Ideal.isJacobson_of_isIntegral {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [Algebra.IsIntegral R S] [IsJacobsonRing R] :

IsJacobsonRing S

Alias of isJacobsonRing_of_isIntegral.

source

@[deprecated isJacobsonRing_of_isIntegral']

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

IsJacobsonRing S

Alias of isJacobsonRing_of_isIntegral'.

A variant of isJacobsonRing_of_isIntegral that takes RingHom.IsIntegral instead.

source

@[deprecated IsLocalization.isMaximal_iff_isMaximal_disjoint]

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 : IsJacobsonRing R] (J : Ideal S) :

J.IsMaximal ↔ (Ideal.comap (algebraMap R S) J).IsMaximal ∧ y ∉ Ideal.comap (algebraMap R S) J

Alias of IsLocalization.isMaximal_iff_isMaximal_disjoint.

source

@[deprecated IsLocalization.isMaximal_of_isMaximal_disjoint]

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] [IsJacobsonRing R] (I : Ideal R) (hI : I.IsMaximal) (hy : y ∉ I) :

(Ideal.map (algebraMap R S) I).IsMaximal

Alias of IsLocalization.isMaximal_of_isMaximal_disjoint.

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

source

@[deprecated isJacobsonRing_localization]

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 : IsJacobsonRing R] :

IsJacobsonRing S

Alias of isJacobsonRing_localization.

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

source

@[deprecated Polynomial.isIntegral_isLocalization_polynomial_quotient]

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.map (Ideal.Quotient.mk (Ideal.comap Polynomial.C P)) pX).leadingCoeff Rₘ] [Algebra (Polynomial R ⧸ P) Sₘ] [IsLocalization (Submonoid.map (Ideal.quotientMap P Polynomial.C ⋯) (Submonoid.powers (Polynomial.map (Ideal.Quotient.mk (Ideal.comap Polynomial.C P)) pX).leadingCoeff)) Sₘ] :

(IsLocalization.map Sₘ (Ideal.quotientMap P Polynomial.C ⋯) ⋯).IsIntegral

Alias of Polynomial.isIntegral_isLocalization_polynomial_quotient.

source

@[deprecated Polynomial.jacobson_bot_of_integral_localization]

theorem Ideal.Polynomial.jacobson_bot_of_integral_localization {S : Type u_2} [CommRing S] [IsDomain S] {R : Type u_5} [CommRing R] [IsDomain R] [IsJacobsonRing 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φ' : (IsLocalization.map Sₘ φ ⋯).IsIntegral) :

⊥.jacobson = ⊥

Alias of Polynomial.jacobson_bot_of_integral_localization.

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

source

@[deprecated Polynomial.isJacobsonRing_polynomial_of_isJacobsonRing]