A Prime-Generated Formalization of Nagata's Factoriality Theorem in Lean 4
Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina G. de Oliveira
math.AC
Apr 6, 2026 · v1
TL;DR
Lean 4 + Mathlib formalization of Nagata's factoriality theorem.
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.
Problem
Nagata's factoriality theorem (if R is a noetherian domain and S is a prime-generated submonoid such that the localization is a UFD, then R is a UFD) lacked a machine-checked formalization. A subtlety around the prime-generated hypothesis versus a degenerate prime-or-unit condition had not been formally resolved.
Approach
The paper presents a Lean 4 Mathlib formalization of Nagata's theorem using the prime-generated hypothesis, where every element of S factors as a finite product of primes belonging to S. The development packages the theorem for both the concrete type Localization S and through abstract IsLocalization formulations. The formalization process exposed that a superficially cleaner prime-or-unit condition is degenerate.
Results
The formalization is complete and contributed to Mathlib. As applications, two Nagata-based proofs that polynomial rings R[X] over UFDs are UFDs are formalized: one via the classical Gauss lemma route and one via localization at the set of leading coefficients.
