# mathlib3documentation

ring_theory.jacobson

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

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. 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.is_radical 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 of this typeclass
theorem ideal.is_jacobson_iff {R : Type u_1} [comm_ring R] :
(I : ideal R), I.is_radical I.jacobson = I
theorem ideal.is_jacobson.out {R : Type u_1} [comm_ring R] :
{I : ideal R}, I.is_radical I.jacobson = I
theorem ideal.is_jacobson_iff_prime_eq {R : Type u_1} [comm_ring R] :
(P : ideal R), P.is_prime 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.

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 J.is_maximal J = ) I =

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 < K K = ) I =
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.is_radical) :
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 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.

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 R[X], then R → R[X]/P is an integral map.

@[protected, instance]
def ideal.mv_polynomial.is_jacobson {R : Type u_1} [comm_ring R] {ι : Type u_2} [finite ι]  :

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