A Prime-Generated Formalization of Nagata's Factoriality Theorem in Lean 4

TL;DR

This paper formalizes Nagata's factoriality theorem in Lean 4, showing that certain localizations of a noetherian domain imply it is a UFD, and applies this to polynomial rings.

Contribution

First formalization of Nagata's factoriality theorem in Lean 4, including applications to polynomial rings and multiple localization techniques.

Findings

Formalization of Nagata's theorem in Lean 4.

Proof that R[X] is a UFD if R is a noetherian UFD.

Implementation of two localization-based proofs for polynomial rings.

Abstract

We present a Lean 4 Mathlib formalization of Nagata's factoriality theorem: if R is a noetherian domain and S <= R is a prime-generated submonoid such that S^{-1}R is a UFD, then R itself is a UFD. The prime-generated hypothesis -- every element of S is a finite product of primes belonging to S -- replaces a superficially cleaner but degenerate prime-or-unit condition that the formalization effort exposed. The development packages the theorem both for the concrete type Localization S and through abstract IsLocalization formulations. As applications, we formalize two Nagata-based proofs that R[X] is a UFD whenever R is a noetherian UFD: one via Laurent-polynomial localization at powers of X, and one via localization at the constant primes and identification with Frac(R)[X]. Reusing the same package, we also obtain the iterated polynomial corollary R[X][Y]. No public formalization of this result is known to us in Lean, Coq, or Isabelle.