mathlibdocumentation

ring_theory.jacobson

Jacobson Rings #

The following conditions are equivalent for a ring R:

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. 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 that R is a Jacobson ring. It is a class, implemented as the predicate that for any ideal, I.radical = I implies I.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 if R is a Jacobson ring and f : R →+* S is surjective, then S is also a Jacobson ring
• is_jacobson_mv_polynomial says that multi-variate polynomials over a Jacobson ring are Jacobson.

Tags #

Jacobson, Jacobson Ring

@[class]
structure ideal.is_jacobson (R : Type u_3) [comm_ring R] :
Prop

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.

Instances
theorem ideal.is_jacobson_iff {R : Type u_1} [comm_ring R] :
∀ (I : ideal R), I.radical = II.jacobson = I
theorem ideal.is_jacobson.out {R : Type u_1} [comm_ring R] :
∀ {I : ideal R}, I.radical = II.jacobson = I
theorem ideal.is_jacobson_iff_prime_eq {R : Type u_1} [comm_ring R] :
∀ (P : ideal R), P.is_primeP.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.

theorem ideal.is_jacobson_iff_Inf_maximal {R : Type u_1} [comm_ring R] :
∀ {I : ideal R}, I.is_prime(∃ (M : set (ideal R)), (∀ (J : ideal R), J MJ.is_maximal J = ) I = Inf 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.is_jacobson_iff_Inf_maximal' {R : Type u_1} [comm_ring R] :
∀ {I : ideal R}, I.is_prime(∃ (M : set (ideal R)), (∀ (J : ideal R), J M∀ (K : ideal R), J < KK = ) I = Inf M)
theorem ideal.radical_eq_jacobson {R : Type u_1} [comm_ring R] [H : ideal.is_jacobson R] (I : ideal R) :
@[protected, instance]
def ideal.is_jacobson_field {K : Type u_1} [field K] :

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

theorem ideal.is_jacobson_of_surjective {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [H : ideal.is_jacobson R] :
(∃ (f : R →+* S),
@[protected, instance]
def ideal.is_jacobson_quotient {R : Type u_1} [comm_ring R] {I : ideal R}  :
theorem ideal.is_jacobson_iso {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] (e : R ≃+* S) :
theorem ideal.is_jacobson_of_is_integral {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [ S] (hRS : S) (hR : ideal.is_jacobson R) :
theorem ideal.is_jacobson_of_is_integral' {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] (f : R →+* S) (hf : f.is_integral) (hR : ideal.is_jacobson R) :
theorem ideal.disjoint_powers_iff_not_mem {R : Type u_1} [comm_ring R] {I : ideal R} (y : R) (hI : I.radical = I) :
theorem ideal.is_maximal_iff_is_maximal_disjoint {R : Type u_1} (S : Type u_2) [comm_ring R] [comm_ring S] (y : R) [ S] [ S] [H : ideal.is_jacobson R] (J : ideal S) :

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

theorem ideal.is_maximal_of_is_maximal_disjoint {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] (y : R) [ S] [ S] (I : ideal R) (hI : I.is_maximal) (hy : y 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_rel_iso_of_maximal for the more general statement, and the reverse of this implication

def ideal.order_iso_of_maximal {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] (y : R) [ S] [ S]  :
{p // p.is_maximal} ≃o {p // p.is_maximal 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
theorem ideal.is_jacobson_localization {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] (y : R) [ S] [ S] [H : ideal.is_jacobson R] :

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

theorem ideal.polynomial.is_integral_is_localization_polynomial_quotient {R : Type u_1} [comm_ring R] {Rₘ : Type u_3} {Sₘ : Type u_4} [comm_ring Rₘ] [comm_ring Sₘ] (P : ideal (polynomial R)) (pX : polynomial R) (hpX : pX P) [algebra (R Rₘ] [algebra P) Sₘ]  :

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.

theorem ideal.polynomial.jacobson_bot_of_integral_localization {S : Type u_2} [comm_ring S] [is_domain S] {R : Type u_1} [comm_ring R] [is_domain R] (Rₘ : Type u_3) (Sₘ : Type u_4) [comm_ring Rₘ] [comm_ring Sₘ] (φ : R →+* S) (hφ : function.injective φ) (x : R) (hx : x 0) [ Rₘ] [ Rₘ] [ Sₘ] [ Sₘ] (hφ' : φ _).is_integral) :

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

@[protected, instance]
theorem ideal.polynomial.is_maximal_comap_C_of_is_maximal {R : Type u_1} [comm_ring R] (P : ideal (polynomial R)) [hP : P.is_maximal] [nontrivial R] (hP' : ∀ (x : R), x = 0) :

If R is a Jacobson ring, and P is a maximal ideal of polynomial R, then R → (polynomial R)/P is an integral map.

theorem ideal.polynomial.comp_C_integral_of_surjective_of_jacobson {R : Type u_1} [comm_ring R] {S : Type u_2} [field S] (f : →+* S) (hf : function.surjective f) :
@[protected, instance]
def ideal.mv_polynomial.mv_polynomial.ideal.is_jacobson {R : Type u_1} [comm_ring R] {ι : Type u_2} [fintype ι]  :

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.mv_polynomial.comp_C_integral_of_surjective_of_jacobson {R : Type u_1} [comm_ring R] {σ : Type u_2} [fintype σ] {S : Type u_3} [field S] (f : →+* S) (hf : function.surjective f) :