A Prime-Generated Formalization of Nagata's Factoriality Theorem in Lean 4
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2026
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866915919518760960 |
|---|---|
| author | Ramos, Arthur F. de Queiroz, Ruy J. G. B. de Oliveira, Anjolina G. |
| author_facet | Ramos, Arthur F. de Queiroz, Ruy J. G. B. de Oliveira, Anjolina G. |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2604_05238 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | A Prime-Generated Formalization of Nagata's Factoriality Theorem in Lean 4 Ramos, Arthur F. de Queiroz, Ruy J. G. B. de Oliveira, Anjolina G. Commutative Algebra Logic in Computer Science 03B35, 13A05, 13B30 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. |
| title | A Prime-Generated Formalization of Nagata's Factoriality Theorem in Lean 4 |
| topic | Commutative Algebra Logic in Computer Science 03B35, 13A05, 13B30 |
| url | https://arxiv.org/abs/2604.05238 |