Documentation

Mathlib.RingTheory.JacobsonIdeal

Jacobson radical #

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 of R to ideals of R, by letting the nilradical 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 ring, and I be a left ideal of R

Furthermore when I is a two-sided ideal of R

Main statements #

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
Instances For
    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_isMaximal {R : Type u} [Ring R] {I : Ideal R} [H : I.IsMaximal] :
    I.jacobson = I
    @[instance 100]
    instance Ideal.jacobson.isMaximal {R : Type u} [Ring R] {I : Ideal R} [H : I.IsMaximal] :
    I.jacobson.IsMaximal
    Equations
    • =
    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_add_sub_mem_of_mem_jacobson {R : Type u} [Ring R] {I : Ideal R} (r : R) (h : r I.jacobson) :
    ∃ (s : R), s * (r + 1) - 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_sInf_maximal {R : Type u} [Ring R] {I : Ideal R} :
    I.jacobson = I ∃ (M : Set (Ideal R)), (∀ JM, J.IsMaximal J = ) I = sInf 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_sInf_maximal' {R : Type u} [Ring R] {I : Ideal R} :
    I.jacobson = I ∃ (M : Set (Ideal R)), (∀ JM, ∀ (K : Ideal R), J < KK = ) I = sInf M
    theorem Ideal.eq_jacobson_iff_not_mem {R : Type u} [Ring R] {I : Ideal R} :
    I.jacobson = I xI, ∃ (M : Ideal R), (I M M.IsMaximal) xM

    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) :
    RingHom.ker f IIdeal.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 = sInf (Ideal.comap f '' {J : Ideal S | K J J.IsMaximal})
    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 : Ideal R} {J : Ideal R} :
    I JI.jacobson J.jacobson
    theorem Ideal.jacobson_mul_mem_right {R : Type u} [Ring R] {I : Ideal R} (mul_mem_right : ∀ {x y : R}, x Ix * y I) {x : R} {y : R} :
    x I.jacobsonx * y I.jacobson

    The Jacobson radical of a two-sided ideal is two-sided.

    It is preferable to use TwoSidedIdeal.jacobson instead of this lemma.

    theorem Ideal.radical_le_jacobson {R : Type u} [CommRing R] {I : Ideal R} :
    I.radical I.jacobson
    theorem Ideal.isRadical_of_eq_jacobson {R : Type u} [CommRing R] {I : Ideal R} (h : I.jacobson = I) :
    I.IsRadical
    theorem Ideal.isUnit_of_sub_one_mem_jacobson_bot {R : Type u} [CommRing R] (r : R) (h : r - 1 .jacobson) :
    theorem Ideal.mem_jacobson_bot {R : Type u} [CommRing R] {x : R} :
    x .jacobson ∀ (y : R), IsUnit (x * y + 1)
    theorem Ideal.jacobson_eq_iff_jacobson_quotient_eq_bot {R : Type u} [CommRing 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} [CommRing 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} [CommRing R] {I : Ideal R} :
    I.radical.jacobson = I.jacobson
    theorem Ideal.jacobson_bot_polynomial_le_sInf_map_maximal {R : Type u} [CommRing R] :
    .jacobson sInf (Ideal.map Polynomial.C '' {J : Ideal R | J.IsMaximal})
    theorem Ideal.jacobson_bot_polynomial_of_jacobson_bot {R : Type u} [CommRing R] (h : .jacobson = ) :
    .jacobson =
    class Ideal.IsLocal {R : Type u} [CommRing R] (I : Ideal R) :

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

    • out : I.jacobson.IsMaximal

      A ring R is local if and only if its jacobson radical is maximal

    Instances
      theorem Ideal.IsLocal.out {R : Type u} :
      ∀ {inst : CommRing R} {I : Ideal R} [self : I.IsLocal], I.jacobson.IsMaximal

      A ring R is local if and only if its jacobson radical is maximal

      theorem Ideal.isLocal_iff {R : Type u} [CommRing R] {I : Ideal R} :
      I.IsLocal I.jacobson.IsMaximal
      theorem Ideal.isLocal_of_isMaximal_radical {R : Type u} [CommRing R] {I : Ideal R} (hi : I.radical.IsMaximal) :
      I.IsLocal
      theorem Ideal.IsLocal.le_jacobson {R : Type u} [CommRing R] {I : Ideal R} {J : Ideal R} (hi : I.IsLocal) (hij : I J) (hj : J ) :
      J I.jacobson
      theorem Ideal.IsLocal.mem_jacobson_or_exists_inv {R : Type u} [CommRing R] {I : Ideal R} (hi : I.IsLocal) (x : R) :
      x I.jacobson ∃ (y : R), y * x - 1 I
      theorem Ideal.isPrimary_of_isMaximal_radical {R : Type u} [CommRing R] {I : Ideal R} (hi : I.radical.IsMaximal) :
      I.IsPrimary

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

      Equations
      • I.jacobson = (TwoSidedIdeal.asIdeal I).jacobson.toTwoSided
      Instances For
        theorem TwoSidedIdeal.asIdeal_jacobson {R : Type u} [Ring R] (I : TwoSidedIdeal R) :
        TwoSidedIdeal.asIdeal I.jacobson = (TwoSidedIdeal.asIdeal I).jacobson