Jacobson rings via principal quotients

A commutative ring is a Jacobson ring as soon as its Jacobson radical vanishes and its quotient by every nonzero principal ideal is a Jacobson ring. Indeed, every nonzero prime ideal contains a nonzero element, and so is the preimage of a prime ideal of such a quotient.

This is the shape of the Jacobson criterion of Bosch–Güntzer–Remmert for rings with a Weierstrass theory: Weierstrass division makes the quotient by a nonzero element finite over a smaller ring, so that isJacobsonRing_of_isIntegral applies to it, while the vanishing of the Jacobson radical is checked separately.

References

• [Bosch, Güntzer, Remmert, Non-Archimedean Analysis][bosch-guntzer-remmert], §§5.2.5–5.2.6.

theorem TauCeti.isJacobsonRing_of_quotient_span_singleton {R : Type u_1} [CommRing R] (hR : ⊥.jacobson = ⊥) (h : ∀ (x : R), x ≠ 0 → IsJacobsonRing (R ⧸ Ideal.span {x})) : IsJacobsonRing R

Jacobson rings via principal quotients. A commutative ring whose Jacobson radical is zero, and whose quotient by every nonzero principal ideal is a Jacobson ring, is a Jacobson ring.