mathlib documentation

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

Main statements

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] :
ideal.is_jacobson 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] :
ideal.is_jacobson 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] :
ideal.is_jacobson 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] :

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

theorem ideal.disjoint_powers_iff_not_mem {R : Type u} [comm_ring R] {y : R} {I : ideal R} :

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 : localization_map.away_map y S) [ideal.is_jacobson R] (I : ideal R) :

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 : localization_map.away_map y S) [ideal.is_jacobson R] :
{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.