Factoriality from a principal ideal domain quotient

Let R be a Noetherian domain and x an element of its Jacobson radical such that R ⧸ (x) is a principal ideal domain. Then R is a unique factorization domain: every nonzero prime 𝔮 contains a prime element, namely x if x ∈ 𝔮, and otherwise a generator of 𝔮, which is principal by Ideal.IsPrime.isPrincipal_of_isPrincipal_map_quotient_span_singleton. Kaplansky's criterion concludes.

Main results

• UniqueFactorizationMonoid.of_isPrincipalIdealRing_quotient_span_singleton: a Noetherian domain with an element x of its Jacobson radical such that R ⧸ (x) is a principal ideal domain is a unique factorization domain.

References

• I. Kaplansky, Commutative Rings, for the criterion by prime elements in prime ideals, which is Mathlib's UniqueFactorizationMonoid.iff_exists_prime_mem_of_isPrime.

theorem UniqueFactorizationMonoid.of_isPrincipalIdealRing_quotient_span_singleton {R : Type u_1} [CommRing R] [IsDomain R] [IsNoetherianRing R] {x : R} (hx : x ∈ ⊥.jacobson) [IsDomain (R ⧸ Ideal.span {x})] [IsPrincipalIdealRing (R ⧸ Ideal.span {x})] : UniqueFactorizationMonoid R

A domain is factorial if it is a principal ideal domain modulo a radical element. Let R be a Noetherian domain and x an element of its Jacobson radical such that R ⧸ (x) is a principal ideal domain. Then R is a unique factorization domain.