Email Gateway (Apr 30 2026 at 18:07): Email Gateway (Apr 30 2026 at 18:07):From: Lawrence Paulson <lp15@cam.ac.uk>
I’m happy to announce a new contribution: Nagata Factoriality, by Arthur Freitas Ramos , David Barros Hulak and Ruy Jose Guerra Barretto de Queiroz.
Abstract
This entry formalizes a prime-generated version of Nagata's factoriality theorem in Isabelle/HOL. It develops the basic theory of prime-generated multiplicative sets, packages a wrapper interface around the AFP entry Localization_Ring, and proves record-based descent theorems showing that factoriality descends from a localization to the base ring under prime-generated and prime-or-unit hypotheses on the multiplicative set. The theorem package also includes closure-based corollaries for arbitrary and finite families of prime generators. The application layer specializes this framework to polynomial rings, both for localization away the polynomial variable X and for localizations generated by constant prime polynomials.
https://www.isa-afp.org/entries/Nagata-Factoriality.html
Last updated: May 02 2026 at 13:17 UTC