Closedness of primitive ideals #
Primitive ideals of a normed ring with summable geometric series are closed. In particular this applies to unital Banach algebras, without commutativity or a normalization of the identity's norm. Together with the primitive-ideal description of the radical, this realizes the radical as an intersection of closed two-sided ideals.
The annihilator of the quotient by a maximal left ideal J consists of those
a for which every right multiple a * x lies in J. Mathlib's
Submodule.annihilator_quotient identifies this with a colon ideal, and
Ideal.IsMaximal.isClosed gives the closedness of J.
References #
- Dales, Banach Algebras and Automatic Continuity, §§1.3–1.5.
theorem
Ideal.IsPrimitive.isClosed
{R : Type u_1}
[NormedRing R]
[HasSummableGeomSeries R]
{I : Ideal R}
(hI : I.IsPrimitive)
:
IsClosed ↑I
Primitive ideals in a normed ring with summable geometric series are closed. In particular, primitive ideals of a unital Banach algebra are closed.