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. is_jacobson_polynomial_iff_is_jacobson 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]
structure ideal.is_jacobson (R : Type u_3) [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.

Instances of this typeclass
theorem ideal.is_jacobson_iff {R : Type u_1} [comm_ring R] :
ideal.is_jacobson R ∀ (I : ideal R), I.radical = II.jacobson = I
theorem ideal.is_jacobson.out {R : Type u_1} [comm_ring R] :
ideal.is_jacobson R∀ {I : ideal R}, I.radical = II.jacobson = I
theorem ideal.is_jacobson_iff_prime_eq {R : Type u_1} [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_1} [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 = has_Inf.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_1} [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 = has_Inf.Inf M)
theorem ideal.radical_eq_jacobson {R : Type u_1} [comm_ring R] [H : ideal.is_jacobson R] (I : ideal R) :
@[protected, instance]
def ideal.is_jacobson_field {K : Type u_1} [field K] :

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

theorem ideal.is_jacobson_of_surjective {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [H : ideal.is_jacobson R] :
@[protected, instance]
theorem ideal.is_jacobson_iso {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] (e : R ≃+* S) :
theorem ideal.is_jacobson_of_is_integral {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [algebra R S] (hRS : algebra.is_integral R S) (hR : ideal.is_jacobson R) :
theorem ideal.is_jacobson_of_is_integral' {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] (f : R →+* S) (hf : f.is_integral) (hR : ideal.is_jacobson R) :
theorem ideal.disjoint_powers_iff_not_mem {R : Type u_1} [comm_ring R] {I : ideal R} (y : R) (hI : I.radical = I) :
theorem ideal.is_maximal_iff_is_maximal_disjoint {R : Type u_1} (S : Type u_2) [comm_ring R] [comm_ring S] (y : R) [algebra R S] [is_localization.away y 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_1} {S : Type u_2} [comm_ring R] [comm_ring S] (y : R) [algebra R S] [is_localization.away y S] [ideal.is_jacobson R] (I : ideal R) (hI : I.is_maximal) (hy : y 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_1} {S : Type u_2} [comm_ring R] [comm_ring S] (y : R) [algebra R S] [is_localization.away 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_1} {S : Type u_2} [comm_ring R] [comm_ring S] (y : R) [algebra R S] [is_localization.away y S] [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.

If I is a prime ideal of polynomial R and pX ∈ I is a non-constant polynomial, then the map R →+* R[x]/I descends to an integral map when localizing at pX.leading_coeff. 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} [comm_ring S] [is_domain S] {R : Type u_1} [comm_ring R] [is_domain R] [ideal.is_jacobson R] (Rₘ : Type u_3) (Sₘ : Type u_4) [comm_ring Rₘ] [comm_ring Sₘ] (φ : R →+* S) (hφ : function.injective φ) (x : R) (hx : x 0) [algebra R Rₘ] [is_localization.away x Rₘ] [algebra S Sₘ] [is_localization (submonoid.map φ (submonoid.powers x)) Sₘ] (hφ' : (is_localization.map Sₘ φ _).is_integral) :

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

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

@[protected, instance]

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