Import Nagata's prime-generated factoriality theorem

LeanPool.lean

@@ -4828,6 +4828,26 @@ public import LeanPool.MoserLatticeColorings
 public import LeanPool.MoserLatticeColorings.Basic
 public import LeanPool.MoserLatticeColorings.Ring
 public import LeanPool.MulticolorTriangleRamsey
+public import LeanPool.NagataFactoriality
+public import LeanPool.NagataFactoriality.NagataFactoriality
+public import LeanPool.NagataFactoriality.NagataFactoriality.Applications
+public import LeanPool.NagataFactoriality.NagataFactoriality.Applications.Examples
+public import LeanPool.NagataFactoriality.NagataFactoriality.Applications.FractionField
+public import LeanPool.NagataFactoriality.NagataFactoriality.Applications.Gauss
+public import LeanPool.NagataFactoriality.NagataFactoriality.Applications.Laurent
+public import LeanPool.NagataFactoriality.NagataFactoriality.Basic
+public import LeanPool.NagataFactoriality.NagataFactoriality.Basic.Divisibility
+public import LeanPool.NagataFactoriality.NagataFactoriality.Basic.Noetherian
+public import LeanPool.NagataFactoriality.NagataFactoriality.Basic.Ring
+public import LeanPool.NagataFactoriality.NagataFactoriality.Basic.UFD
+public import LeanPool.NagataFactoriality.NagataFactoriality.Localization
+public import LeanPool.NagataFactoriality.NagataFactoriality.Localization.IsLocalization
+public import LeanPool.NagataFactoriality.NagataFactoriality.Localization.Localization
+public import LeanPool.NagataFactoriality.NagataFactoriality.Localization.MultSet
+public import LeanPool.NagataFactoriality.NagataFactoriality.Localization.Properties
+public import LeanPool.NagataFactoriality.NagataFactoriality.Nagata
+public import LeanPool.NagataFactoriality.NagataFactoriality.Nagata.Lemmas
+public import LeanPool.NagataFactoriality.NagataFactoriality.Nagata.Theorem
 public import LeanPool.NashWilliams
 public import LeanPool.NashWilliams.Combinatorics
 public import LeanPool.NashWilliams.Combinatorics.Front

LeanPool/NagataFactoriality.lean

@@ -0,0 +1,41 @@
+/-
+Copyright (c) 2026 the authors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina G. de Oliveira
+-/
+
+module
+
+public import LeanPool.NagataFactoriality.NagataFactoriality
+public import LeanPool.NagataFactoriality.NagataFactoriality.Applications
+public import LeanPool.NagataFactoriality.NagataFactoriality.Applications.Examples
+public import LeanPool.NagataFactoriality.NagataFactoriality.Applications.FractionField
+public import LeanPool.NagataFactoriality.NagataFactoriality.Applications.Gauss
+public import LeanPool.NagataFactoriality.NagataFactoriality.Applications.Laurent
+public import LeanPool.NagataFactoriality.NagataFactoriality.Basic
+public import LeanPool.NagataFactoriality.NagataFactoriality.Basic.Divisibility
+public import LeanPool.NagataFactoriality.NagataFactoriality.Basic.Noetherian
+public import LeanPool.NagataFactoriality.NagataFactoriality.Basic.Ring
+public import LeanPool.NagataFactoriality.NagataFactoriality.Basic.UFD
+public import LeanPool.NagataFactoriality.NagataFactoriality.Localization
+public import LeanPool.NagataFactoriality.NagataFactoriality.Localization.IsLocalization
+public import LeanPool.NagataFactoriality.NagataFactoriality.Localization.Localization
+public import LeanPool.NagataFactoriality.NagataFactoriality.Localization.MultSet
+public import LeanPool.NagataFactoriality.NagataFactoriality.Localization.Properties
+public import LeanPool.NagataFactoriality.NagataFactoriality.Nagata
+public import LeanPool.NagataFactoriality.NagataFactoriality.Nagata.Lemmas
+public import LeanPool.NagataFactoriality.NagataFactoriality.Nagata.Theorem
+
+
+/-!
+# Nagata's prime-generated factoriality theorem
+
+Source: url:https://github.com/arthur742ramos/nagatafactoriality
+Authors: Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina G. de Oliveira
+Status: verified
+Main declarations: `NagataFactoriality.nagata_theorem`
+Tags: commutative-algebra
+MSC: 13F15
+-/
+
+@[expose] public section

LeanPool/NagataFactoriality/NagataFactoriality.lean

@@ -0,0 +1,20 @@
+/-
+Copyright (c) 2026 the authors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina G. de Oliveira
+-/
+module
+
+public import LeanPool.NagataFactoriality.NagataFactoriality.Basic
+public import LeanPool.NagataFactoriality.NagataFactoriality.Localization
+public import LeanPool.NagataFactoriality.NagataFactoriality.Nagata
+public import LeanPool.NagataFactoriality.NagataFactoriality.Applications
+
+
+/-!
+# NagataFactoriality
+
+Supporting results for Nagata’s factoriality theorem.
+-/
+
+@[expose] public section

LeanPool/NagataFactoriality/NagataFactoriality/Applications.lean

@@ -0,0 +1,20 @@
+/-
+Copyright (c) 2026 the authors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina G. de Oliveira
+-/
+module
+
+public import LeanPool.NagataFactoriality.NagataFactoriality.Applications.Gauss
+public import LeanPool.NagataFactoriality.NagataFactoriality.Applications.Laurent
+public import LeanPool.NagataFactoriality.NagataFactoriality.Applications.FractionField
+public import LeanPool.NagataFactoriality.NagataFactoriality.Applications.Examples
+
+
+/-!
+# Applications
+
+Supporting results for Nagata’s factoriality theorem.
+-/
+
+@[expose] public section

LeanPool/NagataFactoriality/NagataFactoriality/Applications/Examples.lean

@@ -0,0 +1,39 @@
+/-
+Copyright (c) 2026 the authors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina G. de Oliveira
+-/
+module
+
+public import Mathlib.Algebra.EuclideanDomain.Int
+public import Mathlib.RingTheory.PrincipalIdealDomain
+public import Mathlib.RingTheory.Polynomial.UniqueFactorization
+
+
+/-!
+# Examples
+
+Supporting results for Nagata’s factoriality theorem.
+-/
+
+@[expose] public section
+
+namespace NagataFactoriality
+
+open Polynomial
+
+theorem int_uniqueFactorizationMonoid : UniqueFactorizationMonoid ℤ := by
+  infer_instance
+
+theorem int_polynomial_uniqueFactorizationMonoid : UniqueFactorizationMonoid ℤ[X] := by
+  infer_instance
+
+theorem mvPolynomial_uniqueFactorizationMonoid (n : ℕ) (k : Type*) [Field k] :
+    UniqueFactorizationMonoid (MvPolynomial (Fin n) k) := by
+  infer_instance
+
+theorem iterated_polynomial_uniqueFactorizationMonoid (k : Type*) [Field k] :
+    UniqueFactorizationMonoid (Polynomial (Polynomial k)) := by
+  infer_instance
+
+end NagataFactoriality

LeanPool/NagataFactoriality/NagataFactoriality/Applications/FractionField.lean

@@ -0,0 +1,157 @@
+/-
+Copyright (c) 2026 the authors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina G. de Oliveira
+-/
+module
+
+public import Mathlib.RingTheory.Localization.Algebra
+public import Mathlib.RingTheory.Localization.FractionRing
+public import Mathlib.RingTheory.Polynomial.Basic
+public import Mathlib.RingTheory.Polynomial.UniqueFactorization
+public import LeanPool.NagataFactoriality.NagataFactoriality.Nagata.Theorem
+
+
+/-!
+# Polynomial UFD via Fraction Field Localization and Nagata's Theorem
+
+This file provides an alternative Nagata-based proof that if `R` is a noetherian UFD,
+then `R[X]` is a UFD, by localizing `R[X]` at the multiplicative submonoid generated
+by the constant primes and identifying the localization with `Frac(R)[X]`.
+
+This is structurally different from the Laurent polynomial route in
+`NagataFactoriality.Applications.Laurent`, which localizes at `X` and identifies
+with `R[T;T⁻¹]`.
+
+## Strategy
+
+1. The submonoid `S` of `R[X]` generated by `{C(p) | p prime in R}` is `PrimeGenerated`.
+2. The localization of `R[X]` at `S` can be identified with `Frac(R)[X]`:
+   - The larger submonoid `(R⁰).map C` gives `IsLocalization` for `Frac(R)[X]`
+     via `Polynomial.isLocalization`.
+   - Since every nonzero element of `R` factors into primes (UFD), the localization
+     at the smaller prime-generated submonoid `S` agrees with the localization at
+     `(R⁰).map C`.
+3. Since `Frac(R)` is a field, `Frac(R)[X]` is a Euclidean domain, hence a UFD.
+4. Nagata's theorem then gives `UniqueFactorizationMonoid R[X]`.
+
+## Main results
+
+* `polynomial_uniqueFactorizationMonoid_via_fractionField`: If `R` is a noetherian UFD,
+  then `R[X]` is a UFD, proved by localizing at constant primes and using Nagata's theorem.
+-/
+
+@[expose] public section
+
+noncomputable section
+
+namespace NagataFactoriality
+
+open Polynomial
+
+section FractionFieldRoute
+
+variable (R : Type*) [CommRing R] [IsDomain R] [UniqueFactorizationMonoid R]
+
+/-- The submonoid of `R[X]` generated by constant primes `{C(p) | p prime in R}`. -/
+private abbrev constPrimeSubmonoid : Submonoid R[X] :=
+  Submonoid.closure (C '' {r : R | Prime r})
+
+omit [IsDomain R] [UniqueFactorizationMonoid R] in
+private theorem constPrimeSubmonoid_primeGenerated :
+    PrimeGenerated (constPrimeSubmonoid R) :=
+  primeGenerated_closure_of_primes (fun _ ⟨_, hr, hrq⟩ => hrq ▸ Polynomial.prime_C_iff.mpr hr)
+
+/-- The image of `R⁰` (nonzero divisors) under `C : R → R[X]`. In a domain this is
+    the submonoid of nonzero constant polynomials. -/
+private abbrev nzdMapC : Submonoid R[X] :=
+  (nonZeroDivisors R).map (C : R →+* R[X])
+
+omit [UniqueFactorizationMonoid R] in
+private theorem constPrimeSubmonoid_le_nzdMapC :
+    constPrimeSubmonoid R ≤ nzdMapC R := by
+  apply Submonoid.closure_le.mpr
+  intro x hx
+  rcases hx with ⟨r, hr, rfl⟩
+  have hr' : Prime r := by simpa using hr
+  exact Submonoid.mem_map.2 ⟨r, mem_nonZeroDivisors_iff_ne_zero.mpr hr'.ne_zero, rfl⟩
+
+variable {R}
+
+omit [IsDomain R] in
+/-- In a UFD, `C(r)` for nonzero `r` maps to a unit in the localization at constant primes,
+because `r` factors into primes and each constant prime becomes invertible. -/
+private theorem isUnit_algebraMap_C_of_ne_zero (r : R) (hr : r ≠ 0) :
+    IsUnit (algebraMap R[X] (_root_.Localization (constPrimeSubmonoid R)) (C r)) := by
+  obtain ⟨f, hf_prime, hf_assoc⟩ := UniqueFactorizationMonoid.exists_prime_factors r hr
+  -- Associated (C f.prod) (C r) in R[X], mapping through algebraMap preserves this
+  have hassocC := (hf_assoc.map (C : R →+* R[X])).map
+    (algebraMap R[X] (_root_.Localization (constPrimeSubmonoid R)))
+  -- C f.prod ∈ constPrimeSubmonoid, hence maps to a unit
+  have hmem : C f.prod ∈ constPrimeSubmonoid R := by
+    have : C f.prod = (f.map C).prod := by
+      rw [Multiset.prod_hom]
+    rw [this]
+    exact multiset_prod_mem_of_factors (fun q hq => by
+      obtain ⟨p, hp, rfl⟩ := Multiset.mem_map.mp hq
+      exact Submonoid.subset_closure ⟨p, hf_prime p hp, rfl⟩)
+  exact hassocC.isUnit_iff.mp (IsLocalization.map_units _ ⟨_, hmem⟩)
+
+variable (R)
+
+/-- The localization of `R[X]` at the constant prime submonoid is also a localization
+at the (larger) image of all nonzero elements, because in a UFD every nonzero element
+factors into primes and units. -/
+private theorem isLocalization_nzdMapC_localization :
+    IsLocalization (nzdMapC R) (_root_.Localization (constPrimeSubmonoid R)) where
+  map_units := by
+    intro ⟨t, ht⟩
+    obtain ⟨r, hr, rfl⟩ := ht
+    exact isUnit_algebraMap_C_of_ne_zero r (mem_nonZeroDivisors_iff_ne_zero.mp hr)
+  surj := by
+    intro z
+    obtain ⟨⟨a, s⟩, hz⟩ := _root_.IsLocalization.surj (M := constPrimeSubmonoid R) z
+    exact ⟨⟨a, ⟨s, constPrimeSubmonoid_le_nzdMapC R s.2⟩⟩, hz⟩
+  exists_of_eq := by
+    intro x y hxy
+    obtain ⟨⟨c, hc⟩, hcxy⟩ := _root_.IsLocalization.exists_of_eq (M := constPrimeSubmonoid R) hxy
+    exact ⟨⟨c, constPrimeSubmonoid_le_nzdMapC R hc⟩, hcxy⟩
+
+/-- If `R` is a noetherian UFD, then `R[X]` is a UFD.
+
+This is proved by localizing `R[X]` at the multiplicative submonoid generated by
+the constant primes `{C(p) | p prime in R}` and showing the localization is isomorphic
+to `Frac(R)[X]`, which is a UFD since `Frac(R)` is a field.
+
+Nagata's theorem then recovers `UniqueFactorizationMonoid R[X]`.
+
+This route is structurally distinct from the Laurent polynomial route
+(`polynomial_uniqueFactorizationMonoid_via_nagata` in `Applications.Laurent`),
+which localizes at `X` and identifies with `R[T;T⁻¹]`. -/
+theorem polynomial_uniqueFactorizationMonoid_via_fractionField
+    [IsNoetherianRing R] : UniqueFactorizationMonoid R[X] := by
+  let S := constPrimeSubmonoid R
+  have hS : PrimeGenerated S := constPrimeSubmonoid_primeGenerated R
+  let : Fact ((0 : R[X]) ∉ S) := ⟨zero_notMem_of_primeGenerated hS⟩
+  -- Set up the algebra structure on (FractionRing R)[X] over R[X]
+  let : Algebra R[X] (FractionRing R)[X] :=
+    (Polynomial.mapRingHom (algebraMap R (FractionRing R))).toAlgebra
+  -- (FractionRing R)[X] is a localization of R[X] at nzdMapC
+  let : IsLocalization (nzdMapC R) (FractionRing R)[X] :=
+    Polynomial.isLocalization (nonZeroDivisors R) (FractionRing R)
+  -- The localization at constPrimeSubmonoid is also a localization at nzdMapC
+  let : IsLocalization (nzdMapC R) (_root_.Localization S) :=
+    isLocalization_nzdMapC_localization R
+  -- Build the algebra equivalence between (FractionRing R)[X] and Localization S
+  let e := IsLocalization.algEquiv (nzdMapC R)
+    (Polynomial (FractionRing R)) (_root_.Localization S)
+  -- (FractionRing R)[X] is a UFD: FractionRing R is a field, hence a UFD
+  have : UniqueFactorizationMonoid (FractionRing R)[X] := inferInstance
+  -- Transfer UFD across the algebra equivalence
+  have hUFDLoc : UniqueFactorizationMonoid (_root_.Localization S) :=
+    MulEquiv.uniqueFactorizationMonoid e.toMulEquiv inferInstance
+  exact nagata_theorem (R := R[X]) S hS hUFDLoc
+
+end FractionFieldRoute
+
+end NagataFactoriality

LeanPool/NagataFactoriality/NagataFactoriality/Applications/Gauss.lean

@@ -0,0 +1,37 @@
+/-
+Copyright (c) 2026 the authors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina G. de Oliveira
+-/
+module
+
+public import Mathlib.RingTheory.Polynomial.Content
+public import Mathlib.RingTheory.Polynomial.GaussLemma
+public import Mathlib.RingTheory.Polynomial.UniqueFactorization
+
+
+/-!
+# Gauss
+
+Supporting results for Nagata’s factoriality theorem.
+-/
+
+@[expose] public section
+
+namespace NagataFactoriality
+
+open Polynomial
+
+theorem polynomial_content_mul {R : Type*} [CommRing R] [StrongNormalizedGCDMonoid R]
+    (p q : R[X]) : (p * q).content = p.content * q.content :=
+  Polynomial.content_mul
+
+theorem primitive_mul {R : Type*} [CommRing R] [NormalizedGCDMonoid R]
+    {p q : R[X]} (hp : p.IsPrimitive) (hq : q.IsPrimitive) : (p * q).IsPrimitive :=
+  hp.mul hq
+
+theorem polynomial_uniqueFactorizationMonoid {R : Type*} [CommRing R]
+    [UniqueFactorizationMonoid R] : UniqueFactorizationMonoid R[X] := by
+  infer_instance
+
+end NagataFactoriality