Lifting principal primes from a quotient by a radical element

Let x be an element of the Jacobson radical of R and 𝔮 a finitely generated prime not containing x. Since 𝔮 is prime and x ∉ 𝔮, the kernel 𝔮 ∩ (x) of 𝔮 → R ⧸ (x) is x 𝔮. If the image of 𝔮 is principal, generated by the image of some f ∈ 𝔮, then 𝔮 = (f) + x 𝔮 and Nakayama's lemma gives 𝔮 = (f).

Main results

• Ideal.IsPrime.isPrincipal_of_isPrincipal_map_quotient_span_singleton: a finitely generated prime 𝔮 not containing an element x of the Jacobson radical is principal as soon as its image in R ⧸ (x) is.

theorem Ideal.IsPrime.isPrincipal_of_isPrincipal_map_quotient_span_singleton {R : Type u_1} [CommRing R] {q : Ideal R} (hq : q.IsPrime) (hfg : q.FG) {x : R} (hx : x ∈ ⊥.jacobson) (hxq : x ∉ q) (h : Submodule.IsPrincipal (map (Quotient.mk (span {x})) q)) : Submodule.IsPrincipal q

A prime is principal if its image modulo a radical element is. Let x be an element of the Jacobson radical of R and 𝔮 a finitely generated prime ideal not containing x. If the image of 𝔮 in R ⧸ (x) is principal, then 𝔮 is principal.