Nagata's criterion

Let R be an integral domain satisfying ACC on divisibility, and let p be a prime element such that R[p^{-1}] is a UFD. Then R is a UFD. The proof uses Kaplansky's theorem: every nonzero prime ideal of R contains a prime element, obtained by lifting a prime from the localisation and cancelling powers of p.

theorem nagata_powers_le_nonZeroDivisors {R₀ : Type u_1} [CommRing R₀] [IsDomain R₀] (p : R₀) (hp : Prime p) : Submonoid.powers p ≤ nonZeroDivisors R₀

theorem nagata_algebraMap_injective {R₀ : Type u_1} [CommRing R₀] [IsDomain R₀] (p : R₀) (hp : Prime p) : Function.Injective ⇑(algebraMap R₀ (Localization.Away p))

theorem dvd_of_dvd_mul_prime_pow {R₀ : Type u_1} [CommRing R₀] [IsDomain R₀] {p q a : R₀} (hp : Prime p) (hpq : ¬p ∣ q) (n : ℕ) : q ∣ a * p ^ n → q ∣ a

Key cancellation lemma: if p is prime, p ∤ q, and q ∣ a * p ^ n, then q ∣ a. We peel off factors of p one at a time.

theorem prime_of_image_prime {R₀ : Type u_1} [CommRing R₀] [IsDomain R₀] (p : R₀) (hp : Prime p) (q : R₀) (hpq : ¬p ∣ q) (hq_loc : Prime ((algebraMap R₀ (Localization.Away p)) q)) : Prime q

If q ∈ R₀ has prime image in Localization.Away p and p ∤ q, then q is prime in R₀.

theorem nagata_criterion {R₀ : Type u_1} [CommRing R₀] [IsDomain R₀] [WfDvdMonoid R₀] (p : R₀) (hp : Prime p) (hUFD_loc : UniqueFactorizationMonoid (Localization.Away p)) : UniqueFactorizationMonoid R₀

Nagata's criterion: if p is prime in R and R[p⁻¹] is a UFD, then R is a UFD. This is the converse direction of localization preserving UFDs: if inverting one prime element yields a UFD, the original ring was already a UFD.