Primitive ideals and the Jacobson radical

A primitive ideal is the annihilator of a nonzero simple left module. We define this using the quotients by maximal left ideals, so the predicate does not depend on a choice of universe for the simple module. The characterization by arbitrary simple modules follows from Mathlib's isSimpleModule_iff_quot_maximal.

The Jacobson radical is the intersection of the primitive ideals. Thus a ring has zero Jacobson radical exactly when its simple left modules separate its elements. No commutativity, norm or finiteness hypothesis is needed. In the commutative case, primitive ideals are exactly maximal ideals.

References

• Dales, Banach Algebras and Automatic Continuity, §§1.3–1.5.
• The simple-module realization uses isSimpleModule_iff_quot_maximal, and the radical inclusion uses IsSemisimpleModule.jacobson_le_annihilator.

def Ideal.IsPrimitive {R : Type u} [Ring R] (I : Ideal R) : Prop

A primitive ideal is the annihilator of the simple left module associated to a maximal left ideal. Equivalently, it is the annihilator of a simple left module in any universe; see isPrimitive_annihilator and IsPrimitive.exists_annihilator.

theorem Ideal.isPrimitive_iff_exists_isMaximal {R : Type u} [Ring R] (I : Ideal R) : I.IsPrimitive ↔ ∃ (J : Ideal R), J.IsMaximal ∧ Module.annihilator R (R ⧸ J) = I

Primitive ideals are exactly annihilators of quotients by maximal left ideals.

theorem Ideal.isPrimitive_annihilator {R : Type u} [Ring R] (M : Type v) [AddCommGroup M] [Module R M] [hM : IsSimpleModule R M] : (Module.annihilator R M).IsPrimitive

The annihilator of a simple left module is primitive. The module may live in any universe.

theorem Ideal.IsPrimitive.exists_annihilator {R : Type u} [Ring R] {I : Ideal R} (hI : I.IsPrimitive) : ∃ (M : Type u) (x : AddCommGroup M) (x_1 : Module R M), IsSimpleModule R M ∧ Module.annihilator R M = I

A primitive ideal has a simple-module realization in the universe of the ring.

theorem Ideal.IsPrimitive.isTwoSided {R : Type u} [Ring R] {I : Ideal R} (hI : I.IsPrimitive) : I.IsTwoSided

Primitive ideals are two-sided even when the ring is noncommutative.

theorem Ideal.IsPrimitive.ne_top {R : Type u} [Ring R] {I : Ideal R} (hI : I.IsPrimitive) : I ≠ ⊤

A primitive ideal is proper, because its realizing simple module is nonzero.

@[simp]

theorem Ideal.not_isPrimitive_top {R : Type u} [Ring R] : ¬⊤.IsPrimitive

The whole ring is never a primitive ideal.

theorem Ideal.IsPrimitive.jacobson_le {R : Type u} [Ring R] {I : Ideal R} (hI : I.IsPrimitive) : Ring.jacobson R ≤ I

Every primitive ideal contains the Jacobson radical.

theorem Ideal.IsPrimitive.mem_or_mem_of_forall_mul_mul_mem {R : Type u} [Ring R] {P : Ideal R} (hP : P.IsPrimitive) {a b : R} (h : ∀ (r : R), a * r * b ∈ P) : a ∈ P ∨ b ∈ P

Primitive ideals are prime. If a * r * b lies in a primitive ideal P for every r, then a ∈ P or b ∈ P.

theorem Ideal.IsPrimitive.inf_le_iff {R : Type u} [Ring R] {P : Ideal R} (hP : P.IsPrimitive) (I J : TwoSidedIdeal R) : TwoSidedIdeal.asIdeal (I ⊓ J) ≤ P ↔ TwoSidedIdeal.asIdeal I ≤ P ∨ TwoSidedIdeal.asIdeal J ≤ P

A primitive ideal containing the intersection of two two-sided ideals contains one of them. Two-sidedness is essential here; arbitrary left ideals do not satisfy this property.

@[simp]

theorem Ideal.isPrimitive_iff_isMaximal {S : Type u_1} [CommRing S] (I : Ideal S) : I.IsPrimitive ↔ I.IsMaximal

In a commutative ring, primitive ideals are exactly maximal ideals.

theorem TauCeti.Ring.jacobson_eq_sInf_isPrimitive (R : Type u) [Ring R] : Ring.jacobson R = sInf {I : Ideal R | I.IsPrimitive}

The Jacobson radical of a ring is the intersection of its primitive ideals.

theorem TauCeti.Ring.mem_jacobson_iff_forall_mem_isPrimitive (R : Type u) [Ring R] {a : R} : a ∈ Ring.jacobson R ↔ ∀ (I : Ideal R), I.IsPrimitive → a ∈ I

An element is in the radical exactly when it belongs to every primitive ideal.

theorem TauCeti.Ring.jacobson_eq_bot_iff_forall_ne_zero_exists_isPrimitive_notMem (R : Type u) [Ring R] : Ring.jacobson R = ⊥ ↔ ∀ (a : R), a ≠ 0 → ∃ (I : Ideal R), I.IsPrimitive ∧ a ∉ I

Zero Jacobson radical means that primitive ideals separate nonzero elements.