mathlib3 documentation

ring_theory.jacobson_ideal

Jacobson radical #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

The Jacobson radical of a ring R is defined to be the intersection of all maximal ideals of R. This is similar to how the nilradical is equal to the intersection of all prime ideals of R.

We can extend the idea of the nilradical to ideals of R, by letting the radical of an ideal I be the intersection of prime ideals containing I. Under this extension, the original nilradical is the radical of the zero ideal ⊥. Here we define the Jacobson radical of an ideal I in a similar way, as the intersection of maximal ideals containing I.

Main definitions #

Let R be a commutative ring, and I be an ideal of R

jacobson I is the jacobson radical, i.e. the infimum of all maximal ideals containing I.
is_local I is the proposition that the jacobson radical of I is itself a maximal ideal

Main statements #

mem_jacobson_iff gives a characterization of members of the jacobson of I
is_local_of_is_maximal_radical: if the radical of I is maximal then so is the jacobson radical

Tags #

Jacobson, Jacobson radical, Local Ideal

def ideal.jacobson {R : Type u} [ring R] (I : ideal R) :

The Jacobson radical of I is the infimum of all maximal (left) ideals containing I.

Equations

I.jacobson = has_Inf.Inf {J : ideal R | I ≤ J ∧ J.is_maximal}

Instances for ideal.jacobson

ideal.jacobson.is_maximal

theorem ideal.le_jacobson {R : Type u} [ring R] {I : ideal R} :

I ≤ I.jacobson

@[simp]

theorem ideal.jacobson_idem {R : Type u} [ring R] {I : ideal R} :

I.jacobson.jacobson = I.jacobson

@[simp]

theorem ideal.jacobson_top {R : Type u} [ring R] :

⊤.jacobson = ⊤

@[simp]

theorem ideal.jacobson_eq_top_iff {R : Type u} [ring R] {I : ideal R} :

I.jacobson = ⊤ ↔ I = ⊤

theorem ideal.jacobson_eq_bot {R : Type u} [ring R] {I : ideal R} :

I.jacobson = ⊥ → I = ⊥

theorem ideal.jacobson_eq_self_of_is_maximal {R : Type u} [ring R] {I : ideal R} [H : I.is_maximal] :

@[protected, instance]

def ideal.jacobson.is_maximal {R : Type u} [ring R] {I : ideal R} [H : I.is_maximal] :

I.jacobson.is_maximal

theorem ideal.mem_jacobson_iff {R : Type u} [ring R] {I : ideal R} {x : R} :

x ∈ I.jacobson ↔ ∀ (y : R), ∃ (z : R), z * y * x + z - 1 ∈ I

theorem ideal.exists_mul_sub_mem_of_sub_one_mem_jacobson {R : Type u} [ring R] {I : ideal R} (r : R) (h : r - 1 ∈ I.jacobson) :

∃ (s : R), s * r - 1 ∈ I

theorem ideal.eq_jacobson_iff_Inf_maximal {R : Type u} [ring R] {I : ideal R} :

I.jacobson = I ↔ ∃ (M : set (ideal R)), (∀ (J : ideal R), J ∈ M → J.is_maximal ∨ J = ⊤) ∧ I = has_Inf.Inf M

An ideal equals its Jacobson radical iff it is the intersection of a set of maximal ideals. Allowing the set to include ⊤ is equivalent, and is included only to simplify some proofs.

theorem ideal.eq_jacobson_iff_Inf_maximal' {R : Type u} [ring R] {I : ideal R} :

I.jacobson = I ↔ ∃ (M : set (ideal R)), (∀ (J : ideal R), J ∈ M → ∀ (K : ideal R), J < K → K = ⊤) ∧ I = has_Inf.Inf M

theorem ideal.eq_jacobson_iff_not_mem {R : Type u} [ring R] {I : ideal R} :

I.jacobson = I ↔ ∀ (x : R), x ∉ I → (∃ (M : ideal R), (I ≤ M ∧ M.is_maximal) ∧ x ∉ M)

An ideal I equals its Jacobson radical if and only if every element outside I also lies outside of a maximal ideal containing I.

theorem ideal.map_jacobson_of_surjective {R : Type u} {S : Type v} [ring R] [ring S] {I : ideal R} {f : R →+* S} (hf : function.surjective ⇑f) :

ring_hom.ker f ≤ I → ideal.map f I.jacobson = (ideal.map f I).jacobson

theorem ideal.map_jacobson_of_bijective {R : Type u} {S : Type v} [ring R] [ring S] {I : ideal R} {f : R →+* S} (hf : function.bijective ⇑f) :

ideal.map f I.jacobson = (ideal.map f I).jacobson

theorem ideal.comap_jacobson {R : Type u} {S : Type v} [ring R] [ring S] {f : R →+* S} {K : ideal S} :

ideal.comap f K.jacobson = has_Inf.Inf (ideal.comap f '' {J : ideal S | K ≤ J ∧ J.is_maximal})

theorem ideal.comap_jacobson_of_surjective {R : Type u} {S : Type v} [ring R] [ring S] {f : R →+* S} (hf : function.surjective ⇑f) {K : ideal S} :

ideal.comap f K.jacobson = (ideal.comap f K).jacobson

theorem ideal.jacobson_mono {R : Type u} [ring R] {I J : ideal R} :

I ≤ J → I.jacobson ≤ J.jacobson

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

I.radical ≤ I.jacobson

theorem ideal.is_radical_of_eq_jacobson {R : Type u} [comm_ring R] {I : ideal R} (h : I.jacobson = I) :

theorem ideal.is_unit_of_sub_one_mem_jacobson_bot {R : Type u} [comm_ring R] (r : R) (h : r - 1 ∈ ⊥.jacobson) :

theorem ideal.mem_jacobson_bot {R : Type u} [comm_ring R] {x : R} :

x ∈ ⊥.jacobson ↔ ∀ (y : R), is_unit (x * y + 1)

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

I.jacobson = I ↔ ⊥.jacobson = ⊥

An ideal I of R is equal to its Jacobson radical if and only if the Jacobson radical of the quotient ring R/I is the zero ideal

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

I.radical = I.jacobson ↔ ⊥.radical = ⊥.jacobson

The standard radical and Jacobson radical of an ideal I of R are equal if and only if the nilradical and Jacobson radical of the quotient ring R/I coincide

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

I.radical.jacobson = I.jacobson

theorem ideal.jacobson_bot_polynomial_le_Inf_map_maximal {R : Type u} [comm_ring R] :

⊥.jacobson ≤ has_Inf.Inf (ideal.map polynomial.C '' {J : ideal R | J.is_maximal})

theorem ideal.jacobson_bot_polynomial_of_jacobson_bot {R : Type u} [comm_ring R] (h : ⊥.jacobson = ⊥) :

⊥.jacobson = ⊥

@[class]

structure ideal.is_local {R : Type u} [comm_ring R] (I : ideal R) :

Prop

out : I.jacobson.is_maximal

An ideal I is local iff its Jacobson radical is maximal.

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

I.is_local ↔ I.jacobson.is_maximal

theorem ideal.is_local_of_is_maximal_radical {R : Type u} [comm_ring R] {I : ideal R} (hi : I.radical.is_maximal) :

theorem ideal.is_local.le_jacobson {R : Type u} [comm_ring R] {I J : ideal R} (hi : I.is_local) (hij : I ≤ J) (hj : J ≠ ⊤) :

J ≤ I.jacobson

theorem ideal.is_local.mem_jacobson_or_exists_inv {R : Type u} [comm_ring R] {I : ideal R} (hi : I.is_local) (x : R) :

x ∈ I.jacobson ∨ ∃ (y : R), y * x - 1 ∈ I

theorem ideal.is_primary_of_is_maximal_radical {R : Type u} [comm_ring R] {I : ideal R} (hi : I.radical.is_maximal) :