# mathlibdocumentation

ring_theory.jacobson

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

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

## Tags

Jacobson, Jacobson Ring

@[class]
def ideal.is_jacobson (R : Type u) [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.

Equations
Instances
theorem ideal.is_jacobson_iff_prime_eq {R : Type u} [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} [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} [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} [comm_ring R] (H : ideal.is_jacobson R) (I : ideal R) :

@[instance]
def ideal.is_jacobson_field {K : Type u} [field K] :

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

theorem ideal.is_jacobson_of_surjective {R : Type u} [comm_ring R] {S : Type v} [comm_ring S] [H : ideal.is_jacobson R] :
(∃ (f : R →+* S),

@[instance]
def ideal.is_jacobson_quotient {R : Type u} [comm_ring R] {I : ideal R}  :

theorem ideal.is_jacobson_iso {R : Type u} [comm_ring R] {S : Type v} [comm_ring S] :
R ≃+* S

theorem ideal.is_jacobson_of_is_integral {R : Type u} [comm_ring R] {S : Type v} [comm_ring S] [ S] :

theorem ideal.disjoint_powers_iff_not_mem {R : Type u} [comm_ring R] {y : R} {I : ideal R} :
I.radical = I I y I.carrier)

theorem ideal.is_maximal_iff_is_maximal_disjoint {R : Type u} [comm_ring R] {S : Type v} [comm_ring S] {y : R} (f : 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} [comm_ring R] {S : Type v} [comm_ring S] {y : R} (f : S) (I : ideal R) :
I.is_maximaly 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} [comm_ring R] {S : Type v} [comm_ring S] {y : R} (f : 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} [comm_ring R] {S : Type v} [comm_ring S] {y : R} [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.