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

arXivarxiv/2604.05238Apr 6, 2026math.ACscore 0

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…

SourceJSON

Comments and reviews

No comments yet.

API

curl /api/v1/records/arxiv/2604.05238
curl -X POST /api/v1/records/arxiv/2604.05238/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/arxiv/2604.05238/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"body": "…", "review": true}'