Documentation

Mathlib.RingTheory.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. isJacobson_quotient says that the quotient of a Jacobson ring is Jacobson. isJacobson_localization says the localization of a Jacobson ring to a single element is Jacobson. isJacobson_polynomial_iff_isJacobson 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

Main statements #

Tags #

Jacobson, Jacobson Ring

class Ideal.IsJacobson (R : Type u_3) [CommRing R] :

A ring is a Jacobson ring if for every radical ideal I, the Jacobson radical of I is equal to I. See isJacobson_iff_prime_eq and isJacobson_iff_sInf_maximal for equivalent definitions.

  • out' : ∀ (I : Ideal R), I.IsRadicalI.jacobson = I
Instances
    theorem Ideal.IsJacobson.out' {R : Type u_3} [CommRing R] [self : Ideal.IsJacobson R] (I : Ideal R) :
    I.IsRadicalI.jacobson = I
    theorem Ideal.isJacobson_iff {R : Type u_3} [CommRing R] :
    Ideal.IsJacobson R ∀ (I : Ideal R), I.IsRadicalI.jacobson = I
    theorem Ideal.IsJacobson.out {R : Type u_3} [CommRing R] :
    Ideal.IsJacobson R∀ {I : Ideal R}, I.IsRadicalI.jacobson = I
    theorem Ideal.isJacobson_iff_prime_eq {R : Type u_1} [CommRing R] :
    Ideal.IsJacobson R ∀ (P : Ideal R), P.IsPrimeP.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.isJacobson_iff_sInf_maximal {R : Type u_1} [CommRing R] :
    Ideal.IsJacobson R ∀ {I : Ideal R}, I.IsPrime∃ (M : Set (Ideal R)), (JM, J.IsMaximal J = ) I = sInf 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.isJacobson_iff_sInf_maximal' {R : Type u_1} [CommRing R] :
    Ideal.IsJacobson R ∀ {I : Ideal R}, I.IsPrime∃ (M : Set (Ideal R)), (JM, ∀ (K : Ideal R), J < KK = ) I = sInf M
    theorem Ideal.radical_eq_jacobson {R : Type u_1} [CommRing R] [H : Ideal.IsJacobson R] (I : Ideal R) :
    I.radical = I.jacobson
    @[instance 100]

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

    Equations
    • =
    theorem Ideal.isJacobson_of_surjective {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [H : Ideal.IsJacobson R] :
    (∃ (f : R →+* S), Function.Surjective f)Ideal.IsJacobson S
    @[instance 100]
    Equations
    • =
    theorem Ideal.isJacobson_of_isIntegral' {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (f : R →+* S) (hf : f.IsIntegral) (hR : Ideal.IsJacobson R) :
    theorem Ideal.isMaximal_iff_isMaximal_disjoint {R : Type u_1} (S : Type u_2) [CommRing R] [CommRing S] (y : R) [Algebra R S] [IsLocalization.Away y S] [H : Ideal.IsJacobson R] (J : Ideal S) :
    J.IsMaximal (Ideal.comap (algebraMap R S) J).IsMaximal yIdeal.comap (algebraMap R S) J

    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_relIso_of_maximal for the more general relation isomorphism

    theorem Ideal.isMaximal_of_isMaximal_disjoint {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (y : R) [Algebra R S] [IsLocalization.Away y S] [Ideal.IsJacobson R] (I : Ideal R) (hI : I.IsMaximal) (hy : yI) :
    (Ideal.map (algebraMap R S) I).IsMaximal

    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_relIso_of_maximal for the more general statement, and the reverse of this implication

    def Ideal.orderIsoOfMaximal {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (y : R) [Algebra R S] [IsLocalization.Away y S] [Ideal.IsJacobson R] :
    { p : Ideal S // p.IsMaximal } ≃o { p : Ideal R // p.IsMaximal yp }

    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
    • One or more equations did not get rendered due to their size.
    Instances For
      theorem Ideal.isJacobson_localization {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (y : R) [Algebra R S] [IsLocalization.Away y S] [H : Ideal.IsJacobson 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.Subring.mem_closure_image_of {S : Type u_1} {T : Type u_2} [CommRing S] [CommRing T] (g : S →+* T) (u : Set S) (x : S) (hx : x Subring.closure u) :
      g x Subring.closure (g '' u)
      theorem Ideal.Polynomial.mem_closure_X_union_C {R : Type u_1} [Ring R] (p : Polynomial R) :
      p Subring.closure (insert Polynomial.X {f : Polynomial R | f.degree 0})
      theorem Ideal.Polynomial.isIntegral_isLocalization_polynomial_quotient {R : Type u_1} [CommRing R] {Rₘ : Type u_3} {Sₘ : Type u_4} [CommRing Rₘ] [CommRing Sₘ] (P : Ideal (Polynomial R)) (pX : Polynomial R) (hpX : pX P) [Algebra (R Ideal.comap Polynomial.C P) Rₘ] [IsLocalization.Away (Polynomial.map (Ideal.Quotient.mk (Ideal.comap Polynomial.C P)) pX).leadingCoeff Rₘ] [Algebra (Polynomial R P) Sₘ] [IsLocalization (Submonoid.map (Ideal.quotientMap P Polynomial.C ) (Submonoid.powers (Polynomial.map (Ideal.Quotient.mk (Ideal.comap Polynomial.C P)) pX).leadingCoeff)) Sₘ] :
      (IsLocalization.map Sₘ (Ideal.quotientMap P Polynomial.C ) ).IsIntegral

      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.leadingCoeff. 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} [CommRing S] [IsDomain S] {R : Type u_5} [CommRing R] [IsDomain R] [Ideal.IsJacobson R] (Rₘ : Type u_6) (Sₘ : Type u_7) [CommRing Rₘ] [CommRing Sₘ] (φ : R →+* S) (hφ : Function.Injective φ) (x : R) (hx : x 0) [Algebra R Rₘ] [IsLocalization.Away x Rₘ] [Algebra S Sₘ] [IsLocalization (Submonoid.map φ (Submonoid.powers x)) Sₘ] (hφ' : (IsLocalization.map Sₘ φ ).IsIntegral) :
      .jacobson =

      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

      theorem Ideal.Polynomial.isMaximal_comap_C_of_isMaximal {R : Type u_1} [CommRing R] [Ideal.IsJacobson R] (P : Ideal (Polynomial R)) [hP : P.IsMaximal] [Nontrivial R] (hP' : ∀ (x : R), Polynomial.C x Px = 0) :
      (Ideal.comap Polynomial.C P).IsMaximal
      theorem Ideal.Polynomial.quotient_mk_comp_C_isIntegral_of_jacobson {R : Type u_1} [CommRing R] [Ideal.IsJacobson R] (P : Ideal (Polynomial R)) [hP : P.IsMaximal] :
      ((Ideal.Quotient.mk P).comp Polynomial.C).IsIntegral

      If R is a Jacobson ring, and P is a maximal ideal of R[X], then R → R[X]/P is an integral map.

      theorem Ideal.Polynomial.isMaximal_comap_C_of_isJacobson {R : Type u_1} [CommRing R] [Ideal.IsJacobson R] (P : Ideal (Polynomial R)) [hP : P.IsMaximal] :
      (Ideal.comap Polynomial.C P).IsMaximal
      theorem Ideal.Polynomial.isMaximal_comap_C_of_isJacobson' {R : Type u_1} [CommRing R] [Ideal.IsJacobson R] {P : Ideal (Polynomial R)} (hP : P.IsMaximal) :
      (Ideal.comap Polynomial.C P).IsMaximal
      theorem Ideal.Polynomial.comp_C_integral_of_surjective_of_jacobson {R : Type u_1} [CommRing R] [Ideal.IsJacobson R] {S : Type u_2} [Field S] (f : Polynomial R →+* S) (hf : Function.Surjective f) :
      (f.comp Polynomial.C).IsIntegral

      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

      Equations
      • =
      theorem Ideal.MvPolynomial.quotient_mk_comp_C_isIntegral_of_jacobson {n : } {R : Type u_1} [CommRing R] [Ideal.IsJacobson R] (P : Ideal (MvPolynomial (Fin n) R)) [hP : P.IsMaximal] :
      ((Ideal.Quotient.mk P).comp MvPolynomial.C).IsIntegral
      theorem Ideal.MvPolynomial.comp_C_integral_of_surjective_of_jacobson {R : Type u_1} [CommRing R] [Ideal.IsJacobson R] {σ : Type u_2} [Finite σ] {S : Type u_3} [Field S] (f : MvPolynomial σ R →+* S) (hf : Function.Surjective f) :
      (f.comp MvPolynomial.C).IsIntegral