From 00e156d67ee7936484ff2a231beb7f3b5f6d1c36 Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Mon, 21 Sep 2026 18:02:21 +0000 Subject: [PATCH 1/8] Import complete nagatafactoriality proof development --- LeanPool.lean | 1 + LeanPool/NagataFactoriality.lean | 36 + .../NagataFactoriality.lean | 9 + .../NagataFactoriality/Applications.lean | 9 + .../Applications/Examples.lean | 28 + .../Applications/FractionField.lean | 149 ++++ .../Applications/Gauss.lean | 26 + .../Applications/Laurent.lean | 114 +++ .../NagataFactoriality/Basic.lean | 9 + .../Basic/Divisibility.lean | 81 +++ .../NagataFactoriality/Basic/Noetherian.lean | 20 + .../NagataFactoriality/Basic/Ring.lean | 10 + .../NagataFactoriality/Basic/UFD.lean | 69 ++ .../NagataFactoriality/Localization.lean | 9 + .../Localization/IsLocalization.lean | 120 ++++ .../Localization/Localization.lean | 182 +++++ .../Localization/MultSet.lean | 35 + .../Localization/Properties.lean | 7 + .../NagataFactoriality/Nagata.lean | 7 + .../NagataFactoriality/Nagata/Lemmas.lean | 656 ++++++++++++++++++ .../NagataFactoriality/Nagata/Theorem.lean | 105 +++ LeanPool/projects.yml | 27 + 22 files changed, 1709 insertions(+) create mode 100644 LeanPool/NagataFactoriality.lean create mode 100644 LeanPool/NagataFactoriality/NagataFactoriality.lean create mode 100644 LeanPool/NagataFactoriality/NagataFactoriality/Applications.lean create mode 100644 LeanPool/NagataFactoriality/NagataFactoriality/Applications/Examples.lean create mode 100644 LeanPool/NagataFactoriality/NagataFactoriality/Applications/FractionField.lean create mode 100644 LeanPool/NagataFactoriality/NagataFactoriality/Applications/Gauss.lean create mode 100644 LeanPool/NagataFactoriality/NagataFactoriality/Applications/Laurent.lean create mode 100644 LeanPool/NagataFactoriality/NagataFactoriality/Basic.lean create mode 100644 LeanPool/NagataFactoriality/NagataFactoriality/Basic/Divisibility.lean create mode 100644 LeanPool/NagataFactoriality/NagataFactoriality/Basic/Noetherian.lean create mode 100644 LeanPool/NagataFactoriality/NagataFactoriality/Basic/Ring.lean create mode 100644 LeanPool/NagataFactoriality/NagataFactoriality/Basic/UFD.lean create mode 100644 LeanPool/NagataFactoriality/NagataFactoriality/Localization.lean create mode 100644 LeanPool/NagataFactoriality/NagataFactoriality/Localization/IsLocalization.lean create mode 100644 LeanPool/NagataFactoriality/NagataFactoriality/Localization/Localization.lean create mode 100644 LeanPool/NagataFactoriality/NagataFactoriality/Localization/MultSet.lean create mode 100644 LeanPool/NagataFactoriality/NagataFactoriality/Localization/Properties.lean create mode 100644 LeanPool/NagataFactoriality/NagataFactoriality/Nagata.lean create mode 100644 LeanPool/NagataFactoriality/NagataFactoriality/Nagata/Lemmas.lean create mode 100644 LeanPool/NagataFactoriality/NagataFactoriality/Nagata/Theorem.lean diff --git a/LeanPool.lean b/LeanPool.lean index 50fa6e5b30..aaa4dc75ac 100644 --- a/LeanPool.lean +++ b/LeanPool.lean @@ -3840,6 +3840,7 @@ import LeanPool.MoserLatticeColorings import LeanPool.MoserLatticeColorings.Basic import LeanPool.MoserLatticeColorings.Ring import LeanPool.MulticolorTriangleRamsey +import LeanPool.NagataFactoriality import LeanPool.NashWilliams import LeanPool.NashWilliams.Combinatorics import LeanPool.NashWilliams.Combinatorics.Front diff --git a/LeanPool/NagataFactoriality.lean b/LeanPool/NagataFactoriality.lean new file mode 100644 index 0000000000..a772ae3ab3 --- /dev/null +++ b/LeanPool/NagataFactoriality.lean @@ -0,0 +1,36 @@ +/- +Copyright (c) 2026 Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina G. de Oliveira. 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 +-/ + +import LeanPool.NagataFactoriality.NagataFactoriality +import LeanPool.NagataFactoriality.NagataFactoriality.Applications +import LeanPool.NagataFactoriality.NagataFactoriality.Applications.Examples +import LeanPool.NagataFactoriality.NagataFactoriality.Applications.FractionField +import LeanPool.NagataFactoriality.NagataFactoriality.Applications.Gauss +import LeanPool.NagataFactoriality.NagataFactoriality.Applications.Laurent +import LeanPool.NagataFactoriality.NagataFactoriality.Basic +import LeanPool.NagataFactoriality.NagataFactoriality.Basic.Divisibility +import LeanPool.NagataFactoriality.NagataFactoriality.Basic.Noetherian +import LeanPool.NagataFactoriality.NagataFactoriality.Basic.Ring +import LeanPool.NagataFactoriality.NagataFactoriality.Basic.UFD +import LeanPool.NagataFactoriality.NagataFactoriality.Localization +import LeanPool.NagataFactoriality.NagataFactoriality.Localization.IsLocalization +import LeanPool.NagataFactoriality.NagataFactoriality.Localization.Localization +import LeanPool.NagataFactoriality.NagataFactoriality.Localization.MultSet +import LeanPool.NagataFactoriality.NagataFactoriality.Localization.Properties +import LeanPool.NagataFactoriality.NagataFactoriality.Nagata +import LeanPool.NagataFactoriality.NagataFactoriality.Nagata.Lemmas +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 +-/ diff --git a/LeanPool/NagataFactoriality/NagataFactoriality.lean b/LeanPool/NagataFactoriality/NagataFactoriality.lean new file mode 100644 index 0000000000..226c0d665f --- /dev/null +++ b/LeanPool/NagataFactoriality/NagataFactoriality.lean @@ -0,0 +1,9 @@ +/- +Copyright (c) 2026 Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina G. de Oliveira. 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 +-/ +import LeanPool.NagataFactoriality.NagataFactoriality.Basic +import LeanPool.NagataFactoriality.NagataFactoriality.Localization +import LeanPool.NagataFactoriality.NagataFactoriality.Nagata +import LeanPool.NagataFactoriality.NagataFactoriality.Applications diff --git a/LeanPool/NagataFactoriality/NagataFactoriality/Applications.lean b/LeanPool/NagataFactoriality/NagataFactoriality/Applications.lean new file mode 100644 index 0000000000..0a040f6024 --- /dev/null +++ b/LeanPool/NagataFactoriality/NagataFactoriality/Applications.lean @@ -0,0 +1,9 @@ +/- +Copyright (c) 2026 Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina G. de Oliveira. 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 +-/ +import LeanPool.NagataFactoriality.NagataFactoriality.Applications.Gauss +import LeanPool.NagataFactoriality.NagataFactoriality.Applications.Laurent +import LeanPool.NagataFactoriality.NagataFactoriality.Applications.FractionField +import LeanPool.NagataFactoriality.NagataFactoriality.Applications.Examples diff --git a/LeanPool/NagataFactoriality/NagataFactoriality/Applications/Examples.lean b/LeanPool/NagataFactoriality/NagataFactoriality/Applications/Examples.lean new file mode 100644 index 0000000000..1b9b09afec --- /dev/null +++ b/LeanPool/NagataFactoriality/NagataFactoriality/Applications/Examples.lean @@ -0,0 +1,28 @@ +/- +Copyright (c) 2026 Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina G. de Oliveira. 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 +-/ +import Mathlib.Algebra.EuclideanDomain.Int +import Mathlib.RingTheory.PrincipalIdealDomain +import Mathlib.RingTheory.Polynomial.UniqueFactorization + +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 diff --git a/LeanPool/NagataFactoriality/NagataFactoriality/Applications/FractionField.lean b/LeanPool/NagataFactoriality/NagataFactoriality/Applications/FractionField.lean new file mode 100644 index 0000000000..b83addf2e4 --- /dev/null +++ b/LeanPool/NagataFactoriality/NagataFactoriality/Applications/FractionField.lean @@ -0,0 +1,149 @@ +/- +Copyright (c) 2026 Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina G. de Oliveira. 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 +-/ +import Mathlib.RingTheory.Localization.Algebra +import Mathlib.RingTheory.Localization.FractionRing +import Mathlib.RingTheory.Polynomial.Basic +import Mathlib.RingTheory.Polynomial.UniqueFactorization +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. +-/ + +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} + +/-- 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 + letI : Fact ((0 : R[X]) ∉ S) := ⟨zero_notMem_of_primeGenerated hS⟩ + -- Set up the algebra structure on (FractionRing R)[X] over R[X] + letI : Algebra R[X] (FractionRing R)[X] := + (Polynomial.mapRingHom (algebraMap R (FractionRing R))).toAlgebra + -- (FractionRing R)[X] is a localization of R[X] at nzdMapC + letI : IsLocalization (nzdMapC R) (FractionRing R)[X] := + Polynomial.isLocalization (nonZeroDivisors R) (FractionRing R) + -- The localization at constPrimeSubmonoid is also a localization at nzdMapC + letI : 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 + haveI : 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 diff --git a/LeanPool/NagataFactoriality/NagataFactoriality/Applications/Gauss.lean b/LeanPool/NagataFactoriality/NagataFactoriality/Applications/Gauss.lean new file mode 100644 index 0000000000..897249e82a --- /dev/null +++ b/LeanPool/NagataFactoriality/NagataFactoriality/Applications/Gauss.lean @@ -0,0 +1,26 @@ +/- +Copyright (c) 2026 Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina G. de Oliveira. 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 +-/ +import Mathlib.RingTheory.Polynomial.Content +import Mathlib.RingTheory.Polynomial.GaussLemma +import Mathlib.RingTheory.Polynomial.UniqueFactorization + +namespace NagataFactoriality + +open Polynomial + +theorem polynomial_content_mul {R : Type*} [CommRing R] [IsDomain R] [NormalizedGCDMonoid R] + (p q : R[X]) : (p * q).content = p.content * q.content := + Polynomial.content_mul + +theorem primitive_mul {R : Type*} [CommRing R] [IsDomain 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] [IsDomain R] + [UniqueFactorizationMonoid R] : UniqueFactorizationMonoid R[X] := by + infer_instance + +end NagataFactoriality diff --git a/LeanPool/NagataFactoriality/NagataFactoriality/Applications/Laurent.lean b/LeanPool/NagataFactoriality/NagataFactoriality/Applications/Laurent.lean new file mode 100644 index 0000000000..86f61f4d20 --- /dev/null +++ b/LeanPool/NagataFactoriality/NagataFactoriality/Applications/Laurent.lean @@ -0,0 +1,114 @@ +/- +Copyright (c) 2026 Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina G. de Oliveira. 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 +-/ +import Mathlib.Algebra.Polynomial.Laurent +import Mathlib.Algebra.Polynomial.RingDivision +import Mathlib.RingTheory.Localization.Ideal +import Mathlib.RingTheory.Polynomial.UniqueFactorization +import LeanPool.NagataFactoriality.NagataFactoriality.Nagata.Lemmas +import LeanPool.NagataFactoriality.NagataFactoriality.Nagata.Theorem + +namespace NagataFactoriality + +open scoped LaurentPolynomial +open Polynomial + +theorem laurentPolynomial_isLocalization (R : Type*) [CommSemiring R] : + IsLocalization.Away (X : R[X]) R[T;T⁻¹] := + LaurentPolynomial.isLocalization + +theorem polynomial_prime_X {R : Type*} [CommRing R] [IsDomain R] : + Prime (Polynomial.X : R[X]) := + (Polynomial.prime_X : Prime (Polynomial.X : R[X])) + +theorem polynomial_toLaurent_prime_of_not_dvd_X {R : Type*} [CommRing R] [IsDomain R] + {p : R[X]} (hp : Prime p) (hX : ¬ p ∣ X) : Prime (Polynomial.toLaurent p) := by + let M : Submonoid R[X] := Submonoid.powers X + have hspanPrime : (Ideal.span ({p} : Set R[X])).IsPrime := + (Ideal.span_singleton_prime hp.ne_zero).2 hp + have hdisj : Disjoint (M : Set R[X]) ↑(Ideal.span ({p} : Set R[X])) := by + rw [Set.disjoint_left] + intro m hm hmspan + rcases hm with ⟨n, rfl⟩ + have hmspan' : p ∣ X ^ n := by + simpa [Ideal.mem_span_singleton] using hmspan + exact hX (hp.dvd_of_dvd_pow hmspan') + have hmapPrime : (Ideal.map (algebraMap R[X] R[T;T⁻¹]) (Ideal.span ({p} : Set R[X]))).IsPrime := + IsLocalization.isPrime_of_isPrime_disjoint M R[T;T⁻¹] _ hspanPrime hdisj + have hspanMap : Ideal.map (algebraMap R[X] R[T;T⁻¹]) (Ideal.span ({p} : Set R[X])) = + Ideal.span ({Polynomial.toLaurent p} : Set R[T;T⁻¹]) := by + simpa [LaurentPolynomial.algebraMap_eq_toLaurent, Set.image_singleton] using + (Ideal.map_span (algebraMap R[X] R[T;T⁻¹]) ({p} : Set R[X])) + rw [hspanMap] at hmapPrime + exact (Ideal.span_singleton_prime (Polynomial.toLaurent_ne_zero.2 hp.ne_zero)).1 hmapPrime + +theorem laurentPolynomial_uniqueFactorizationMonoid {R : Type*} [CommRing R] [IsDomain R] + [UniqueFactorizationMonoid R] : UniqueFactorizationMonoid R[T;T⁻¹] := by + letI : UniqueFactorizationMonoid R[X] := inferInstance + rw [UniqueFactorizationMonoid.iff_exists_prime_factors] + intro f hf + obtain ⟨n, p, hpLaurent⟩ := LaurentPolynomial.exists_T_pow f + have hp0 : p ≠ 0 := by + intro hpz + have hT0 : (LaurentPolynomial.T n : R[T;T⁻¹]) ≠ 0 := (LaurentPolynomial.isUnit_T n).ne_zero + have : f * LaurentPolynomial.T n = 0 := by + simpa [hpz] using hpLaurent.symm + exact hf ((mul_eq_zero.mp this).resolve_right hT0) + obtain ⟨q, hpq, hqX⟩ := p.exists_eq_pow_rootMultiplicity_mul_and_not_dvd hp0 0 + have hpq' : p = X ^ p.rootMultiplicity 0 * q := by + simpa using hpq + have hqX' : ¬ X ∣ q := by + simpa using hqX + have hq0 : q ≠ 0 := by + intro hq0 + apply hp0 + rw [hpq', hq0, mul_zero] + obtain ⟨w, hwprime, hwassoc⟩ := UniqueFactorizationMonoid.exists_prime_factors q hq0 + refine ⟨w.map Polynomial.toLaurent, ?_, ?_⟩ + · intro z hz + rcases Multiset.mem_map.1 hz with ⟨r, hr, rfl⟩ + have hrdvdq : r ∣ q := hwassoc.dvd_iff_dvd_right.mp (Multiset.dvd_prod hr) + have hrnot : ¬ r ∣ X := by + intro hrX + have hassoc : Associated r X := + (hwprime r hr).irreducible.associated_of_dvd Polynomial.irreducible_X hrX + exact hqX' (dvd_trans hassoc.symm.dvd hrdvdq) + exact polynomial_toLaurent_prime_of_not_dvd_X (hwprime r hr) hrnot + · have hmapassoc : Associated (w.map Polynomial.toLaurent).prod (Polynomial.toLaurent q) := by + rw [Multiset.prod_hom] + exact hwassoc.map Polynomial.toLaurent + have hfp : Associated f (Polynomial.toLaurent p) := by + rw [hpLaurent] + exact associated_mul_unit_right _ _ (LaurentPolynomial.isUnit_T n) + have hpqAssoc : Associated (Polynomial.toLaurent p) (Polynomial.toLaurent q) := by + rw [hpq', map_mul, Polynomial.toLaurent_X_pow] + simpa [LaurentPolynomial.T_mul] using + (associated_mul_unit_left (Polynomial.toLaurent q) (LaurentPolynomial.T (p.rootMultiplicity 0)) + (LaurentPolynomial.isUnit_T (p.rootMultiplicity 0))) + exact hmapassoc.trans (hfp.trans hpqAssoc).symm + +theorem polynomial_uniqueFactorizationMonoid_of_laurent {R : Type*} [CommRing R] [IsDomain R] + [IsNoetherianRing R] [UniqueFactorizationMonoid R[T;T⁻¹]] : + UniqueFactorizationMonoid R[X] := by + let S : Submonoid R[X] := Submonoid.powers X + have hS : PrimeGenerated S := by + simpa [S] using (primeGenerated_powers (p := (X : R[X])) (polynomial_prime_X (R := R))) + letI : _root_.IsLocalization S R[T;T⁻¹] := by + simpa [S] using (laurentPolynomial_isLocalization R : _root_.IsLocalization.Away (X : R[X]) R[T;T⁻¹]) + exact nagata_theorem_isLocalization (R := R[X]) (T := R[T;T⁻¹]) S hS inferInstance + +theorem polynomial_uniqueFactorizationMonoid_via_nagata {R : Type*} [CommRing R] [IsDomain R] + [IsNoetherianRing R] [UniqueFactorizationMonoid R] : UniqueFactorizationMonoid R[X] := by + letI : UniqueFactorizationMonoid R[T;T⁻¹] := laurentPolynomial_uniqueFactorizationMonoid (R := R) + exact polynomial_uniqueFactorizationMonoid_of_laurent (R := R) + +theorem iterated_polynomial_uniqueFactorizationMonoid_via_nagata + {R : Type*} [CommRing R] [IsDomain R] [IsNoetherianRing R] + [UniqueFactorizationMonoid R] : UniqueFactorizationMonoid (Polynomial (Polynomial R)) := by + letI : UniqueFactorizationMonoid R[X] := + polynomial_uniqueFactorizationMonoid_via_nagata (R := R) + simpa using polynomial_uniqueFactorizationMonoid_via_nagata (R := R[X]) + +end NagataFactoriality diff --git a/LeanPool/NagataFactoriality/NagataFactoriality/Basic.lean b/LeanPool/NagataFactoriality/NagataFactoriality/Basic.lean new file mode 100644 index 0000000000..c09562f153 --- /dev/null +++ b/LeanPool/NagataFactoriality/NagataFactoriality/Basic.lean @@ -0,0 +1,9 @@ +/- +Copyright (c) 2026 Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina G. de Oliveira. 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 +-/ +import LeanPool.NagataFactoriality.NagataFactoriality.Basic.Ring +import LeanPool.NagataFactoriality.NagataFactoriality.Basic.Divisibility +import LeanPool.NagataFactoriality.NagataFactoriality.Basic.Noetherian +import LeanPool.NagataFactoriality.NagataFactoriality.Basic.UFD diff --git a/LeanPool/NagataFactoriality/NagataFactoriality/Basic/Divisibility.lean b/LeanPool/NagataFactoriality/NagataFactoriality/Basic/Divisibility.lean new file mode 100644 index 0000000000..91efe32ce6 --- /dev/null +++ b/LeanPool/NagataFactoriality/NagataFactoriality/Basic/Divisibility.lean @@ -0,0 +1,81 @@ +/- +Copyright (c) 2026 Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina G. de Oliveira. 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 +-/ +import Mathlib.RingTheory.Noetherian.UniqueFactorizationDomain +import LeanPool.NagataFactoriality.NagataFactoriality.Basic.Ring + +namespace NagataFactoriality + +open scoped BigOperators + +def listProd {α : Type*} [CommMonoid α] : List α → α + | [] => 1 + | a :: as => a * listProd as + +@[simp] theorem listProd_nil {α : Type*} [CommMonoid α] : listProd ([] : List α) = 1 := rfl + +@[simp] theorem listProd_cons {α : Type*} [CommMonoid α] (a : α) (as : List α) : + listProd (a :: as) = a * listProd as := rfl + +theorem listProd_append {α : Type*} [CommMonoid α] (xs ys : List α) : + listProd (xs ++ ys) = listProd xs * listProd ys := by + induction xs with + | nil => simp [listProd] + | cons x xs ih => simp [listProd, ih, mul_assoc] + +theorem dvd_refl {α : Type*} [CommMonoid α] (a : α) : a ∣ a := dvd_rfl + +theorem dvd_trans {α : Type*} [CommMonoid α] {a b c : α} : + a ∣ b → b ∣ c → a ∣ c := by + intro hab hbc + exact Dvd.dvd.trans hab hbc + +theorem dvd_mul_of_dvd_left {α : Type*} [CommMonoid α] {a b c : α} : + a ∣ b → a ∣ b * c := by + intro h + exact dvd_trans h (dvd_mul_right b c) + +theorem dvd_mul_of_dvd_right {α : Type*} [CommMonoid α] {a b c : α} : + a ∣ c → a ∣ b * c := by + intro h + exact dvd_trans h (dvd_mul_left c b) + +theorem isUnit_one {α : Type*} [CommMonoid α] : IsUnit (1 : α) := _root_.isUnit_one + +theorem isUnit_mul {α : Type*} [CommMonoid α] {a b : α} : + IsUnit a → IsUnit b → IsUnit (a * b) := by + intro ha hb + exact ha.mul hb + +theorem isUnit_of_dvd_one {α : Type*} [CommMonoid α] {a : α} (h : a ∣ 1) : IsUnit a := + _root_.isUnit_of_dvd_one h + +theorem isUnit_ne_zero {α : Type*} [CommRing α] [IsDomain α] {a : α} (ha : IsUnit a) : a ≠ 0 := + ha.ne_zero + +theorem associated_refl {α : Type*} [Monoid α] (a : α) : Associated a a := Associated.refl a + +theorem associated_symm {α : Type*} [Monoid α] {a b : α} : + Associated a b → Associated b a := Associated.symm + +theorem associated_trans {α : Type*} [Monoid α] {a b c : α} : + Associated a b → Associated b c → Associated a c := fun hab hbc => hab.trans hbc + +theorem dvd_of_associated {α : Type*} [Monoid α] {a b : α} (h : Associated a b) : a ∣ b := + h.dvd + +theorem prime_irreducible {α : Type*} [CommRing α] [IsDomain α] {p : α} (hp : Prime p) : + Irreducible p := + hp.irreducible + +theorem associated_of_irreducible_of_dvd {α : Type*} [CommRing α] [IsDomain α] {p q : α} + (hp : Irreducible p) (hq : Irreducible q) (hdiv : p ∣ q) : Associated p q := by + exact (hp.dvd_irreducible_iff_associated hq).mp hdiv + +theorem prime_of_associated {α : Type*} [CommRing α] [IsDomain α] {p q : α} + (hp : Prime p) (hassoc : Associated p q) : Prime q := by + exact (hassoc.prime_iff).mp hp + +end NagataFactoriality diff --git a/LeanPool/NagataFactoriality/NagataFactoriality/Basic/Noetherian.lean b/LeanPool/NagataFactoriality/NagataFactoriality/Basic/Noetherian.lean new file mode 100644 index 0000000000..83857287f1 --- /dev/null +++ b/LeanPool/NagataFactoriality/NagataFactoriality/Basic/Noetherian.lean @@ -0,0 +1,20 @@ +/- +Copyright (c) 2026 Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina G. de Oliveira. 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 +-/ +import Mathlib.RingTheory.Noetherian.UniqueFactorizationDomain +import LeanPool.NagataFactoriality.NagataFactoriality.Basic.Divisibility + +namespace NagataFactoriality + +theorem hasFactorization_of_noetherian {α : Type*} [CommRing α] [IsDomain α] + [IsNoetherianRing α] : WfDvdMonoid α := by + infer_instance + +theorem IsNoetherianRing.hasFactorization {α : Type*} [CommRing α] [IsDomain α] + (h : IsNoetherianRing α) : WfDvdMonoid α := by + letI := h + exact hasFactorization_of_noetherian (α := α) + +end NagataFactoriality diff --git a/LeanPool/NagataFactoriality/NagataFactoriality/Basic/Ring.lean b/LeanPool/NagataFactoriality/NagataFactoriality/Basic/Ring.lean new file mode 100644 index 0000000000..32a825c502 --- /dev/null +++ b/LeanPool/NagataFactoriality/NagataFactoriality/Basic/Ring.lean @@ -0,0 +1,10 @@ +/- +Copyright (c) 2026 Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina G. de Oliveira. 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 +-/ +import Mathlib + +namespace NagataFactoriality + +end NagataFactoriality diff --git a/LeanPool/NagataFactoriality/NagataFactoriality/Basic/UFD.lean b/LeanPool/NagataFactoriality/NagataFactoriality/Basic/UFD.lean new file mode 100644 index 0000000000..4b545e3c26 --- /dev/null +++ b/LeanPool/NagataFactoriality/NagataFactoriality/Basic/UFD.lean @@ -0,0 +1,69 @@ +/- +Copyright (c) 2026 Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina G. de Oliveira. 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 +-/ +import Mathlib.RingTheory.UniqueFactorizationDomain.Basic +import LeanPool.NagataFactoriality.NagataFactoriality.Basic.Noetherian + +namespace NagataFactoriality + +theorem ufd_iff_factorization_and_irreducibles_prime {α : Type*} [CommRing α] [IsDomain α] : + UniqueFactorizationMonoid α ↔ WfDvdMonoid α ∧ ∀ p : α, Irreducible p → Prime p := by + constructor + · intro h + refine ⟨?_, ?_⟩ + · letI : UniqueFactorizationMonoid α := h + exact (inferInstance : WfDvdMonoid α) + · intro p hp + letI : UniqueFactorizationMonoid α := h + exact (UniqueFactorizationMonoid.irreducible_iff_prime).mp hp + · rintro ⟨hfac, hprime⟩ + exact UniqueFactorizationMonoid.of_exists_prime_factors (fun a ha => by + letI : WfDvdMonoid α := hfac + obtain ⟨f, hf, hassoc⟩ := WfDvdMonoid.exists_factors a ha + refine ⟨f, ?_, hassoc⟩ + intro b hb + exact hprime b (hf b hb)) + +theorem prime_iff_irreducible_of_ufd {α : Type*} [CommRing α] [IsDomain α] + [UniqueFactorizationMonoid α] {p : α} : Prime p ↔ Irreducible p := + UniqueFactorizationMonoid.irreducible_iff_prime.symm + +theorem ufd_of_factorization_and_primes {α : Type*} [CommRing α] [IsDomain α] + (hfac : WfDvdMonoid α) + (hprime : ∀ p : α, Irreducible p → Prime p) : UniqueFactorizationMonoid α := by + exact (ufd_iff_factorization_and_irreducibles_prime (α := α)).2 ⟨hfac, hprime⟩ + +/-- Two factorizations are equivalent when they differ only by associates and permutation. -/ +abbrev FactorizationEquivalent {α : Type*} [Monoid α] (f g : Multiset α) : Prop := + Multiset.Rel Associated f g + +theorem factorizationEquivalent_iff_map_eq_map {α : Type*} [CommMonoid α] {f g : Multiset α} : + FactorizationEquivalent f g ↔ f.map Associates.mk = g.map Associates.mk := + Associates.rel_associated_iff_map_eq_map + +theorem factorization_unique {α : Type*} [CommRing α] [IsDomain α] + (hfac : WfDvdMonoid α) + (hprime : ∀ p : α, Irreducible p → Prime p) + {f g : Multiset α} + (hf : ∀ x ∈ f, Irreducible x) + (hg : ∀ x ∈ g, Irreducible x) + (hfg : Associated f.prod g.prod) : + FactorizationEquivalent f g := by + letI : UniqueFactorizationMonoid α := ufd_of_factorization_and_primes hfac hprime + exact UniqueFactorizationMonoid.factors_unique hf hg hfg + +theorem factors_unique {α : Type*} [CommRing α] [IsDomain α] + (hfac : WfDvdMonoid α) + (hprime : ∀ p : α, Irreducible p → Prime p) + {a : α} (ha : a ≠ 0) {f : Multiset α} + (hf : ∀ x ∈ f, Irreducible x) + (hfa : Associated f.prod a) : + letI : UniqueFactorizationMonoid α := ufd_of_factorization_and_primes hfac hprime + FactorizationEquivalent f (UniqueFactorizationMonoid.factors a) := by + letI : UniqueFactorizationMonoid α := ufd_of_factorization_and_primes hfac hprime + exact UniqueFactorizationMonoid.factors_unique hf UniqueFactorizationMonoid.irreducible_of_factor + (hfa.trans (UniqueFactorizationMonoid.factors_prod ha).symm) + +end NagataFactoriality diff --git a/LeanPool/NagataFactoriality/NagataFactoriality/Localization.lean b/LeanPool/NagataFactoriality/NagataFactoriality/Localization.lean new file mode 100644 index 0000000000..fdcce48ca3 --- /dev/null +++ b/LeanPool/NagataFactoriality/NagataFactoriality/Localization.lean @@ -0,0 +1,9 @@ +/- +Copyright (c) 2026 Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina G. de Oliveira. 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 +-/ +import LeanPool.NagataFactoriality.NagataFactoriality.Localization.MultSet +import LeanPool.NagataFactoriality.NagataFactoriality.Localization.Localization +import LeanPool.NagataFactoriality.NagataFactoriality.Localization.IsLocalization +import LeanPool.NagataFactoriality.NagataFactoriality.Localization.Properties diff --git a/LeanPool/NagataFactoriality/NagataFactoriality/Localization/IsLocalization.lean b/LeanPool/NagataFactoriality/NagataFactoriality/Localization/IsLocalization.lean new file mode 100644 index 0000000000..50dc8456fc --- /dev/null +++ b/LeanPool/NagataFactoriality/NagataFactoriality/Localization/IsLocalization.lean @@ -0,0 +1,120 @@ +/- +Copyright (c) 2026 Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina G. de Oliveira. 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 +-/ +import Mathlib.RingTheory.Localization.Basic +import LeanPool.NagataFactoriality.NagataFactoriality.Localization.MultSet + +namespace NagataFactoriality + +namespace IsLocalization + +variable {α β : Type*} [CommRing α] [CommRing β] {S : Submonoid α} +variable [Algebra α β] [_root_.IsLocalization S β] + +@[simp] theorem mk'_mul_map (a s : α) (hs : s ∈ S) : + _root_.IsLocalization.mk' β a ⟨s, hs⟩ * algebraMap α β s = algebraMap α β a := by + exact _root_.IsLocalization.mk'_spec_mk (M := S) (S := β) a s hs + +@[simp] theorem map_mul_mk' (a b s : α) (hs : s ∈ S) : + algebraMap α β a * _root_.IsLocalization.mk' β b ⟨s, hs⟩ = + _root_.IsLocalization.mk' β (a * b) ⟨s, hs⟩ := by + simpa using (_root_.IsLocalization.mul_mk'_eq_mk'_of_mul (M := S) (S := β) a b ⟨s, hs⟩) + +theorem surj (z : β) : ∃ a s, ∃ hs : s ∈ S, z = _root_.IsLocalization.mk' β a ⟨s, hs⟩ := by + obtain ⟨a, s, hs⟩ := _root_.IsLocalization.mk'_surjective (M := S) (S := β) z + exact ⟨a, s, s.property, hs.symm⟩ + +section Nonzero + +variable [IsDomain α] [Fact ((0 : α) ∉ S)] + +theorem algebraMap_injective (S : Submonoid α) [Fact ((0 : α) ∉ S)] [_root_.IsLocalization S β] : + Function.Injective (algebraMap α β) := + let hle : S ≤ nonZeroDivisors α := NagataFactoriality.Submonoid.le_nonZeroDivisors + _root_.IsLocalization.injective (M := S) (S := β) hle + +theorem mk'_eq_iff {a b s t : α} (hs : s ∈ S) (ht : t ∈ S) : + _root_.IsLocalization.mk' β a ⟨s, hs⟩ = _root_.IsLocalization.mk' β b ⟨t, ht⟩ ↔ a * t = b * s := by + constructor + · intro h + have h' := (_root_.IsLocalization.mk'_eq_iff_eq' (M := S) (S := β)).1 h + exact algebraMap_injective (α := α) (β := β) S <| by + simpa [map_mul, mul_assoc, mul_left_comm, mul_comm] using h' + · intro h + exact _root_.IsLocalization.mk'_eq_of_eq' (M := S) (S := β) <| by + simpa [mul_assoc, mul_left_comm, mul_comm] using h.symm + +theorem map_eq_iff (S : Submonoid α) [Fact ((0 : α) ∉ S)] [_root_.IsLocalization S β] (a b : α) : + algebraMap α β a = algebraMap α β b ↔ a = b := + (algebraMap_injective (α := α) (β := β) S).eq_iff + +theorem mk'_eq_zero_iff {a s : α} (hs : s ∈ S) : + _root_.IsLocalization.mk' β a ⟨s, hs⟩ = 0 ↔ a = 0 := by + have h := mk'_eq_iff (S := S) (β := β) (a := a) (b := 0) (s := s) (t := 1) hs S.one_mem + simpa using h + +@[simp] theorem map_eq_zero_iff (S : Submonoid α) [Fact ((0 : α) ∉ S)] [_root_.IsLocalization S β] + (a : α) : algebraMap α β a = 0 ↔ a = 0 := by + let hle : S ≤ nonZeroDivisors α := NagataFactoriality.Submonoid.le_nonZeroDivisors + exact _root_.IsLocalization.to_map_eq_zero_iff (M := S) (S := β) (x := a) hle + +theorem dvd_map_iff {a b : α} : + algebraMap α β a ∣ algebraMap α β b ↔ ∃ s : α, s ∈ S ∧ a ∣ s * b := by + constructor + · rintro ⟨x, hx⟩ + obtain ⟨c, s, hs, rfl⟩ := surj (S := S) (β := β) x + refine ⟨s, hs, ?_⟩ + have hEq : algebraMap α β b = _root_.IsLocalization.mk' β (a * c) ⟨s, hs⟩ := by + calc + algebraMap α β b = algebraMap α β a * _root_.IsLocalization.mk' β c ⟨s, hs⟩ := hx + _ = _root_.IsLocalization.mk' β (a * c) ⟨s, hs⟩ := map_mul_mk' (S := S) a c s hs + have hCross : algebraMap α β (b * s) = algebraMap α β (a * c) := by + have hCross' : + algebraMap α β b * algebraMap α β s = algebraMap α β (a * c) := by + exact (_root_.IsLocalization.eq_mk'_iff_mul_eq (M := S) (S := β) + (z := algebraMap α β b) (x := a * c) (y := ⟨s, hs⟩)).1 hEq + simpa [map_mul, mul_assoc, mul_left_comm, mul_comm] using hCross' + refine ⟨c, ?_⟩ + exact by simpa [mul_comm] using (algebraMap_injective (α := α) (β := β) S hCross) + · rintro ⟨s, hs, c, hc⟩ + refine ⟨_root_.IsLocalization.mk' β c ⟨s, hs⟩, ?_⟩ + symm + calc + algebraMap α β a * _root_.IsLocalization.mk' β c ⟨s, hs⟩ = + _root_.IsLocalization.mk' β (a * c) ⟨s, hs⟩ := map_mul_mk' (S := S) a c s hs + _ = _root_.IsLocalization.mk' β b ⟨1, S.one_mem⟩ := by + apply (mk'_eq_iff (S := S) (β := β) (hs := hs) (ht := S.one_mem)).2 + simpa [mul_assoc, mul_left_comm, mul_comm] using hc.symm + _ = algebraMap α β b := by simpa using (_root_.IsLocalization.mk'_one (S := β) b) + +end Nonzero + +@[simp] theorem isUnit_mk'_of_mem {a s : α} (ha : a ∈ S) (hs : s ∈ S) : + IsUnit (_root_.IsLocalization.mk' β a ⟨s, hs⟩) := by + apply isUnit_iff_exists_inv.2 + refine ⟨_root_.IsLocalization.mk' β s ⟨a, ha⟩, ?_⟩ + simpa using (_root_.IsLocalization.mk'_mul_mk'_eq_one' (M := S) (S := β) a ⟨s, hs⟩ ha) + +theorem isUnit_map_of_mem {s : α} (hs : s ∈ S) : IsUnit (algebraMap α β s) := by + simpa using (_root_.IsLocalization.map_units (S := β) ⟨s, hs⟩) + +theorem isUnit_map_of_isUnit {a : α} (ha : IsUnit a) : IsUnit (algebraMap α β a) := + ha.map (algebraMap α β) + +theorem isUnit_mk'_of_isUnit {a s : α} (ha : IsUnit a) (hs : s ∈ S) : + IsUnit (_root_.IsLocalization.mk' β a ⟨s, hs⟩) := by + have hmk : + _root_.IsLocalization.mk' β a ⟨s, hs⟩ = + algebraMap α β a * _root_.IsLocalization.mk' β 1 ⟨s, hs⟩ := by + calc + _root_.IsLocalization.mk' β a ⟨s, hs⟩ = _root_.IsLocalization.mk' β (a * 1) ⟨s, hs⟩ := by simp + _ = algebraMap α β a * _root_.IsLocalization.mk' β 1 ⟨s, hs⟩ := by + rw [← map_mul_mk' (S := S) a 1 s hs] + rw [hmk] + exact (isUnit_map_of_isUnit (β := β) ha).mul (isUnit_mk'_of_mem (β := β) S.one_mem hs) + +end IsLocalization + +end NagataFactoriality diff --git a/LeanPool/NagataFactoriality/NagataFactoriality/Localization/Localization.lean b/LeanPool/NagataFactoriality/NagataFactoriality/Localization/Localization.lean new file mode 100644 index 0000000000..9673417cf6 --- /dev/null +++ b/LeanPool/NagataFactoriality/NagataFactoriality/Localization/Localization.lean @@ -0,0 +1,182 @@ +/- +Copyright (c) 2026 Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina G. de Oliveira. 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 +-/ +import Mathlib.RingTheory.Localization.Basic +import LeanPool.NagataFactoriality.NagataFactoriality.Localization.MultSet + +namespace NagataFactoriality + +abbrev Localization {α : Type*} [CommRing α] (S : Submonoid α) := _root_.Localization S + +namespace Localization + +variable {α : Type*} [CommRing α] {S : Submonoid α} + +def mk (a s : α) (hs : s ∈ S) : Localization S := + _root_.Localization.mk a ⟨s, hs⟩ + +def of (a : α) : Localization S := + algebraMap α (Localization S) a + +@[simp] theorem mk_one (a : α) : mk (S := S) a 1 S.one_mem = of (S := S) a := by + simpa [mk, of] using (_root_.Localization.mk_one_eq_algebraMap (M := S) a) + +@[simp] theorem of_zero : of (S := S) (0 : α) = 0 := by + simp [of] + +@[simp] theorem of_one : of (S := S) (1 : α) = 1 := by + simp [of] + +@[simp] theorem of_add (a b : α) : of (S := S) (a + b) = of (S := S) a + of (S := S) b := by + simp [of] + +@[simp] theorem of_mul (a b : α) : of (S := S) (a * b) = of (S := S) a * of (S := S) b := by + simp [of] + +@[simp] theorem of_neg (a : α) : of (S := S) (-a) = -of (S := S) a := by + simp [of] + +@[simp] theorem mk_mul_den (a s : α) (hs : s ∈ S) : + mk (S := S) a s hs * of (S := S) s = of (S := S) a := by + rw [mk, of, _root_.Localization.mk_eq_mk'_apply] + exact IsLocalization.mk'_spec_mk (M := S) (S := Localization S) a s hs + +@[simp] theorem den_mul_mk (a s : α) (hs : s ∈ S) : + of (S := S) s * mk (S := S) a s hs = of (S := S) a := by + rw [mul_comm] + exact mk_mul_den (S := S) a s hs + +theorem surj (z : Localization S) : ∃ a s, ∃ hs : s ∈ S, z = mk (S := S) a s hs := by + obtain ⟨a, s, hs⟩ := IsLocalization.mk'_surjective (M := S) (S := Localization S) z + exact ⟨a, s, s.property, by + simpa [mk, _root_.Localization.mk_eq_mk'_apply] using hs.symm⟩ + +section Nonzero + +variable [IsDomain α] [Fact ((0 : α) ∉ S)] + +instance : IsDomain (Localization S) := + IsLocalization.isDomain_localization (M := S) (Submonoid.le_nonZeroDivisors (S := S)) + +theorem algebraMap_injective : Function.Injective (algebraMap α (Localization S)) := + IsLocalization.injective (M := S) (S := Localization S) (Submonoid.le_nonZeroDivisors (S := S)) + +theorem mk_eq_iff {a b s t : α} (hs : s ∈ S) (ht : t ∈ S) : + mk (S := S) a s hs = mk (S := S) b t ht ↔ a * t = b * s := by + constructor + · intro h + have h' : + algebraMap α (Localization S) (a * t) = algebraMap α (Localization S) (b * s) := by + have h'' : + IsLocalization.mk' (Localization S) a ⟨s, hs⟩ = + IsLocalization.mk' (Localization S) b ⟨t, ht⟩ := by + simpa [mk, _root_.Localization.mk_eq_mk'_apply] using h + exact (IsLocalization.mk'_eq_iff_eq' (M := S) (S := Localization S)).1 h'' + exact algebraMap_injective (S := S) <| + by simpa [map_mul, mul_assoc, mul_left_comm, mul_comm] using h' + · intro h + have h' : + IsLocalization.mk' (Localization S) a ⟨s, hs⟩ = + IsLocalization.mk' (Localization S) b ⟨t, ht⟩ := by + exact IsLocalization.mk'_eq_of_eq' (M := S) (S := Localization S) <| + by simpa [mul_assoc, mul_left_comm, mul_comm] using h.symm + simpa [mk, _root_.Localization.mk_eq_mk'_apply] using h' + +theorem of_eq_iff (a b : α) : of (S := S) a = of (S := S) b ↔ a = b := + (algebraMap_injective (S := S)).eq_iff + +theorem mk_eq_zero_iff {a s : α} (hs : s ∈ S) : mk (S := S) a s hs = 0 ↔ a = 0 := by + have h := mk_eq_iff (S := S) (a := a) (b := 0) (s := s) (t := 1) hs S.one_mem + simpa [of] using h + +@[simp] theorem of_eq_zero_iff (a : α) : of (S := S) a = 0 ↔ a = 0 := by + show algebraMap α (Localization S) a = 0 ↔ a = 0 + exact IsLocalization.to_map_eq_zero_iff (M := S) (S := Localization S) (x := a) + (Submonoid.le_nonZeroDivisors (S := S)) + +end Nonzero + +@[simp] theorem mk_mul_mk {a b s t : α} (hs : s ∈ S) (ht : t ∈ S) : + mk (S := S) a s hs * mk (S := S) b t ht = + mk (S := S) (a * b) (s * t) (S.mul_mem hs ht) := by + simpa [mk, _root_.Localization.mk_eq_mk'_apply] using + (IsLocalization.mk'_mul (M := S) (S := Localization S) a b ⟨s, hs⟩ ⟨t, ht⟩).symm + +@[simp] theorem of_mul_mk (a b s : α) (hs : s ∈ S) : + of (S := S) a * mk (S := S) b s hs = mk (S := S) (a * b) s hs := by + simpa [mk, of, _root_.Localization.mk_eq_mk'_apply] using + (IsLocalization.mul_mk'_eq_mk'_of_mul (M := S) (S := Localization S) a b ⟨s, hs⟩) + +@[simp] theorem mk_mul_of (a b s : α) (hs : s ∈ S) : + mk (S := S) a s hs * of (S := S) b = mk (S := S) (a * b) s hs := by + calc + mk (S := S) a s hs * of (S := S) b = + of (S := S) b * mk (S := S) a s hs := by rw [mul_comm] + _ = mk (S := S) (b * a) s hs := of_mul_mk (S := S) b a s hs + _ = mk (S := S) (a * b) s hs := by rw [mul_comm] + +theorem isUnit_mk_of_mem {a s : α} (ha : a ∈ S) (hs : s ∈ S) : + IsUnit (mk (S := S) a s hs) := by + apply isUnit_iff_exists_inv.2 + refine ⟨mk (S := S) s a ha, ?_⟩ + simpa [mk, _root_.Localization.mk_eq_mk'_apply] using + (IsLocalization.mk'_mul_mk'_eq_one' (M := S) (S := Localization S) a ⟨s, hs⟩ ha) + +theorem isUnit_of_mem {s : α} (hs : s ∈ S) : IsUnit (of (S := S) s) := by + simpa [of] using (IsLocalization.map_units (S := Localization S) ⟨s, hs⟩) + +theorem isUnit_of_isUnit {a : α} (ha : IsUnit a) : IsUnit (of (S := S) a) := + ha.map (algebraMap α (Localization S)) + +theorem isUnit_mk_of_isUnit {a s : α} (ha : IsUnit a) (hs : s ∈ S) : + IsUnit (mk (S := S) a s hs) := by + have hmk : mk (S := S) a s hs = of (S := S) a * mk (S := S) 1 s hs := by + calc + mk (S := S) a s hs = mk (S := S) (a * 1) s hs := by simp + _ = of (S := S) a * mk (S := S) 1 s hs := by + rw [← of_mul_mk (S := S) a 1 s hs] + rw [hmk] + exact isUnit_mul (isUnit_of_isUnit (S := S) ha) (isUnit_mk_of_mem (S := S) S.one_mem hs) + +section Nonzero + +variable [IsDomain α] [Fact ((0 : α) ∉ S)] + +theorem dvd_of_iff {a b : α} : + of (S := S) a ∣ of (S := S) b ↔ ∃ s : α, s ∈ S ∧ a ∣ s * b := by + constructor + · rintro ⟨x, hx⟩ + obtain ⟨c, s, hs, rfl⟩ := surj (S := S) x + refine ⟨s, hs, ?_⟩ + have hEq : of (S := S) b = mk (S := S) (a * c) s hs := by + calc + of (S := S) b = of (S := S) a * mk (S := S) c s hs := hx + _ = mk (S := S) (a * c) s hs := of_mul_mk (S := S) a c s hs + have hCross : + algebraMap α (Localization S) (b * s) = algebraMap α (Localization S) (a * c) := by + have hCross' : + of (S := S) b * algebraMap α (Localization S) s = + algebraMap α (Localization S) (a * c) := by + exact (IsLocalization.eq_mk'_iff_mul_eq (M := S) (S := Localization S) + (z := of (S := S) b) (x := a * c) (y := ⟨s, hs⟩)).1 <| + by simpa [mk, of, _root_.Localization.mk_eq_mk'_apply] using hEq + simpa [of, map_mul, mul_assoc, mul_left_comm, mul_comm] using hCross' + have hEq' : b * s = a * c := (algebraMap_injective (S := S)) hCross + exact ⟨c, by simpa [mul_comm] using hEq'⟩ + · rintro ⟨s, hs, c, hc⟩ + refine ⟨mk (S := S) c s hs, ?_⟩ + symm + calc + of (S := S) a * mk (S := S) c s hs = mk (S := S) (a * c) s hs := + of_mul_mk (S := S) a c s hs + _ = of (S := S) b := by + apply (mk_eq_iff (S := S) (hs := hs) (ht := S.one_mem)).2 + simpa [mul_assoc, mul_left_comm, mul_comm] using hc.symm + +end Nonzero + +end Localization + +end NagataFactoriality diff --git a/LeanPool/NagataFactoriality/NagataFactoriality/Localization/MultSet.lean b/LeanPool/NagataFactoriality/NagataFactoriality/Localization/MultSet.lean new file mode 100644 index 0000000000..5ea7e2561e --- /dev/null +++ b/LeanPool/NagataFactoriality/NagataFactoriality/Localization/MultSet.lean @@ -0,0 +1,35 @@ +/- +Copyright (c) 2026 Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina G. de Oliveira. 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 +-/ +import LeanPool.NagataFactoriality.NagataFactoriality.Basic.Divisibility + +namespace NagataFactoriality + +namespace Submonoid + +variable {α : Type*} [CommRing α] [IsDomain α] + +theorem zero_notMem_of_prime_or_unit {S : Submonoid α} + (hS : ∀ s ∈ S, Prime s ∨ IsUnit s) : (0 : α) ∉ S := by + intro h0 + rcases hS 0 h0 with h0prime | h0unit + · exact h0prime.ne_zero rfl + · exact h0unit.ne_zero rfl + +omit [IsDomain α] in +theorem mem_ne_zero {S : Submonoid α} [Fact ((0 : α) ∉ S)] {s : α} (hs : s ∈ S) : s ≠ 0 := by + intro hs0 + have h0 : (0 : α) ∈ S := by simpa [hs0] using hs + exact (Fact.out : (0 : α) ∉ S) h0 + +theorem le_nonZeroDivisors {S : Submonoid α} [Fact ((0 : α) ∉ S)] : + S ≤ nonZeroDivisors α := by + intro s hs + rw [mem_nonZeroDivisors_iff_ne_zero] + exact mem_ne_zero hs + +end Submonoid + +end NagataFactoriality diff --git a/LeanPool/NagataFactoriality/NagataFactoriality/Localization/Properties.lean b/LeanPool/NagataFactoriality/NagataFactoriality/Localization/Properties.lean new file mode 100644 index 0000000000..8801e46810 --- /dev/null +++ b/LeanPool/NagataFactoriality/NagataFactoriality/Localization/Properties.lean @@ -0,0 +1,7 @@ +/- +Copyright (c) 2026 Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina G. de Oliveira. 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 +-/ +import LeanPool.NagataFactoriality.NagataFactoriality.Localization.Localization +import LeanPool.NagataFactoriality.NagataFactoriality.Localization.IsLocalization diff --git a/LeanPool/NagataFactoriality/NagataFactoriality/Nagata.lean b/LeanPool/NagataFactoriality/NagataFactoriality/Nagata.lean new file mode 100644 index 0000000000..a6390a0749 --- /dev/null +++ b/LeanPool/NagataFactoriality/NagataFactoriality/Nagata.lean @@ -0,0 +1,7 @@ +/- +Copyright (c) 2026 Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina G. de Oliveira. 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 +-/ +import LeanPool.NagataFactoriality.NagataFactoriality.Nagata.Lemmas +import LeanPool.NagataFactoriality.NagataFactoriality.Nagata.Theorem diff --git a/LeanPool/NagataFactoriality/NagataFactoriality/Nagata/Lemmas.lean b/LeanPool/NagataFactoriality/NagataFactoriality/Nagata/Lemmas.lean new file mode 100644 index 0000000000..b772e8b437 --- /dev/null +++ b/LeanPool/NagataFactoriality/NagataFactoriality/Nagata/Lemmas.lean @@ -0,0 +1,656 @@ +/- +Copyright (c) 2026 Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina G. de Oliveira. 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 +-/ +import LeanPool.NagataFactoriality.NagataFactoriality.Localization.Properties +import LeanPool.NagataFactoriality.NagataFactoriality.Localization.IsLocalization +import LeanPool.NagataFactoriality.NagataFactoriality.Basic.UFD + +namespace NagataFactoriality + +def Avoids {α : Type*} [CommRing α] [IsDomain α] (S : Submonoid α) (p : α) : Prop := + ∀ s : α, s ∈ S → ¬ p ∣ s + +/-- A submonoid is prime-generated if each of its elements is a finite product of prime elements. -/ +def PrimeGenerated {α : Type*} [CommRing α] (S : Submonoid α) : Prop := + ∀ s : α, s ∈ S → ∃ f : Multiset α, (∀ q ∈ f, q ∈ S ∧ Prime q) ∧ f.prod = s + +private def submonoidZeroNotMemFact {α : Type*} [CommRing α] [IsDomain α] {S : Submonoid α} + (hS : ∀ s ∈ S, Prime s ∨ IsUnit s) : Fact ((0 : α) ∉ S) := + ⟨Submonoid.zero_notMem_of_prime_or_unit hS⟩ + +theorem multiset_prod_ne_zero_of_prime_factors {α : Type*} [CommRing α] [IsDomain α] + {f : Multiset α} (hf : ∀ q ∈ f, Prime q) : f.prod ≠ 0 := by + revert hf + refine Multiset.induction_on f ?_ ?_ + · intro _ + exact one_ne_zero + · intro q qs ih hqs + have hq : Prime q := hqs q (by simp) + have htail : ∀ r ∈ qs, Prime r := by + intro r hr + exact hqs r (by simp [hr]) + simpa using mul_ne_zero hq.ne_zero (ih htail) + +theorem zero_notMem_of_primeGenerated {α : Type*} [CommRing α] [IsDomain α] {S : Submonoid α} + (hS : PrimeGenerated S) : (0 : α) ∉ S := by + intro hs + rcases hS 0 hs with ⟨f, hf, hprod⟩ + exact (multiset_prod_ne_zero_of_prime_factors (fun q hq => (hf q hq).2)) hprod + +theorem primeGenerated_powers {α : Type*} [CommRing α] {p : α} (hp : Prime p) : + PrimeGenerated (Submonoid.powers p) := by + intro s hs + rcases hs with ⟨n, rfl⟩ + refine ⟨Multiset.replicate n p, ?_, by simp⟩ + intro q hq + have hqp : q = p := by + exact Multiset.eq_of_mem_replicate hq + subst hqp + refine ⟨⟨1, by simp⟩, hp⟩ + +theorem primeGenerated_closure_of_primes {α : Type*} [CommRing α] {s : Set α} + (hs : ∀ q ∈ s, Prime q) : PrimeGenerated (Submonoid.closure s) := by + intro x hx + induction hx using Submonoid.closure_induction (s := s) with + | mem x hx => + refine ⟨{x}, ?_, by simp⟩ + intro q hq + have hqx : q = x := Multiset.mem_singleton.mp hq + subst q + exact ⟨Submonoid.subset_closure hx, hs x hx⟩ + | one => + exact ⟨0, by simp⟩ + | mul x y hx hy ihx ihy => + rcases ihx with ⟨fx, hfx, hprodx⟩ + rcases ihy with ⟨fy, hfy, hprody⟩ + refine ⟨fx + fy, ?_, by simp [hprodx, hprody, Multiset.prod_add]⟩ + intro q hq + rcases Multiset.mem_add.mp hq with hq | hq + · exact hfx q hq + · exact hfy q hq + +theorem primeGenerated_closure_finset_of_primes {α : Type*} [CommRing α] (s : Finset α) + (hs : ∀ q ∈ s, Prime q) : PrimeGenerated (Submonoid.closure (↑s : Set α)) := + primeGenerated_closure_of_primes (s := (↑s : Set α)) (fun q hq => hs q hq) + +theorem prime_of_irreducible_of_dvd_prime_factors {α : Type*} [CommRing α] [IsDomain α] + {f : Multiset α} (hf : ∀ q ∈ f, Prime q) {p : α} + (hp : Irreducible p) (hdiv : p ∣ f.prod) : Prime p := by + revert hf hdiv + refine Multiset.induction_on f ?_ ?_ + · intro _ hdiv + exact False.elim (hp.not_isUnit (isUnit_of_dvd_one (by simpa using hdiv))) + · intro q qs ih hqs hdiv + have hq : Prime q := hqs q (by simp) + have htail : ∀ r ∈ qs, Prime r := by + intro r hr + exact hqs r (by simp [hr]) + rcases hdiv with ⟨d, hd⟩ + have hq_dvd : q ∣ p * d := by + refine ⟨qs.prod, ?_⟩ + simpa [Multiset.prod_cons, mul_assoc, mul_left_comm, mul_comm] using hd.symm + rcases hq.2.2 p d hq_dvd with hqp | hqd + · have hqIrred : Irreducible q := prime_irreducible hq + have hassoc : Associated q p := associated_of_irreducible_of_dvd hqIrred hp hqp + exact prime_of_associated hq hassoc + · rcases hqd with ⟨e, hde⟩ + have hcancel : qs.prod = p * e := by + apply mul_left_cancel₀ hq.ne_zero + calc + q * qs.prod = p * d := by simpa [Multiset.prod_cons, mul_assoc, mul_left_comm, mul_comm] using hd + _ = p * (q * e) := by rw [hde] + _ = q * (p * e) := by ac_rfl + exact ih htail ⟨e, hcancel⟩ + +theorem prime_of_irreducible_of_dvd_mem_primeGenerated {α : Type*} [CommRing α] [IsDomain α] + {S : Submonoid α} (hS : PrimeGenerated S) {p s : α} + (hp : Irreducible p) (hs : s ∈ S) (hdiv : p ∣ s) : Prime p := by + rcases hS s hs with ⟨f, hf, hprod⟩ + rw [← hprod] at hdiv + exact prime_of_irreducible_of_dvd_prime_factors (fun q hq => (hf q hq).2) hp hdiv + +theorem dvd_of_mul_eq_prime_factors {α : Type*} [CommRing α] [IsDomain α] + {f : Multiset α} (hf : ∀ q ∈ f, Prime q) {p a c : α} (hp : Irreducible p) + (hnot : ∀ q ∈ f, ¬ p ∣ q) (hEq : f.prod * a = p * c) : p ∣ a := by + have hmain : + ∀ g : Multiset α, (∀ q ∈ g, Prime q) → (∀ q ∈ g, ¬ p ∣ q) → + ∀ {d : α}, g.prod * a = p * d → p ∣ a := by + intro g + refine Multiset.induction_on g ?_ ?_ + · intro hg hnotg d hEqg + refine ⟨d, ?_⟩ + simpa using hEqg + · intro q qs ih hqs hnotqs d hEqqs + have hq : Prime q := hqs q (by simp) + have htail : ∀ r ∈ qs, Prime r := by + intro r hr + exact hqs r (by simp [hr]) + have htailNot : ∀ r ∈ qs, ¬ p ∣ r := by + intro r hr + exact hnotqs r (by simp [hr]) + have hqNot : ¬ p ∣ q := hnotqs q (by simp) + have hq_dvd : q ∣ p * d := by + refine ⟨qs.prod * a, ?_⟩ + simpa [mul_assoc] using hEqqs.symm + rcases hq.2.2 p d hq_dvd with hqp | hqc + · have hqIrred : Irreducible q := prime_irreducible hq + have hassoc : Associated q p := associated_of_irreducible_of_dvd hqIrred hp hqp + exact False.elim (hqNot (dvd_of_associated (associated_symm hassoc))) + · rcases hqc with ⟨e, hd⟩ + have hq0 : q ≠ 0 := hq.ne_zero + have hEq' : q * (qs.prod * a) = q * (p * e) := by + calc + q * (qs.prod * a) = (q ::ₘ qs).prod * a := by simp [mul_assoc] + _ = p * d := hEqqs + _ = p * (q * e) := by rw [hd] + _ = q * (p * e) := by ac_rfl + have hcancel : qs.prod * a = p * e := mul_left_cancel₀ hq0 hEq' + exact ih htail htailNot hcancel + exact hmain f hf hnot hEq + +theorem dvd_of_localization_dvd_primeGenerated_isLocalization {α β : Type*} + [CommRing α] [IsDomain α] {S : Submonoid α} [CommRing β] [Algebra α β] [IsDomain β] + [_root_.IsLocalization S β] (hS : PrimeGenerated S) {p a : α} (hp : Irreducible p) + (havoid : Avoids S p) (hdiv : algebraMap α β p ∣ algebraMap α β a) : p ∣ a := by + letI : Fact ((0 : α) ∉ S) := ⟨zero_notMem_of_primeGenerated hS⟩ + rcases (NagataFactoriality.IsLocalization.dvd_map_iff (S := S) (β := β) (a := p) (b := a)).1 hdiv with + ⟨s, hs, hsa⟩ + rcases hsa with ⟨c, hc⟩ + rcases hS s hs with ⟨f, hf, hprod⟩ + have hnot : ∀ q ∈ f, ¬ p ∣ q := by + intro q hq hpq + have hq_dvd_prod : q ∣ f.prod := Multiset.dvd_prod hq + have hp_dvd_s : p ∣ s := by + rw [← hprod] + exact dvd_trans hpq hq_dvd_prod + exact havoid s hs hp_dvd_s + have hEq : f.prod * a = p * c := by + simpa [hprod] using hc + exact dvd_of_mul_eq_prime_factors (fun q hq => (hf q hq).2) hp hnot hEq + +theorem dvd_of_localization_dvd_primeGenerated {α : Type*} [CommRing α] [IsDomain α] + {S : Submonoid α} (hS : PrimeGenerated S) {p a : α} (hp : Irreducible p) + (havoid : Avoids S p) (hdiv : Localization.of (S := S) p ∣ Localization.of (S := S) a) : p ∣ a := by + letI : Fact ((0 : α) ∉ S) := ⟨zero_notMem_of_primeGenerated hS⟩ + letI : IsDomain (Localization S) := by infer_instance + simpa [Localization.of] using + (dvd_of_localization_dvd_primeGenerated_isLocalization + (β := Localization S) (S := S) hS hp havoid hdiv) + +theorem multiset_prod_mem_of_factors {α : Type*} [CommMonoid α] {S : Submonoid α} {f : Multiset α} + (hf : ∀ q ∈ f, q ∈ S) : f.prod ∈ S := by + revert hf + refine Multiset.induction_on f ?_ ?_ + · intro _ + simp + · intro q qs ih hqs + have hq : q ∈ S := hqs q (by simp) + have htail : ∀ r ∈ qs, r ∈ S := by + intro r hr + exact hqs r (by simp [hr]) + simpa using S.mul_mem hq (ih htail) + +theorem split_prime_factors_of_mul_eq {α : Type*} [CommRing α] [IsDomain α] + {f : Multiset α} (hf : ∀ q ∈ f, Prime q) {p a b : α} (_hp : Irreducible p) + (hEq : p * f.prod = a * b) : + ∃ f₁ f₂ : Multiset α, ∃ a' b' : α, + f₁ + f₂ = f ∧ + a = f₁.prod * a' ∧ + b = f₂.prod * b' ∧ + p = a' * b' := by + have hmain : + ∀ (g : Multiset α) (a b : α), (∀ q ∈ g, Prime q) → p * g.prod = a * b → + ∃ f₁ f₂ : Multiset α, ∃ a' b' : α, + f₁ + f₂ = g ∧ + a = f₁.prod * a' ∧ + b = f₂.prod * b' ∧ + p = a' * b' := by + intro g + refine Multiset.induction_on g ?_ ?_ + · intro a b _ hEq + refine ⟨0, 0, a, b, rfl, ?_, ?_, ?_⟩ + · simp + · simp + · simpa using hEq + · intro q qs ih a b hqs hEq + have hq : Prime q := hqs q (by simp) + have htail : ∀ r ∈ qs, Prime r := by + intro r hr + exact hqs r (by simp [hr]) + have hq_dvd_ab : q ∣ a * b := by + refine ⟨p * qs.prod, ?_⟩ + calc + a * b = p * (q * qs.prod) := by + simpa [Multiset.prod_cons, mul_assoc, mul_left_comm, mul_comm] using hEq.symm + _ = q * (p * qs.prod) := by ac_rfl + rcases hq.2.2 a b hq_dvd_ab with hqa | hqb + · rcases hqa with ⟨a₁, ha₁⟩ + have hEq' : p * qs.prod = a₁ * b := by + have haux : q * (p * qs.prod) = q * (a₁ * b) := by + calc + q * (p * qs.prod) = p * (q * qs.prod) := by ac_rfl + _ = a * b := by + simpa [Multiset.prod_cons, mul_assoc, mul_left_comm, mul_comm] using hEq + _ = (q * a₁) * b := by rw [ha₁] + _ = q * (a₁ * b) := by ac_rfl + exact mul_left_cancel₀ hq.ne_zero haux + rcases ih (a := a₁) (b := b) htail hEq' with ⟨f₁, f₂, a', b', hpart, ha, hb, hpab⟩ + refine ⟨q ::ₘ f₁, f₂, a', b', ?_, ?_, hb, hpab⟩ + · simp [hpart] + · calc + a = q * a₁ := ha₁ + _ = q * (f₁.prod * a') := by rw [ha] + _ = (q ::ₘ f₁).prod * a' := by simp [mul_assoc] + · rcases hqb with ⟨b₁, hb₁⟩ + have hEq' : p * qs.prod = a * b₁ := by + have haux : q * (p * qs.prod) = q * (a * b₁) := by + calc + q * (p * qs.prod) = p * (q * qs.prod) := by ac_rfl + _ = a * b := by + simpa [Multiset.prod_cons, mul_assoc, mul_left_comm, mul_comm] using hEq + _ = a * (q * b₁) := by rw [hb₁] + _ = q * (a * b₁) := by ac_rfl + exact mul_left_cancel₀ hq.ne_zero haux + rcases ih (a := a) (b := b₁) htail hEq' with ⟨f₁, f₂, a', b', hpart, ha, hb, hpab⟩ + refine ⟨f₁, q ::ₘ f₂, a', b', ?_, ha, ?_, hpab⟩ + · simp [hpart] + · calc + b = q * b₁ := hb₁ + _ = q * (f₂.prod * b') := by rw [hb] + _ = (q ::ₘ f₂).prod * b' := by simp [mul_assoc] + exact hmain f a b hf hEq + +theorem localization_irreducible_of_irreducible_primeGenerated_isLocalization {α β : Type*} + [CommRing α] [IsDomain α] {S : Submonoid α} [CommRing β] [Algebra α β] [IsDomain β] + [_root_.IsLocalization S β] (hS : PrimeGenerated S) {p : α} (hp : Irreducible p) + (havoid : Avoids S p) : Irreducible (algebraMap α β p) := by + letI : Fact ((0 : α) ∉ S) := ⟨zero_notMem_of_primeGenerated hS⟩ + refine ⟨?_, ?_⟩ + · intro hunit + have hdiv : algebraMap α β p ∣ (1 : β) := by + rcases isUnit_iff_exists_inv.mp hunit with ⟨x, hx⟩ + exact ⟨x, hx.symm⟩ + have hdiv' : algebraMap α β p ∣ algebraMap α β (1 : α) := by + simpa using hdiv + rcases (NagataFactoriality.IsLocalization.dvd_map_iff + (S := S) (β := β) (a := p) (b := 1)).1 hdiv' with ⟨s, hs, hps⟩ + exact havoid s hs (by simpa using hps) + · intro x y hxy + obtain ⟨a, s, hs, rfl⟩ := NagataFactoriality.IsLocalization.surj (S := S) (β := β) x + obtain ⟨b, t, ht, rfl⟩ := NagataFactoriality.IsLocalization.surj (S := S) (β := β) y + have hEq : + p * (s * t) = a * b := by + have hloc : + algebraMap α β p = + _root_.IsLocalization.mk' β (a * b) ⟨s * t, S.mul_mem hs ht⟩ := by + calc + algebraMap α β p = + _root_.IsLocalization.mk' β a ⟨s, hs⟩ * _root_.IsLocalization.mk' β b ⟨t, ht⟩ := hxy + _ = _root_.IsLocalization.mk' β (a * b) ⟨s * t, S.mul_mem hs ht⟩ := by + simpa using (_root_.IsLocalization.mk'_mul + (M := S) (S := β) a b ⟨s, hs⟩ ⟨t, ht⟩).symm + have hmk : + _root_.IsLocalization.mk' β p ⟨1, S.one_mem⟩ = + _root_.IsLocalization.mk' β (a * b) ⟨s * t, S.mul_mem hs ht⟩ := by + calc + _root_.IsLocalization.mk' β p ⟨1, S.one_mem⟩ = algebraMap α β p := by + simpa using (_root_.IsLocalization.mk'_one (S := β) p) + _ = _root_.IsLocalization.mk' β (a * b) ⟨s * t, S.mul_mem hs ht⟩ := hloc + simpa [mul_one] using + (NagataFactoriality.IsLocalization.mk'_eq_iff + (S := S) (β := β) (a := p) (b := a * b) + (s := 1) (t := s * t) S.one_mem (S.mul_mem hs ht)).1 hmk + rcases hS (s * t) (S.mul_mem hs ht) with ⟨f, hf, hfprod⟩ + rcases split_prime_factors_of_mul_eq (fun q hq => (hf q hq).2) hp (by simpa [hfprod] using hEq) + with ⟨f₁, f₂, a', b', hpart, ha, hb, hpab⟩ + rcases hp.isUnit_or_isUnit hpab with haUnit | hbUnit + · left + have hf₁mem : ∀ q ∈ f₁, q ∈ S := by + intro q hq + exact (hf q (by rw [← hpart]; exact Multiset.mem_add.mpr (Or.inl hq))).1 + have hprodMem : f₁.prod ∈ S := multiset_prod_mem_of_factors hf₁mem + have hx_eq : + _root_.IsLocalization.mk' β a ⟨s, hs⟩ = + algebraMap α β f₁.prod * _root_.IsLocalization.mk' β a' ⟨s, hs⟩ := by + rw [ha] + symm + exact NagataFactoriality.IsLocalization.map_mul_mk' (S := S) (β := β) f₁.prod a' s hs + rw [hx_eq] + exact isUnit_mul + (NagataFactoriality.IsLocalization.isUnit_map_of_mem (S := S) (β := β) hprodMem) + (NagataFactoriality.IsLocalization.isUnit_mk'_of_isUnit (S := S) (β := β) haUnit hs) + · right + have hf₂mem : ∀ q ∈ f₂, q ∈ S := by + intro q hq + exact (hf q (by rw [← hpart]; exact Multiset.mem_add.mpr (Or.inr hq))).1 + have hprodMem : f₂.prod ∈ S := multiset_prod_mem_of_factors hf₂mem + have hy_eq : + _root_.IsLocalization.mk' β b ⟨t, ht⟩ = + algebraMap α β f₂.prod * _root_.IsLocalization.mk' β b' ⟨t, ht⟩ := by + rw [hb] + symm + exact NagataFactoriality.IsLocalization.map_mul_mk' (S := S) (β := β) f₂.prod b' t ht + rw [hy_eq] + exact isUnit_mul + (NagataFactoriality.IsLocalization.isUnit_map_of_mem (S := S) (β := β) hprodMem) + (NagataFactoriality.IsLocalization.isUnit_mk'_of_isUnit (S := S) (β := β) hbUnit ht) + +theorem localization_irreducible_of_irreducible_primeGenerated {α : Type*} + [CommRing α] [IsDomain α] {S : Submonoid α} (hS : PrimeGenerated S) {p : α} + (hp : Irreducible p) (havoid : Avoids S p) : Irreducible (Localization.of (S := S) p) := by + letI : Fact ((0 : α) ∉ S) := ⟨zero_notMem_of_primeGenerated hS⟩ + letI : IsDomain (Localization S) := by infer_instance + simpa [Localization.of] using + (localization_irreducible_of_irreducible_primeGenerated_isLocalization + (β := Localization S) (S := S) hS hp havoid) + +theorem prime_of_localization_prime_primeGenerated_isLocalization {α β : Type*} + [CommRing α] [IsDomain α] {S : Submonoid α} [CommRing β] [Algebra α β] [IsDomain β] + [_root_.IsLocalization S β] (hS : PrimeGenerated S) {p : α} (hp : Irreducible p) + (havoid : Avoids S p) (hploc : Prime (algebraMap α β p)) : Prime p := by + letI : Fact ((0 : α) ∉ S) := ⟨zero_notMem_of_primeGenerated hS⟩ + refine ⟨hp.ne_zero, hp.not_isUnit, ?_⟩ + intro a b hdiv + have hlocdiv : algebraMap α β p ∣ algebraMap α β (a * b) := by + rcases hdiv with ⟨c, hc⟩ + exact ⟨algebraMap α β c, by simp [map_mul, hc]⟩ + rcases hploc.2.2 (algebraMap α β a) (algebraMap α β b) + (by simpa [map_mul] using hlocdiv) with hpa | hpb + · left + exact dvd_of_localization_dvd_primeGenerated_isLocalization + (β := β) (S := S) hS hp havoid hpa + · right + exact dvd_of_localization_dvd_primeGenerated_isLocalization + (β := β) (S := S) hS hp havoid hpb + +theorem prime_of_localization_prime_primeGenerated {α : Type*} [CommRing α] [IsDomain α] + {S : Submonoid α} (hS : PrimeGenerated S) {p : α} (hp : Irreducible p) + (havoid : Avoids S p) (hploc : Prime (Localization.of (S := S) p)) : Prime p := by + letI : Fact ((0 : α) ∉ S) := ⟨zero_notMem_of_primeGenerated hS⟩ + letI : IsDomain (Localization S) := by infer_instance + simpa [Localization.of] using + (prime_of_localization_prime_primeGenerated_isLocalization + (β := Localization S) (S := S) hS hp havoid hploc) + +theorem nagata_key_lemma_primeGenerated_isLocalization {α β : Type*} + [CommRing α] [IsDomain α] {S : Submonoid α} [CommRing β] [Algebra α β] [IsDomain β] + [_root_.IsLocalization S β] (hS : PrimeGenerated S) [UniqueFactorizationMonoid β] + {p : α} (hp : Irreducible p) : Prime p := by + letI : Fact ((0 : α) ∉ S) := ⟨zero_notMem_of_primeGenerated hS⟩ + by_cases hmem : ∃ s : α, s ∈ S ∧ p ∣ s + · rcases hmem with ⟨s, hs, hdiv⟩ + exact prime_of_irreducible_of_dvd_mem_primeGenerated hS hp hs hdiv + · have havoid : Avoids S p := by + intro s hs hdiv + exact hmem ⟨s, hs, hdiv⟩ + have hlocIrred : Irreducible (algebraMap α β p) := + localization_irreducible_of_irreducible_primeGenerated_isLocalization + (β := β) (S := S) hS hp havoid + have hlocPrime : Prime (algebraMap α β p) := + (UniqueFactorizationMonoid.irreducible_iff_prime).mp hlocIrred + exact prime_of_localization_prime_primeGenerated_isLocalization + (β := β) (S := S) hS hp havoid hlocPrime + +theorem nagata_key_lemma_primeGenerated {α : Type*} [CommRing α] [IsDomain α] {S : Submonoid α} + (hS : PrimeGenerated S) + (hUFD : + @UniqueFactorizationMonoid (Localization S) + (by + letI : Fact ((0 : α) ∉ S) := ⟨zero_notMem_of_primeGenerated hS⟩ + infer_instance)) + {p : α} (hp : Irreducible p) : Prime p := by + letI : Fact ((0 : α) ∉ S) := ⟨zero_notMem_of_primeGenerated hS⟩ + letI : IsDomain (Localization S) := by infer_instance + letI : UniqueFactorizationMonoid (Localization S) := hUFD + simpa [Localization.of] using + (nagata_key_lemma_primeGenerated_isLocalization + (β := Localization S) (S := S) hS hp) + +theorem prime_of_irreducible_of_dvd_mem {α : Type*} [CommRing α] [IsDomain α] {S : Submonoid α} + (hS : ∀ s ∈ S, Prime s ∨ IsUnit s) {p s : α} + (hp : Irreducible p) (hs : s ∈ S) (hdiv : p ∣ s) : Prime p := by + rcases hS s hs with hsPrime | hsUnit + · have hsIrred : Irreducible s := prime_irreducible hsPrime + have hassoc : Associated p s := associated_of_irreducible_of_dvd hp hsIrred hdiv + exact prime_of_associated hsPrime (associated_symm hassoc) + · exact False.elim (hp.not_isUnit (isUnit_of_dvd_unit hdiv hsUnit)) + +theorem localization_irreducible_of_irreducible_isLocalization {α β : Type*} + [CommRing α] [IsDomain α] {S : Submonoid α} [CommRing β] [Algebra α β] [IsDomain β] + [_root_.IsLocalization S β] (hS : ∀ s ∈ S, Prime s ∨ IsUnit s) {p : α} + (hp : Irreducible p) (havoid : Avoids S p) : Irreducible (algebraMap α β p) := by + letI : Fact ((0 : α) ∉ S) := submonoidZeroNotMemFact hS + refine ⟨?_, ?_⟩ + · intro hunit + have hdiv : algebraMap α β p ∣ (1 : β) := by + rcases isUnit_iff_exists_inv.mp hunit with ⟨x, hx⟩ + exact ⟨x, hx.symm⟩ + have hdiv' : algebraMap α β p ∣ algebraMap α β (1 : α) := by + simpa using hdiv + rcases (NagataFactoriality.IsLocalization.dvd_map_iff + (S := S) (β := β) (a := p) (b := 1)).1 hdiv' with ⟨s, hs, hps⟩ + exact havoid s hs (by simpa using hps) + · intro x y hxy + obtain ⟨a, s, hs, rfl⟩ := NagataFactoriality.IsLocalization.surj (S := S) (β := β) x + obtain ⟨b, t, ht, rfl⟩ := NagataFactoriality.IsLocalization.surj (S := S) (β := β) y + have hprod : p * (s * t) = a * b := by + have hEq : + algebraMap α β p = + _root_.IsLocalization.mk' β (a * b) ⟨s * t, S.mul_mem hs ht⟩ := by + calc + algebraMap α β p = + _root_.IsLocalization.mk' β a ⟨s, hs⟩ * _root_.IsLocalization.mk' β b ⟨t, ht⟩ := hxy + _ = _root_.IsLocalization.mk' β (a * b) ⟨s * t, S.mul_mem hs ht⟩ := by + simpa using (_root_.IsLocalization.mk'_mul + (M := S) (S := β) a b ⟨s, hs⟩ ⟨t, ht⟩).symm + have hEq' : + _root_.IsLocalization.mk' β p ⟨1, S.one_mem⟩ = + _root_.IsLocalization.mk' β (a * b) ⟨s * t, S.mul_mem hs ht⟩ := by + calc + _root_.IsLocalization.mk' β p ⟨1, S.one_mem⟩ = algebraMap α β p := by + simpa using (_root_.IsLocalization.mk'_one (S := β) p) + _ = _root_.IsLocalization.mk' β (a * b) ⟨s * t, S.mul_mem hs ht⟩ := hEq + simpa [mul_one] using + (NagataFactoriality.IsLocalization.mk'_eq_iff + (S := S) (β := β) (a := p) (b := a * b) + (s := 1) (t := s * t) S.one_mem (S.mul_mem hs ht)).1 hEq' + rcases hS (s * t) (S.mul_mem hs ht) with hstPrime | hstUnit + · have hstdiv : s * t ∣ a * b := by + refine ⟨p, ?_⟩ + calc + a * b = p * (s * t) := hprod.symm + _ = (s * t) * p := by ac_rfl + rcases hstPrime.2.2 a b hstdiv with hdiva | hdivb + · rcases hdiva with ⟨d, hd⟩ + have hst0 : s * t ≠ 0 := hstPrime.ne_zero + have hp_eq : p = d * b := by + apply mul_left_cancel₀ hst0 + calc + (s * t) * p = p * (s * t) := by ac_rfl + _ = a * b := hprod + _ = ((s * t) * d) * b := by rw [hd] + _ = (s * t) * (d * b) := by ac_rfl + rcases hp.isUnit_or_isUnit hp_eq with hdUnit | hbUnit + · left + have hx_eq_mk : + _root_.IsLocalization.mk' β a ⟨s, hs⟩ = + _root_.IsLocalization.mk' β (t * d) ⟨1, S.one_mem⟩ := by + apply (NagataFactoriality.IsLocalization.mk'_eq_iff + (S := S) (β := β) (a := a) (b := t * d) + (s := s) (t := 1) hs S.one_mem).2 + calc + a * 1 = a := by simp + _ = s * t * d := by rw [hd] + _ = (t * d) * s := by ac_rfl + have hx_eq : _root_.IsLocalization.mk' β a ⟨s, hs⟩ = algebraMap α β (t * d) := by + calc + _root_.IsLocalization.mk' β a ⟨s, hs⟩ = + _root_.IsLocalization.mk' β (t * d) ⟨1, S.one_mem⟩ := hx_eq_mk + _ = algebraMap α β (t * d) := by + simpa using (_root_.IsLocalization.mk'_one (S := β) (t * d)) + rw [hx_eq] + have htUnitLoc : IsUnit (algebraMap α β t) := + NagataFactoriality.IsLocalization.isUnit_map_of_mem (S := S) (β := β) ht + have hdUnitLoc : IsUnit (algebraMap α β d) := + NagataFactoriality.IsLocalization.isUnit_map_of_isUnit (β := β) hdUnit + simpa [map_mul] using isUnit_mul htUnitLoc hdUnitLoc + · right + exact NagataFactoriality.IsLocalization.isUnit_mk'_of_isUnit + (S := S) (β := β) hbUnit ht + · rcases hdivb with ⟨d, hd⟩ + have hst0 : s * t ≠ 0 := hstPrime.ne_zero + have hp_eq : p = a * d := by + apply mul_left_cancel₀ hst0 + calc + (s * t) * p = p * (s * t) := by ac_rfl + _ = a * b := hprod + _ = a * ((s * t) * d) := by rw [hd] + _ = (s * t) * (a * d) := by ac_rfl + rcases hp.isUnit_or_isUnit hp_eq with haUnit | hdUnit + · left + exact NagataFactoriality.IsLocalization.isUnit_mk'_of_isUnit + (S := S) (β := β) haUnit hs + · right + have hy_eq_mk : + _root_.IsLocalization.mk' β b ⟨t, ht⟩ = + _root_.IsLocalization.mk' β (s * d) ⟨1, S.one_mem⟩ := by + apply (NagataFactoriality.IsLocalization.mk'_eq_iff + (S := S) (β := β) (a := b) (b := s * d) + (s := t) (t := 1) ht S.one_mem).2 + calc + b * 1 = b := by simp + _ = s * t * d := by rw [hd] + _ = (s * d) * t := by ac_rfl + have hy_eq : _root_.IsLocalization.mk' β b ⟨t, ht⟩ = algebraMap α β (s * d) := by + calc + _root_.IsLocalization.mk' β b ⟨t, ht⟩ = + _root_.IsLocalization.mk' β (s * d) ⟨1, S.one_mem⟩ := hy_eq_mk + _ = algebraMap α β (s * d) := by + simpa using (_root_.IsLocalization.mk'_one (S := β) (s * d)) + rw [hy_eq] + have hsUnitLoc : IsUnit (algebraMap α β s) := + NagataFactoriality.IsLocalization.isUnit_map_of_mem (S := S) (β := β) hs + have hdUnitLoc : IsUnit (algebraMap α β d) := + NagataFactoriality.IsLocalization.isUnit_map_of_isUnit (β := β) hdUnit + simpa [map_mul] using isUnit_mul hsUnitLoc hdUnitLoc + · have hassoc : Associated p (a * b) := by + simpa [hprod] using associated_mul_unit_right p (s * t) hstUnit + have habIrred : Irreducible (a * b) := hassoc.irreducible hp + exact (habIrred.isUnit_or_isUnit rfl).elim + (fun haUnit => Or.inl <| + NagataFactoriality.IsLocalization.isUnit_mk'_of_isUnit (S := S) (β := β) haUnit hs) + (fun hbUnit => Or.inr <| + NagataFactoriality.IsLocalization.isUnit_mk'_of_isUnit (S := S) (β := β) hbUnit ht) + +theorem localization_irreducible_of_irreducible {α : Type*} [CommRing α] [IsDomain α] + {S : Submonoid α} (hS : ∀ s ∈ S, Prime s ∨ IsUnit s) {p : α} (hp : Irreducible p) + (havoid : Avoids S p) : Irreducible (Localization.of (S := S) p) := by + letI : Fact ((0 : α) ∉ S) := submonoidZeroNotMemFact hS + letI : IsDomain (Localization S) := by infer_instance + simpa [Localization.of] using + (localization_irreducible_of_irreducible_isLocalization + (β := Localization S) (S := S) hS hp havoid) + +theorem dvd_of_localization_dvd_isLocalization {α β : Type*} + [CommRing α] [IsDomain α] {S : Submonoid α} [CommRing β] [Algebra α β] [IsDomain β] + [_root_.IsLocalization S β] (hS : ∀ s ∈ S, Prime s ∨ IsUnit s) {p a : α} + (hp : Irreducible p) (havoid : Avoids S p) (hdiv : algebraMap α β p ∣ algebraMap α β a) : + p ∣ a := by + letI : Fact ((0 : α) ∉ S) := submonoidZeroNotMemFact hS + rcases (NagataFactoriality.IsLocalization.dvd_map_iff + (S := S) (β := β) (a := p) (b := a)).1 hdiv with ⟨s, hs, hsa⟩ + rcases hsa with ⟨c, hc⟩ + rcases hS s hs with hsPrime | hsUnit + · have hsdiv : s ∣ p * c := ⟨a, hc.symm⟩ + rcases hsPrime.2.2 p c hsdiv with hsp | hsc + · have hsIrred : Irreducible s := prime_irreducible hsPrime + have hassoc : Associated s p := associated_of_irreducible_of_dvd hsIrred hp hsp + exact False.elim (havoid s hs (dvd_of_associated (associated_symm hassoc))) + · rcases hsc with ⟨d, hd⟩ + refine ⟨d, ?_⟩ + have hs0 : s ≠ 0 := hsPrime.ne_zero + have hcancel : s * a = s * (p * d) := by + calc + s * a = p * c := hc + _ = p * (s * d) := by rw [hd] + _ = s * (p * d) := by ac_rfl + exact mul_left_cancel₀ hs0 hcancel + · rcases hsUnit with ⟨u, rfl⟩ + refine ⟨(↑u⁻¹ : α) * c, ?_⟩ + calc + a = (↑u⁻¹ : α) * ((u : α) * a) := by simp + _ = (↑u⁻¹ : α) * (p * c) := by rw [hc] + _ = p * ((↑u⁻¹ : α) * c) := by ac_rfl + +theorem dvd_of_localization_dvd {α : Type*} [CommRing α] [IsDomain α] {S : Submonoid α} + (hS : ∀ s ∈ S, Prime s ∨ IsUnit s) {p a : α} (hp : Irreducible p) (havoid : Avoids S p) + (hdiv : Localization.of (S := S) p ∣ Localization.of (S := S) a) : p ∣ a := by + letI : Fact ((0 : α) ∉ S) := submonoidZeroNotMemFact hS + letI : IsDomain (Localization S) := by infer_instance + simpa [Localization.of] using + (dvd_of_localization_dvd_isLocalization + (β := Localization S) (S := S) hS hp havoid hdiv) + +theorem prime_of_localization_prime_isLocalization {α β : Type*} + [CommRing α] [IsDomain α] {S : Submonoid α} [CommRing β] [Algebra α β] [IsDomain β] + [_root_.IsLocalization S β] (hS : ∀ s ∈ S, Prime s ∨ IsUnit s) {p : α} + (hp : Irreducible p) (havoid : Avoids S p) (hploc : Prime (algebraMap α β p)) : Prime p := by + letI : Fact ((0 : α) ∉ S) := submonoidZeroNotMemFact hS + refine ⟨hp.ne_zero, hp.not_isUnit, ?_⟩ + intro a b hdiv + have hlocdiv : algebraMap α β p ∣ algebraMap α β (a * b) := by + rcases hdiv with ⟨c, hc⟩ + exact ⟨algebraMap α β c, by simp [map_mul, hc]⟩ + rcases hploc.2.2 (algebraMap α β a) (algebraMap α β b) + (by simpa [map_mul] using hlocdiv) with hpa | hpb + · left + exact dvd_of_localization_dvd_isLocalization (β := β) (S := S) hS hp havoid hpa + · right + exact dvd_of_localization_dvd_isLocalization (β := β) (S := S) hS hp havoid hpb + +theorem prime_of_localization_prime {α : Type*} [CommRing α] [IsDomain α] {S : Submonoid α} + (hS : ∀ s ∈ S, Prime s ∨ IsUnit s) {p : α} (hp : Irreducible p) (havoid : Avoids S p) + (hploc : Prime (Localization.of (S := S) p)) : Prime p := by + letI : Fact ((0 : α) ∉ S) := submonoidZeroNotMemFact hS + letI : IsDomain (Localization S) := by infer_instance + simpa [Localization.of] using + (prime_of_localization_prime_isLocalization + (β := Localization S) (S := S) hS hp havoid hploc) + +theorem nagata_key_lemma_isLocalization {α β : Type*} + [CommRing α] [IsDomain α] {S : Submonoid α} [CommRing β] [Algebra α β] [IsDomain β] + [_root_.IsLocalization S β] (hS : ∀ s ∈ S, Prime s ∨ IsUnit s) + [UniqueFactorizationMonoid β] {p : α} (hp : Irreducible p) : Prime p := by + letI : Fact ((0 : α) ∉ S) := submonoidZeroNotMemFact hS + by_cases hmem : ∃ s : α, s ∈ S ∧ p ∣ s + · rcases hmem with ⟨s, hs, hdiv⟩ + exact prime_of_irreducible_of_dvd_mem hS hp hs hdiv + · have havoid : Avoids S p := by + intro s hs hdiv + exact hmem ⟨s, hs, hdiv⟩ + have hlocIrred : Irreducible (algebraMap α β p) := + localization_irreducible_of_irreducible_isLocalization + (β := β) (S := S) hS hp havoid + have hlocPrime : Prime (algebraMap α β p) := + (UniqueFactorizationMonoid.irreducible_iff_prime).mp hlocIrred + exact prime_of_localization_prime_isLocalization + (β := β) (S := S) hS hp havoid hlocPrime + +theorem nagata_key_lemma {α : Type*} [CommRing α] [IsDomain α] {S : Submonoid α} + (hS : ∀ s ∈ S, Prime s ∨ IsUnit s) + (hUFD : + @UniqueFactorizationMonoid (Localization S) + (by + letI : Fact ((0 : α) ∉ S) := submonoidZeroNotMemFact hS + infer_instance)) + {p : α} (hp : Irreducible p) : Prime p := by + letI : Fact ((0 : α) ∉ S) := submonoidZeroNotMemFact hS + letI : IsDomain (Localization S) := by infer_instance + letI : UniqueFactorizationMonoid (Localization S) := hUFD + simpa [Localization.of] using + (nagata_key_lemma_isLocalization + (β := Localization S) (S := S) hS hp) + +end NagataFactoriality diff --git a/LeanPool/NagataFactoriality/NagataFactoriality/Nagata/Theorem.lean b/LeanPool/NagataFactoriality/NagataFactoriality/Nagata/Theorem.lean new file mode 100644 index 0000000000..84c8b212a8 --- /dev/null +++ b/LeanPool/NagataFactoriality/NagataFactoriality/Nagata/Theorem.lean @@ -0,0 +1,105 @@ +/- +Copyright (c) 2026 Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina G. de Oliveira. 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 +-/ +import LeanPool.NagataFactoriality.NagataFactoriality.Nagata.Lemmas + +namespace NagataFactoriality + +theorem nagata_theorem {R : Type*} [CommRing R] [IsDomain R] [IsNoetherianRing R] + (S : Submonoid R) (hS : PrimeGenerated S) + (hUFD : + @UniqueFactorizationMonoid (Localization S) + (by + letI : Fact ((0 : R) ∉ S) := ⟨zero_notMem_of_primeGenerated hS⟩ + infer_instance)) : + UniqueFactorizationMonoid R := by + letI : Fact ((0 : R) ∉ S) := ⟨zero_notMem_of_primeGenerated hS⟩ + letI : UniqueFactorizationMonoid (Localization S) := hUFD + exact ufd_of_factorization_and_primes + (hasFactorization_of_noetherian (α := R)) + (fun p hp => nagata_key_lemma_primeGenerated_isLocalization + (S := S) (β := Localization S) hS hp) + +theorem nagata_theorem_isLocalization {R T : Type*} [CommRing R] [IsDomain R] [IsNoetherianRing R] + (S : Submonoid R) [CommRing T] [Algebra R T] [_root_.IsLocalization S T] + [IsDomain T] (hS : PrimeGenerated S) (hUFD : UniqueFactorizationMonoid T) : + UniqueFactorizationMonoid R := by + letI : UniqueFactorizationMonoid T := hUFD + exact ufd_of_factorization_and_primes + (hasFactorization_of_noetherian (α := R)) + (fun p hp => nagata_key_lemma_primeGenerated_isLocalization (S := S) (β := T) hS hp) + +theorem nagata_theorem_of_prime_generators {R : Type*} [CommRing R] [IsDomain R] + [IsNoetherianRing R] (s : Set R) (hs : ∀ q ∈ s, Prime q) + (hUFD : + @UniqueFactorizationMonoid (Localization (Submonoid.closure s)) + (by + let hS : PrimeGenerated (Submonoid.closure s) := primeGenerated_closure_of_primes hs + letI : Fact ((0 : R) ∉ Submonoid.closure s) := ⟨zero_notMem_of_primeGenerated hS⟩ + infer_instance)) : + UniqueFactorizationMonoid R := by + exact nagata_theorem (R := R) (Submonoid.closure s) (primeGenerated_closure_of_primes hs) hUFD + +theorem nagata_theorem_of_prime_generators_isLocalization {R T : Type*} [CommRing R] [IsDomain R] + [IsNoetherianRing R] (s : Set R) [CommRing T] [Algebra R T] + [_root_.IsLocalization (Submonoid.closure s) T] [IsDomain T] + (hs : ∀ q ∈ s, Prime q) (hUFD : UniqueFactorizationMonoid T) : + UniqueFactorizationMonoid R := by + exact nagata_theorem_isLocalization (R := R) (T := T) (Submonoid.closure s) + (primeGenerated_closure_of_primes hs) hUFD + +theorem nagata_theorem_of_finite_prime_generators {R : Type*} [CommRing R] [IsDomain R] + [IsNoetherianRing R] (s : Finset R) (hs : ∀ q ∈ s, Prime q) + (hUFD : + @UniqueFactorizationMonoid (Localization (Submonoid.closure (↑s : Set R))) + (by + let hS : PrimeGenerated (Submonoid.closure (↑s : Set R)) := + primeGenerated_closure_finset_of_primes s hs + letI : Fact ((0 : R) ∉ Submonoid.closure (↑s : Set R)) := + ⟨zero_notMem_of_primeGenerated hS⟩ + infer_instance)) : + UniqueFactorizationMonoid R := by + exact nagata_theorem_of_prime_generators (R := R) (s := (↑s : Set R)) (fun q hq => hs q hq) hUFD + +theorem nagata_theorem_of_finite_prime_generators_isLocalization {R T : Type*} + [CommRing R] [IsDomain R] [IsNoetherianRing R] (s : Finset R) [CommRing T] [Algebra R T] + [_root_.IsLocalization (Submonoid.closure (↑s : Set R)) T] [IsDomain T] + (hs : ∀ q ∈ s, Prime q) (hUFD : UniqueFactorizationMonoid T) : + UniqueFactorizationMonoid R := by + exact nagata_theorem_of_prime_generators_isLocalization (R := R) (T := T) (s := (↑s : Set R)) + (fun q hq => hs q hq) hUFD + +theorem nagata_theorem_of_prime_or_unit {R : Type*} [CommRing R] [IsDomain R] [IsNoetherianRing R] + (S : Submonoid R) (hS : ∀ s ∈ S, Prime s ∨ IsUnit s) + (hUFD : + @UniqueFactorizationMonoid (Localization S) + (by + letI : Fact ((0 : R) ∉ S) := ⟨Submonoid.zero_notMem_of_prime_or_unit hS⟩ + infer_instance)) : + UniqueFactorizationMonoid R := by + letI : Fact ((0 : R) ∉ S) := ⟨Submonoid.zero_notMem_of_prime_or_unit hS⟩ + letI : UniqueFactorizationMonoid (Localization S) := hUFD + exact ufd_of_factorization_and_primes + (hasFactorization_of_noetherian (α := R)) + (fun p hp => nagata_key_lemma_isLocalization + (S := S) (β := Localization S) hS hp) + +theorem nagata_theorem_of_prime_or_unit_isLocalization {R T : Type*} + [CommRing R] [IsDomain R] [IsNoetherianRing R] (S : Submonoid R) [CommRing T] [Algebra R T] + [_root_.IsLocalization S T] [IsDomain T] + (hS : ∀ s ∈ S, Prime s ∨ IsUnit s) (hUFD : UniqueFactorizationMonoid T) : + UniqueFactorizationMonoid R := by + letI : UniqueFactorizationMonoid T := hUFD + exact ufd_of_factorization_and_primes + (hasFactorization_of_noetherian (α := R)) + (fun p hp => nagata_key_lemma_isLocalization (S := S) (β := T) hS hp) + +theorem ufd_of_factorization_and_prime_irreducibles {α : Type*} [CommRing α] [IsDomain α] + (hfac : WfDvdMonoid α) + (hprime : ∀ p : α, Irreducible p → Prime p) : + UniqueFactorizationMonoid α := + ufd_of_factorization_and_primes hfac hprime + +end NagataFactoriality diff --git a/LeanPool/projects.yml b/LeanPool/projects.yml index 95e0c8ad83..21ab5d6937 100644 --- a/LeanPool/projects.yml +++ b/LeanPool/projects.yml @@ -9966,3 +9966,30 @@ projects: msc: - '90C35' - '05C21' + - slug: nagatafactoriality + title: Nagata's prime-generated factoriality theorem + summary: Nagata’s factoriality criterion for noetherian domains localized at prime-generated + multiplicative sets, with concrete and abstract localization interfaces and applications + to polynomial rings through Laurent and fraction-field localizations. + branch: commutative algebra + entry_module: LeanPool.NagataFactoriality + authors: + - Arthur F. Ramos + - Ruy J. G. B. de Queiroz + - Anjolina G. de Oliveira + source: + url: https://github.com/arthur742ramos/nagatafactoriality + github_repo: arthur742ramos/nagatafactoriality + commit: 2efdf7f86085972bd758449ca43c76a2e7bdf4af + license: Apache-2.0 + status: verified + main_declarations: + - NagataFactoriality.nagata_theorem + main_results: + - declaration: NagataFactoriality.nagata_theorem + informal: A noetherian integral domain is a unique factorization domain when localization + at a prime-generated multiplicative set is a unique factorization domain. + tags: + - commutative-algebra + msc: + - 13F15 From 9fd98808e22d46347e4b9206ee4c576a6c87a001 Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Mon, 21 Sep 2026 18:21:02 +0000 Subject: [PATCH 2/8] Advance nagatafactoriality port to Lean 4.34 --- LeanPool.lean | 19 ++++ LeanPool/NagataFactoriality.lean | 2 +- .../NagataFactoriality.lean | 8 +- .../NagataFactoriality/Applications.lean | 8 +- .../Applications/Examples.lean | 8 +- .../Applications/FractionField.lean | 15 +-- .../Applications/Gauss.lean | 14 ++- .../Applications/Laurent.lean | 24 +++-- .../NagataFactoriality/Basic.lean | 8 +- .../Basic/Divisibility.lean | 13 ++- .../NagataFactoriality/Basic/Noetherian.lean | 10 +- .../NagataFactoriality/Basic/Ring.lean | 12 ++- .../NagataFactoriality/Basic/UFD.lean | 22 +++-- .../NagataFactoriality/Localization.lean | 8 +- .../Localization/IsLocalization.lean | 20 ++-- .../Localization/Localization.lean | 18 +++- .../Localization/MultSet.lean | 8 +- .../Localization/Properties.lean | 8 +- .../NagataFactoriality/Nagata.lean | 8 +- .../NagataFactoriality/Nagata/Lemmas.lean | 94 ++++++++++--------- .../NagataFactoriality/Nagata/Theorem.lean | 28 +++--- 21 files changed, 250 insertions(+), 105 deletions(-) diff --git a/LeanPool.lean b/LeanPool.lean index aaa4dc75ac..9bb6a151f6 100644 --- a/LeanPool.lean +++ b/LeanPool.lean @@ -3841,6 +3841,25 @@ import LeanPool.MoserLatticeColorings.Basic import LeanPool.MoserLatticeColorings.Ring import LeanPool.MulticolorTriangleRamsey import LeanPool.NagataFactoriality +import LeanPool.NagataFactoriality.NagataFactoriality +import LeanPool.NagataFactoriality.NagataFactoriality.Applications +import LeanPool.NagataFactoriality.NagataFactoriality.Applications.Examples +import LeanPool.NagataFactoriality.NagataFactoriality.Applications.FractionField +import LeanPool.NagataFactoriality.NagataFactoriality.Applications.Gauss +import LeanPool.NagataFactoriality.NagataFactoriality.Applications.Laurent +import LeanPool.NagataFactoriality.NagataFactoriality.Basic +import LeanPool.NagataFactoriality.NagataFactoriality.Basic.Divisibility +import LeanPool.NagataFactoriality.NagataFactoriality.Basic.Noetherian +import LeanPool.NagataFactoriality.NagataFactoriality.Basic.Ring +import LeanPool.NagataFactoriality.NagataFactoriality.Basic.UFD +import LeanPool.NagataFactoriality.NagataFactoriality.Localization +import LeanPool.NagataFactoriality.NagataFactoriality.Localization.IsLocalization +import LeanPool.NagataFactoriality.NagataFactoriality.Localization.Localization +import LeanPool.NagataFactoriality.NagataFactoriality.Localization.MultSet +import LeanPool.NagataFactoriality.NagataFactoriality.Localization.Properties +import LeanPool.NagataFactoriality.NagataFactoriality.Nagata +import LeanPool.NagataFactoriality.NagataFactoriality.Nagata.Lemmas +import LeanPool.NagataFactoriality.NagataFactoriality.Nagata.Theorem import LeanPool.NashWilliams import LeanPool.NashWilliams.Combinatorics import LeanPool.NashWilliams.Combinatorics.Front diff --git a/LeanPool/NagataFactoriality.lean b/LeanPool/NagataFactoriality.lean index a772ae3ab3..3e2dde0f4c 100644 --- a/LeanPool/NagataFactoriality.lean +++ b/LeanPool/NagataFactoriality.lean @@ -1,5 +1,5 @@ /- -Copyright (c) 2026 Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina G. de Oliveira. All rights reserved. +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 -/ diff --git a/LeanPool/NagataFactoriality/NagataFactoriality.lean b/LeanPool/NagataFactoriality/NagataFactoriality.lean index 226c0d665f..6b6cda70ec 100644 --- a/LeanPool/NagataFactoriality/NagataFactoriality.lean +++ b/LeanPool/NagataFactoriality/NagataFactoriality.lean @@ -1,5 +1,5 @@ /- -Copyright (c) 2026 Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina G. de Oliveira. All rights reserved. +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 -/ @@ -7,3 +7,9 @@ import LeanPool.NagataFactoriality.NagataFactoriality.Basic import LeanPool.NagataFactoriality.NagataFactoriality.Localization import LeanPool.NagataFactoriality.NagataFactoriality.Nagata import LeanPool.NagataFactoriality.NagataFactoriality.Applications + +/-! +# NagataFactoriality + +Supporting results for Nagata’s factoriality theorem. +-/ diff --git a/LeanPool/NagataFactoriality/NagataFactoriality/Applications.lean b/LeanPool/NagataFactoriality/NagataFactoriality/Applications.lean index 0a040f6024..3fe2bc9396 100644 --- a/LeanPool/NagataFactoriality/NagataFactoriality/Applications.lean +++ b/LeanPool/NagataFactoriality/NagataFactoriality/Applications.lean @@ -1,5 +1,5 @@ /- -Copyright (c) 2026 Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina G. de Oliveira. All rights reserved. +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 -/ @@ -7,3 +7,9 @@ import LeanPool.NagataFactoriality.NagataFactoriality.Applications.Gauss import LeanPool.NagataFactoriality.NagataFactoriality.Applications.Laurent import LeanPool.NagataFactoriality.NagataFactoriality.Applications.FractionField import LeanPool.NagataFactoriality.NagataFactoriality.Applications.Examples + +/-! +# Applications + +Supporting results for Nagata’s factoriality theorem. +-/ diff --git a/LeanPool/NagataFactoriality/NagataFactoriality/Applications/Examples.lean b/LeanPool/NagataFactoriality/NagataFactoriality/Applications/Examples.lean index 1b9b09afec..fdaf91bf67 100644 --- a/LeanPool/NagataFactoriality/NagataFactoriality/Applications/Examples.lean +++ b/LeanPool/NagataFactoriality/NagataFactoriality/Applications/Examples.lean @@ -1,5 +1,5 @@ /- -Copyright (c) 2026 Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina G. de Oliveira. All rights reserved. +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 -/ @@ -7,6 +7,12 @@ import Mathlib.Algebra.EuclideanDomain.Int import Mathlib.RingTheory.PrincipalIdealDomain import Mathlib.RingTheory.Polynomial.UniqueFactorization +/-! +# Examples + +Supporting results for Nagata’s factoriality theorem. +-/ + namespace NagataFactoriality open Polynomial diff --git a/LeanPool/NagataFactoriality/NagataFactoriality/Applications/FractionField.lean b/LeanPool/NagataFactoriality/NagataFactoriality/Applications/FractionField.lean index b83addf2e4..0b8582dc09 100644 --- a/LeanPool/NagataFactoriality/NagataFactoriality/Applications/FractionField.lean +++ b/LeanPool/NagataFactoriality/NagataFactoriality/Applications/FractionField.lean @@ -1,5 +1,5 @@ /- -Copyright (c) 2026 Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina G. de Oliveira. All rights reserved. +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 -/ @@ -38,6 +38,8 @@ with `R[T;T⁻¹]`. then `R[X]` is a UFD, proved by localizing at constant primes and using Nagata's theorem. -/ +noncomputable section + namespace NagataFactoriality open Polynomial @@ -71,6 +73,7 @@ private theorem constPrimeSubmonoid_le_nzdMapC : 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) : @@ -124,21 +127,21 @@ theorem polynomial_uniqueFactorizationMonoid_via_fractionField [IsNoetherianRing R] : UniqueFactorizationMonoid R[X] := by let S := constPrimeSubmonoid R have hS : PrimeGenerated S := constPrimeSubmonoid_primeGenerated R - letI : Fact ((0 : R[X]) ∉ S) := ⟨zero_notMem_of_primeGenerated hS⟩ + let : Fact ((0 : R[X]) ∉ S) := ⟨zero_notMem_of_primeGenerated hS⟩ -- Set up the algebra structure on (FractionRing R)[X] over R[X] - letI : Algebra R[X] (FractionRing 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 - letI : IsLocalization (nzdMapC R) (FractionRing R)[X] := + let : IsLocalization (nzdMapC R) (FractionRing R)[X] := Polynomial.isLocalization (nonZeroDivisors R) (FractionRing R) -- The localization at constPrimeSubmonoid is also a localization at nzdMapC - letI : IsLocalization (nzdMapC R) (_root_.Localization S) := + 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 - haveI : UniqueFactorizationMonoid (FractionRing R)[X] := inferInstance + have : UniqueFactorizationMonoid (FractionRing R)[X] := inferInstance -- Transfer UFD across the algebra equivalence have hUFDLoc : UniqueFactorizationMonoid (_root_.Localization S) := MulEquiv.uniqueFactorizationMonoid e.toMulEquiv inferInstance diff --git a/LeanPool/NagataFactoriality/NagataFactoriality/Applications/Gauss.lean b/LeanPool/NagataFactoriality/NagataFactoriality/Applications/Gauss.lean index 897249e82a..d486bde547 100644 --- a/LeanPool/NagataFactoriality/NagataFactoriality/Applications/Gauss.lean +++ b/LeanPool/NagataFactoriality/NagataFactoriality/Applications/Gauss.lean @@ -1,5 +1,5 @@ /- -Copyright (c) 2026 Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina G. de Oliveira. All rights reserved. +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 -/ @@ -7,19 +7,25 @@ import Mathlib.RingTheory.Polynomial.Content import Mathlib.RingTheory.Polynomial.GaussLemma import Mathlib.RingTheory.Polynomial.UniqueFactorization +/-! +# Gauss + +Supporting results for Nagata’s factoriality theorem. +-/ + namespace NagataFactoriality open Polynomial -theorem polynomial_content_mul {R : Type*} [CommRing R] [IsDomain R] [NormalizedGCDMonoid R] +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] [IsDomain R] [NormalizedGCDMonoid R] +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] [IsDomain R] +theorem polynomial_uniqueFactorizationMonoid {R : Type*} [CommRing R] [UniqueFactorizationMonoid R] : UniqueFactorizationMonoid R[X] := by infer_instance diff --git a/LeanPool/NagataFactoriality/NagataFactoriality/Applications/Laurent.lean b/LeanPool/NagataFactoriality/NagataFactoriality/Applications/Laurent.lean index 86f61f4d20..2e7bf83d31 100644 --- a/LeanPool/NagataFactoriality/NagataFactoriality/Applications/Laurent.lean +++ b/LeanPool/NagataFactoriality/NagataFactoriality/Applications/Laurent.lean @@ -1,5 +1,5 @@ /- -Copyright (c) 2026 Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina G. de Oliveira. All rights reserved. +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 -/ @@ -10,6 +10,12 @@ import Mathlib.RingTheory.Polynomial.UniqueFactorization import LeanPool.NagataFactoriality.NagataFactoriality.Nagata.Lemmas import LeanPool.NagataFactoriality.NagataFactoriality.Nagata.Theorem +/-! +# Laurent + +Supporting results for Nagata’s factoriality theorem. +-/ + namespace NagataFactoriality open scoped LaurentPolynomial @@ -23,7 +29,7 @@ theorem polynomial_prime_X {R : Type*} [CommRing R] [IsDomain R] : Prime (Polynomial.X : R[X]) := (Polynomial.prime_X : Prime (Polynomial.X : R[X])) -theorem polynomial_toLaurent_prime_of_not_dvd_X {R : Type*} [CommRing R] [IsDomain R] +theorem polynomial_toLaurent_prime_of_not_dvd_X {R : Type*} [CommRing R] {p : R[X]} (hp : Prime p) (hX : ¬ p ∣ X) : Prime (Polynomial.toLaurent p) := by let M : Submonoid R[X] := Submonoid.powers X have hspanPrime : (Ideal.span ({p} : Set R[X])).IsPrime := @@ -46,7 +52,7 @@ theorem polynomial_toLaurent_prime_of_not_dvd_X {R : Type*} [CommRing R] [IsDoma theorem laurentPolynomial_uniqueFactorizationMonoid {R : Type*} [CommRing R] [IsDomain R] [UniqueFactorizationMonoid R] : UniqueFactorizationMonoid R[T;T⁻¹] := by - letI : UniqueFactorizationMonoid R[X] := inferInstance + let : UniqueFactorizationMonoid R[X] := inferInstance rw [UniqueFactorizationMonoid.iff_exists_prime_factors] intro f hf obtain ⟨n, p, hpLaurent⟩ := LaurentPolynomial.exists_T_pow f @@ -85,7 +91,8 @@ theorem laurentPolynomial_uniqueFactorizationMonoid {R : Type*} [CommRing R] [Is have hpqAssoc : Associated (Polynomial.toLaurent p) (Polynomial.toLaurent q) := by rw [hpq', map_mul, Polynomial.toLaurent_X_pow] simpa [LaurentPolynomial.T_mul] using - (associated_mul_unit_left (Polynomial.toLaurent q) (LaurentPolynomial.T (p.rootMultiplicity 0)) + (associated_mul_unit_left (Polynomial.toLaurent q) + (LaurentPolynomial.T (p.rootMultiplicity 0)) (LaurentPolynomial.isUnit_T (p.rootMultiplicity 0))) exact hmapassoc.trans (hfp.trans hpqAssoc).symm @@ -95,19 +102,20 @@ theorem polynomial_uniqueFactorizationMonoid_of_laurent {R : Type*} [CommRing R] let S : Submonoid R[X] := Submonoid.powers X have hS : PrimeGenerated S := by simpa [S] using (primeGenerated_powers (p := (X : R[X])) (polynomial_prime_X (R := R))) - letI : _root_.IsLocalization S R[T;T⁻¹] := by - simpa [S] using (laurentPolynomial_isLocalization R : _root_.IsLocalization.Away (X : R[X]) R[T;T⁻¹]) + let : _root_.IsLocalization S R[T;T⁻¹] := by + simpa [S] using (laurentPolynomial_isLocalization R : + _root_.IsLocalization.Away (X : R[X]) R[T;T⁻¹]) exact nagata_theorem_isLocalization (R := R[X]) (T := R[T;T⁻¹]) S hS inferInstance theorem polynomial_uniqueFactorizationMonoid_via_nagata {R : Type*} [CommRing R] [IsDomain R] [IsNoetherianRing R] [UniqueFactorizationMonoid R] : UniqueFactorizationMonoid R[X] := by - letI : UniqueFactorizationMonoid R[T;T⁻¹] := laurentPolynomial_uniqueFactorizationMonoid (R := R) + let : UniqueFactorizationMonoid R[T;T⁻¹] := laurentPolynomial_uniqueFactorizationMonoid (R := R) exact polynomial_uniqueFactorizationMonoid_of_laurent (R := R) theorem iterated_polynomial_uniqueFactorizationMonoid_via_nagata {R : Type*} [CommRing R] [IsDomain R] [IsNoetherianRing R] [UniqueFactorizationMonoid R] : UniqueFactorizationMonoid (Polynomial (Polynomial R)) := by - letI : UniqueFactorizationMonoid R[X] := + let : UniqueFactorizationMonoid R[X] := polynomial_uniqueFactorizationMonoid_via_nagata (R := R) simpa using polynomial_uniqueFactorizationMonoid_via_nagata (R := R[X]) diff --git a/LeanPool/NagataFactoriality/NagataFactoriality/Basic.lean b/LeanPool/NagataFactoriality/NagataFactoriality/Basic.lean index c09562f153..ed1dfe14f8 100644 --- a/LeanPool/NagataFactoriality/NagataFactoriality/Basic.lean +++ b/LeanPool/NagataFactoriality/NagataFactoriality/Basic.lean @@ -1,5 +1,5 @@ /- -Copyright (c) 2026 Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina G. de Oliveira. All rights reserved. +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 -/ @@ -7,3 +7,9 @@ import LeanPool.NagataFactoriality.NagataFactoriality.Basic.Ring import LeanPool.NagataFactoriality.NagataFactoriality.Basic.Divisibility import LeanPool.NagataFactoriality.NagataFactoriality.Basic.Noetherian import LeanPool.NagataFactoriality.NagataFactoriality.Basic.UFD + +/-! +# Basic + +Supporting results for Nagata’s factoriality theorem. +-/ diff --git a/LeanPool/NagataFactoriality/NagataFactoriality/Basic/Divisibility.lean b/LeanPool/NagataFactoriality/NagataFactoriality/Basic/Divisibility.lean index 91efe32ce6..87e7d7bf54 100644 --- a/LeanPool/NagataFactoriality/NagataFactoriality/Basic/Divisibility.lean +++ b/LeanPool/NagataFactoriality/NagataFactoriality/Basic/Divisibility.lean @@ -1,15 +1,22 @@ /- -Copyright (c) 2026 Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina G. de Oliveira. All rights reserved. +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 -/ import Mathlib.RingTheory.Noetherian.UniqueFactorizationDomain import LeanPool.NagataFactoriality.NagataFactoriality.Basic.Ring +/-! +# Divisibility + +Supporting results for Nagata’s factoriality theorem. +-/ + namespace NagataFactoriality open scoped BigOperators +/-- The product of a finite list, defined recursively. -/ def listProd {α : Type*} [CommMonoid α] : List α → α | [] => 1 | a :: as => a * listProd as @@ -70,11 +77,11 @@ theorem prime_irreducible {α : Type*} [CommRing α] [IsDomain α] {p : α} (hp Irreducible p := hp.irreducible -theorem associated_of_irreducible_of_dvd {α : Type*} [CommRing α] [IsDomain α] {p q : α} +theorem associated_of_irreducible_of_dvd {α : Type*} [CommRing α] {p q : α} (hp : Irreducible p) (hq : Irreducible q) (hdiv : p ∣ q) : Associated p q := by exact (hp.dvd_irreducible_iff_associated hq).mp hdiv -theorem prime_of_associated {α : Type*} [CommRing α] [IsDomain α] {p q : α} +theorem prime_of_associated {α : Type*} [CommRing α] {p q : α} (hp : Prime p) (hassoc : Associated p q) : Prime q := by exact (hassoc.prime_iff).mp hp diff --git a/LeanPool/NagataFactoriality/NagataFactoriality/Basic/Noetherian.lean b/LeanPool/NagataFactoriality/NagataFactoriality/Basic/Noetherian.lean index 83857287f1..33620d844d 100644 --- a/LeanPool/NagataFactoriality/NagataFactoriality/Basic/Noetherian.lean +++ b/LeanPool/NagataFactoriality/NagataFactoriality/Basic/Noetherian.lean @@ -1,11 +1,17 @@ /- -Copyright (c) 2026 Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina G. de Oliveira. All rights reserved. +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 -/ import Mathlib.RingTheory.Noetherian.UniqueFactorizationDomain import LeanPool.NagataFactoriality.NagataFactoriality.Basic.Divisibility +/-! +# Noetherian + +Supporting results for Nagata’s factoriality theorem. +-/ + namespace NagataFactoriality theorem hasFactorization_of_noetherian {α : Type*} [CommRing α] [IsDomain α] @@ -14,7 +20,7 @@ theorem hasFactorization_of_noetherian {α : Type*} [CommRing α] [IsDomain α] theorem IsNoetherianRing.hasFactorization {α : Type*} [CommRing α] [IsDomain α] (h : IsNoetherianRing α) : WfDvdMonoid α := by - letI := h + let := h exact hasFactorization_of_noetherian (α := α) end NagataFactoriality diff --git a/LeanPool/NagataFactoriality/NagataFactoriality/Basic/Ring.lean b/LeanPool/NagataFactoriality/NagataFactoriality/Basic/Ring.lean index 32a825c502..08ce5a9e56 100644 --- a/LeanPool/NagataFactoriality/NagataFactoriality/Basic/Ring.lean +++ b/LeanPool/NagataFactoriality/NagataFactoriality/Basic/Ring.lean @@ -1,9 +1,17 @@ /- -Copyright (c) 2026 Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina G. de Oliveira. All rights reserved. +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 -/ -import Mathlib +import Mathlib.RingTheory.Noetherian.Basic +import Mathlib.RingTheory.UniqueFactorizationDomain.Basic +import Mathlib.Tactic + +/-! +# Ring + +Supporting results for Nagata’s factoriality theorem. +-/ namespace NagataFactoriality diff --git a/LeanPool/NagataFactoriality/NagataFactoriality/Basic/UFD.lean b/LeanPool/NagataFactoriality/NagataFactoriality/Basic/UFD.lean index 4b545e3c26..6639e9f336 100644 --- a/LeanPool/NagataFactoriality/NagataFactoriality/Basic/UFD.lean +++ b/LeanPool/NagataFactoriality/NagataFactoriality/Basic/UFD.lean @@ -1,11 +1,17 @@ /- -Copyright (c) 2026 Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina G. de Oliveira. All rights reserved. +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 -/ import Mathlib.RingTheory.UniqueFactorizationDomain.Basic import LeanPool.NagataFactoriality.NagataFactoriality.Basic.Noetherian +/-! +# UFD + +Supporting results for Nagata’s factoriality theorem. +-/ + namespace NagataFactoriality theorem ufd_iff_factorization_and_irreducibles_prime {α : Type*} [CommRing α] [IsDomain α] : @@ -13,20 +19,20 @@ theorem ufd_iff_factorization_and_irreducibles_prime {α : Type*} [CommRing α] constructor · intro h refine ⟨?_, ?_⟩ - · letI : UniqueFactorizationMonoid α := h + · let : UniqueFactorizationMonoid α := h exact (inferInstance : WfDvdMonoid α) · intro p hp - letI : UniqueFactorizationMonoid α := h + let : UniqueFactorizationMonoid α := h exact (UniqueFactorizationMonoid.irreducible_iff_prime).mp hp · rintro ⟨hfac, hprime⟩ exact UniqueFactorizationMonoid.of_exists_prime_factors (fun a ha => by - letI : WfDvdMonoid α := hfac + let : WfDvdMonoid α := hfac obtain ⟨f, hf, hassoc⟩ := WfDvdMonoid.exists_factors a ha refine ⟨f, ?_, hassoc⟩ intro b hb exact hprime b (hf b hb)) -theorem prime_iff_irreducible_of_ufd {α : Type*} [CommRing α] [IsDomain α] +theorem prime_iff_irreducible_of_ufd {α : Type*} [CommRing α] [UniqueFactorizationMonoid α] {p : α} : Prime p ↔ Irreducible p := UniqueFactorizationMonoid.irreducible_iff_prime.symm @@ -51,7 +57,7 @@ theorem factorization_unique {α : Type*} [CommRing α] [IsDomain α] (hg : ∀ x ∈ g, Irreducible x) (hfg : Associated f.prod g.prod) : FactorizationEquivalent f g := by - letI : UniqueFactorizationMonoid α := ufd_of_factorization_and_primes hfac hprime + let : UniqueFactorizationMonoid α := ufd_of_factorization_and_primes hfac hprime exact UniqueFactorizationMonoid.factors_unique hf hg hfg theorem factors_unique {α : Type*} [CommRing α] [IsDomain α] @@ -60,9 +66,9 @@ theorem factors_unique {α : Type*} [CommRing α] [IsDomain α] {a : α} (ha : a ≠ 0) {f : Multiset α} (hf : ∀ x ∈ f, Irreducible x) (hfa : Associated f.prod a) : - letI : UniqueFactorizationMonoid α := ufd_of_factorization_and_primes hfac hprime + let : UniqueFactorizationMonoid α := ufd_of_factorization_and_primes hfac hprime FactorizationEquivalent f (UniqueFactorizationMonoid.factors a) := by - letI : UniqueFactorizationMonoid α := ufd_of_factorization_and_primes hfac hprime + let : UniqueFactorizationMonoid α := ufd_of_factorization_and_primes hfac hprime exact UniqueFactorizationMonoid.factors_unique hf UniqueFactorizationMonoid.irreducible_of_factor (hfa.trans (UniqueFactorizationMonoid.factors_prod ha).symm) diff --git a/LeanPool/NagataFactoriality/NagataFactoriality/Localization.lean b/LeanPool/NagataFactoriality/NagataFactoriality/Localization.lean index fdcce48ca3..0148e1cb9f 100644 --- a/LeanPool/NagataFactoriality/NagataFactoriality/Localization.lean +++ b/LeanPool/NagataFactoriality/NagataFactoriality/Localization.lean @@ -1,5 +1,5 @@ /- -Copyright (c) 2026 Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina G. de Oliveira. All rights reserved. +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 -/ @@ -7,3 +7,9 @@ import LeanPool.NagataFactoriality.NagataFactoriality.Localization.MultSet import LeanPool.NagataFactoriality.NagataFactoriality.Localization.Localization import LeanPool.NagataFactoriality.NagataFactoriality.Localization.IsLocalization import LeanPool.NagataFactoriality.NagataFactoriality.Localization.Properties + +/-! +# Localization + +Supporting results for Nagata’s factoriality theorem. +-/ diff --git a/LeanPool/NagataFactoriality/NagataFactoriality/Localization/IsLocalization.lean b/LeanPool/NagataFactoriality/NagataFactoriality/Localization/IsLocalization.lean index 50dc8456fc..f02e2b7a98 100644 --- a/LeanPool/NagataFactoriality/NagataFactoriality/Localization/IsLocalization.lean +++ b/LeanPool/NagataFactoriality/NagataFactoriality/Localization/IsLocalization.lean @@ -1,11 +1,17 @@ /- -Copyright (c) 2026 Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina G. de Oliveira. All rights reserved. +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 -/ import Mathlib.RingTheory.Localization.Basic import LeanPool.NagataFactoriality.NagataFactoriality.Localization.MultSet +/-! +# IsLocalization + +Supporting results for Nagata’s factoriality theorem. +-/ + namespace NagataFactoriality namespace IsLocalization @@ -13,7 +19,7 @@ namespace IsLocalization variable {α β : Type*} [CommRing α] [CommRing β] {S : Submonoid α} variable [Algebra α β] [_root_.IsLocalization S β] -@[simp] theorem mk'_mul_map (a s : α) (hs : s ∈ S) : +theorem mk'_mul_map (a s : α) (hs : s ∈ S) : _root_.IsLocalization.mk' β a ⟨s, hs⟩ * algebraMap α β s = algebraMap α β a := by exact _root_.IsLocalization.mk'_spec_mk (M := S) (S := β) a s hs @@ -23,7 +29,7 @@ variable [Algebra α β] [_root_.IsLocalization S β] simpa using (_root_.IsLocalization.mul_mk'_eq_mk'_of_mul (M := S) (S := β) a b ⟨s, hs⟩) theorem surj (z : β) : ∃ a s, ∃ hs : s ∈ S, z = _root_.IsLocalization.mk' β a ⟨s, hs⟩ := by - obtain ⟨a, s, hs⟩ := _root_.IsLocalization.mk'_surjective (M := S) (S := β) z + obtain ⟨⟨a, s⟩, hs⟩ := _root_.IsLocalization.mk'_surjective (M := S) (S := β) z exact ⟨a, s, s.property, hs.symm⟩ section Nonzero @@ -36,7 +42,8 @@ theorem algebraMap_injective (S : Submonoid α) [Fact ((0 : α) ∉ S)] [_root_. _root_.IsLocalization.injective (M := S) (S := β) hle theorem mk'_eq_iff {a b s t : α} (hs : s ∈ S) (ht : t ∈ S) : - _root_.IsLocalization.mk' β a ⟨s, hs⟩ = _root_.IsLocalization.mk' β b ⟨t, ht⟩ ↔ a * t = b * s := by + _root_.IsLocalization.mk' β a ⟨s, hs⟩ = _root_.IsLocalization.mk' β b ⟨t, ht⟩ ↔ + a * t = b * s := by constructor · intro h have h' := (_root_.IsLocalization.mk'_eq_iff_eq' (M := S) (S := β)).1 h @@ -55,7 +62,7 @@ theorem mk'_eq_zero_iff {a s : α} (hs : s ∈ S) : have h := mk'_eq_iff (S := S) (β := β) (a := a) (b := 0) (s := s) (t := 1) hs S.one_mem simpa using h -@[simp] theorem map_eq_zero_iff (S : Submonoid α) [Fact ((0 : α) ∉ S)] [_root_.IsLocalization S β] +theorem map_eq_zero_iff (S : Submonoid α) [Fact ((0 : α) ∉ S)] [_root_.IsLocalization S β] (a : α) : algebraMap α β a = 0 ↔ a = 0 := by let hle : S ≤ nonZeroDivisors α := NagataFactoriality.Submonoid.le_nonZeroDivisors exact _root_.IsLocalization.to_map_eq_zero_iff (M := S) (S := β) (x := a) hle @@ -87,7 +94,8 @@ theorem dvd_map_iff {a b : α} : _ = _root_.IsLocalization.mk' β b ⟨1, S.one_mem⟩ := by apply (mk'_eq_iff (S := S) (β := β) (hs := hs) (ht := S.one_mem)).2 simpa [mul_assoc, mul_left_comm, mul_comm] using hc.symm - _ = algebraMap α β b := by simpa using (_root_.IsLocalization.mk'_one (S := β) b) + _ = algebraMap α β b := by + convert (_root_.IsLocalization.mk'_one (M := S) (S := β) b) using 1 end Nonzero diff --git a/LeanPool/NagataFactoriality/NagataFactoriality/Localization/Localization.lean b/LeanPool/NagataFactoriality/NagataFactoriality/Localization/Localization.lean index 9673417cf6..8d67cf27c9 100644 --- a/LeanPool/NagataFactoriality/NagataFactoriality/Localization/Localization.lean +++ b/LeanPool/NagataFactoriality/NagataFactoriality/Localization/Localization.lean @@ -1,27 +1,37 @@ /- -Copyright (c) 2026 Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina G. de Oliveira. All rights reserved. +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 -/ import Mathlib.RingTheory.Localization.Basic import LeanPool.NagataFactoriality.NagataFactoriality.Localization.MultSet +/-! +# Localization + +Supporting results for Nagata’s factoriality theorem. +-/ + namespace NagataFactoriality +/-- Localization of a commutative ring at a multiplicative submonoid. -/ abbrev Localization {α : Type*} [CommRing α] (S : Submonoid α) := _root_.Localization S namespace Localization variable {α : Type*} [CommRing α] {S : Submonoid α} +/-- The fraction with the given numerator and denominator in the submonoid. -/ def mk (a s : α) (hs : s ∈ S) : Localization S := _root_.Localization.mk a ⟨s, hs⟩ +/-- The canonical map from the ring into its localization. -/ def of (a : α) : Localization S := algebraMap α (Localization S) a @[simp] theorem mk_one (a : α) : mk (S := S) a 1 S.one_mem = of (S := S) a := by - simpa [mk, of] using (_root_.Localization.mk_one_eq_algebraMap (M := S) a) + unfold mk of + convert (_root_.Localization.mk_one_eq_algebraMap (M := S) a) using 1 @[simp] theorem of_zero : of (S := S) (0 : α) = 0 := by simp [of] @@ -49,7 +59,7 @@ def of (a : α) : Localization S := exact mk_mul_den (S := S) a s hs theorem surj (z : Localization S) : ∃ a s, ∃ hs : s ∈ S, z = mk (S := S) a s hs := by - obtain ⟨a, s, hs⟩ := IsLocalization.mk'_surjective (M := S) (S := Localization S) z + obtain ⟨⟨a, s⟩, hs⟩ := IsLocalization.mk'_surjective (M := S) (S := Localization S) z exact ⟨a, s, s.property, by simpa [mk, _root_.Localization.mk_eq_mk'_apply] using hs.symm⟩ @@ -92,7 +102,7 @@ theorem mk_eq_zero_iff {a s : α} (hs : s ∈ S) : mk (S := S) a s hs = 0 ↔ a simpa [of] using h @[simp] theorem of_eq_zero_iff (a : α) : of (S := S) a = 0 ↔ a = 0 := by - show algebraMap α (Localization S) a = 0 ↔ a = 0 + change algebraMap α (Localization S) a = 0 ↔ a = 0 exact IsLocalization.to_map_eq_zero_iff (M := S) (S := Localization S) (x := a) (Submonoid.le_nonZeroDivisors (S := S)) diff --git a/LeanPool/NagataFactoriality/NagataFactoriality/Localization/MultSet.lean b/LeanPool/NagataFactoriality/NagataFactoriality/Localization/MultSet.lean index 5ea7e2561e..b4ce73995f 100644 --- a/LeanPool/NagataFactoriality/NagataFactoriality/Localization/MultSet.lean +++ b/LeanPool/NagataFactoriality/NagataFactoriality/Localization/MultSet.lean @@ -1,10 +1,16 @@ /- -Copyright (c) 2026 Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina G. de Oliveira. All rights reserved. +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 -/ import LeanPool.NagataFactoriality.NagataFactoriality.Basic.Divisibility +/-! +# MultSet + +Supporting results for Nagata’s factoriality theorem. +-/ + namespace NagataFactoriality namespace Submonoid diff --git a/LeanPool/NagataFactoriality/NagataFactoriality/Localization/Properties.lean b/LeanPool/NagataFactoriality/NagataFactoriality/Localization/Properties.lean index 8801e46810..fedb34d26b 100644 --- a/LeanPool/NagataFactoriality/NagataFactoriality/Localization/Properties.lean +++ b/LeanPool/NagataFactoriality/NagataFactoriality/Localization/Properties.lean @@ -1,7 +1,13 @@ /- -Copyright (c) 2026 Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina G. de Oliveira. All rights reserved. +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 -/ import LeanPool.NagataFactoriality.NagataFactoriality.Localization.Localization import LeanPool.NagataFactoriality.NagataFactoriality.Localization.IsLocalization + +/-! +# Properties + +Supporting results for Nagata’s factoriality theorem. +-/ diff --git a/LeanPool/NagataFactoriality/NagataFactoriality/Nagata.lean b/LeanPool/NagataFactoriality/NagataFactoriality/Nagata.lean index a6390a0749..998837771f 100644 --- a/LeanPool/NagataFactoriality/NagataFactoriality/Nagata.lean +++ b/LeanPool/NagataFactoriality/NagataFactoriality/Nagata.lean @@ -1,7 +1,13 @@ /- -Copyright (c) 2026 Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina G. de Oliveira. All rights reserved. +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 -/ import LeanPool.NagataFactoriality.NagataFactoriality.Nagata.Lemmas import LeanPool.NagataFactoriality.NagataFactoriality.Nagata.Theorem + +/-! +# Nagata + +Supporting results for Nagata’s factoriality theorem. +-/ diff --git a/LeanPool/NagataFactoriality/NagataFactoriality/Nagata/Lemmas.lean b/LeanPool/NagataFactoriality/NagataFactoriality/Nagata/Lemmas.lean index b772e8b437..7fa82ca3cd 100644 --- a/LeanPool/NagataFactoriality/NagataFactoriality/Nagata/Lemmas.lean +++ b/LeanPool/NagataFactoriality/NagataFactoriality/Nagata/Lemmas.lean @@ -1,5 +1,5 @@ /- -Copyright (c) 2026 Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina G. de Oliveira. All rights reserved. +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 -/ @@ -7,16 +7,23 @@ import LeanPool.NagataFactoriality.NagataFactoriality.Localization.Properties import LeanPool.NagataFactoriality.NagataFactoriality.Localization.IsLocalization import LeanPool.NagataFactoriality.NagataFactoriality.Basic.UFD +/-! +# Lemmas + +Supporting results for Nagata’s factoriality theorem. +-/ + namespace NagataFactoriality -def Avoids {α : Type*} [CommRing α] [IsDomain α] (S : Submonoid α) (p : α) : Prop := +/-- An element avoids a multiplicative set when it divides none of its members. -/ +def Avoids {α : Type*} [CommRing α] (S : Submonoid α) (p : α) : Prop := ∀ s : α, s ∈ S → ¬ p ∣ s /-- A submonoid is prime-generated if each of its elements is a finite product of prime elements. -/ def PrimeGenerated {α : Type*} [CommRing α] (S : Submonoid α) : Prop := ∀ s : α, s ∈ S → ∃ f : Multiset α, (∀ q ∈ f, q ∈ S ∧ Prime q) ∧ f.prod = s -private def submonoidZeroNotMemFact {α : Type*} [CommRing α] [IsDomain α] {S : Submonoid α} +private theorem submonoidZeroNotMemFact {α : Type*} [CommRing α] [IsDomain α] {S : Submonoid α} (hS : ∀ s ∈ S, Prime s ∨ IsUnit s) : Fact ((0 : α) ∉ S) := ⟨Submonoid.zero_notMem_of_prime_or_unit hS⟩ @@ -99,7 +106,8 @@ theorem prime_of_irreducible_of_dvd_prime_factors {α : Type*} [CommRing α] [Is have hcancel : qs.prod = p * e := by apply mul_left_cancel₀ hq.ne_zero calc - q * qs.prod = p * d := by simpa [Multiset.prod_cons, mul_assoc, mul_left_comm, mul_comm] using hd + q * qs.prod = p * d := by + simpa [Multiset.prod_cons, mul_assoc, mul_left_comm, mul_comm] using hd _ = p * (q * e) := by rw [hde] _ = q * (p * e) := by ac_rfl exact ih htail ⟨e, hcancel⟩ @@ -151,11 +159,12 @@ theorem dvd_of_mul_eq_prime_factors {α : Type*} [CommRing α] [IsDomain α] exact hmain f hf hnot hEq theorem dvd_of_localization_dvd_primeGenerated_isLocalization {α β : Type*} - [CommRing α] [IsDomain α] {S : Submonoid α} [CommRing β] [Algebra α β] [IsDomain β] + [CommRing α] [IsDomain α] {S : Submonoid α} [CommRing β] [Algebra α β] [_root_.IsLocalization S β] (hS : PrimeGenerated S) {p a : α} (hp : Irreducible p) (havoid : Avoids S p) (hdiv : algebraMap α β p ∣ algebraMap α β a) : p ∣ a := by - letI : Fact ((0 : α) ∉ S) := ⟨zero_notMem_of_primeGenerated hS⟩ - rcases (NagataFactoriality.IsLocalization.dvd_map_iff (S := S) (β := β) (a := p) (b := a)).1 hdiv with + let : Fact ((0 : α) ∉ S) := ⟨zero_notMem_of_primeGenerated hS⟩ + rcases (NagataFactoriality.IsLocalization.dvd_map_iff + (S := S) (β := β) (a := p) (b := a)).1 hdiv with ⟨s, hs, hsa⟩ rcases hsa with ⟨c, hc⟩ rcases hS s hs with ⟨f, hf, hprod⟩ @@ -172,9 +181,10 @@ theorem dvd_of_localization_dvd_primeGenerated_isLocalization {α β : Type*} theorem dvd_of_localization_dvd_primeGenerated {α : Type*} [CommRing α] [IsDomain α] {S : Submonoid α} (hS : PrimeGenerated S) {p a : α} (hp : Irreducible p) - (havoid : Avoids S p) (hdiv : Localization.of (S := S) p ∣ Localization.of (S := S) a) : p ∣ a := by - letI : Fact ((0 : α) ∉ S) := ⟨zero_notMem_of_primeGenerated hS⟩ - letI : IsDomain (Localization S) := by infer_instance + (havoid : Avoids S p) + (hdiv : Localization.of (S := S) p ∣ Localization.of (S := S) a) : p ∣ a := by + let : Fact ((0 : α) ∉ S) := ⟨zero_notMem_of_primeGenerated hS⟩ + let : IsDomain (Localization S) := by infer_instance simpa [Localization.of] using (dvd_of_localization_dvd_primeGenerated_isLocalization (β := Localization S) (S := S) hS hp havoid hdiv) @@ -263,10 +273,10 @@ theorem split_prime_factors_of_mul_eq {α : Type*} [CommRing α] [IsDomain α] exact hmain f a b hf hEq theorem localization_irreducible_of_irreducible_primeGenerated_isLocalization {α β : Type*} - [CommRing α] [IsDomain α] {S : Submonoid α} [CommRing β] [Algebra α β] [IsDomain β] + [CommRing α] [IsDomain α] {S : Submonoid α} [CommRing β] [Algebra α β] [_root_.IsLocalization S β] (hS : PrimeGenerated S) {p : α} (hp : Irreducible p) (havoid : Avoids S p) : Irreducible (algebraMap α β p) := by - letI : Fact ((0 : α) ∉ S) := ⟨zero_notMem_of_primeGenerated hS⟩ + let : Fact ((0 : α) ∉ S) := ⟨zero_notMem_of_primeGenerated hS⟩ refine ⟨?_, ?_⟩ · intro hunit have hdiv : algebraMap α β p ∣ (1 : β) := by @@ -296,7 +306,7 @@ theorem localization_irreducible_of_irreducible_primeGenerated_isLocalization { _root_.IsLocalization.mk' β (a * b) ⟨s * t, S.mul_mem hs ht⟩ := by calc _root_.IsLocalization.mk' β p ⟨1, S.one_mem⟩ = algebraMap α β p := by - simpa using (_root_.IsLocalization.mk'_one (S := β) p) + convert (_root_.IsLocalization.mk'_one (S := β) p) using 1 _ = _root_.IsLocalization.mk' β (a * b) ⟨s * t, S.mul_mem hs ht⟩ := hloc simpa [mul_one] using (NagataFactoriality.IsLocalization.mk'_eq_iff @@ -340,8 +350,8 @@ theorem localization_irreducible_of_irreducible_primeGenerated_isLocalization { theorem localization_irreducible_of_irreducible_primeGenerated {α : Type*} [CommRing α] [IsDomain α] {S : Submonoid α} (hS : PrimeGenerated S) {p : α} (hp : Irreducible p) (havoid : Avoids S p) : Irreducible (Localization.of (S := S) p) := by - letI : Fact ((0 : α) ∉ S) := ⟨zero_notMem_of_primeGenerated hS⟩ - letI : IsDomain (Localization S) := by infer_instance + let : Fact ((0 : α) ∉ S) := ⟨zero_notMem_of_primeGenerated hS⟩ + let : IsDomain (Localization S) := by infer_instance simpa [Localization.of] using (localization_irreducible_of_irreducible_primeGenerated_isLocalization (β := Localization S) (S := S) hS hp havoid) @@ -350,7 +360,7 @@ theorem prime_of_localization_prime_primeGenerated_isLocalization {α β : Type* [CommRing α] [IsDomain α] {S : Submonoid α} [CommRing β] [Algebra α β] [IsDomain β] [_root_.IsLocalization S β] (hS : PrimeGenerated S) {p : α} (hp : Irreducible p) (havoid : Avoids S p) (hploc : Prime (algebraMap α β p)) : Prime p := by - letI : Fact ((0 : α) ∉ S) := ⟨zero_notMem_of_primeGenerated hS⟩ + let : Fact ((0 : α) ∉ S) := ⟨zero_notMem_of_primeGenerated hS⟩ refine ⟨hp.ne_zero, hp.not_isUnit, ?_⟩ intro a b hdiv have hlocdiv : algebraMap α β p ∣ algebraMap α β (a * b) := by @@ -368,8 +378,8 @@ theorem prime_of_localization_prime_primeGenerated_isLocalization {α β : Type* theorem prime_of_localization_prime_primeGenerated {α : Type*} [CommRing α] [IsDomain α] {S : Submonoid α} (hS : PrimeGenerated S) {p : α} (hp : Irreducible p) (havoid : Avoids S p) (hploc : Prime (Localization.of (S := S) p)) : Prime p := by - letI : Fact ((0 : α) ∉ S) := ⟨zero_notMem_of_primeGenerated hS⟩ - letI : IsDomain (Localization S) := by infer_instance + let : Fact ((0 : α) ∉ S) := ⟨zero_notMem_of_primeGenerated hS⟩ + let : IsDomain (Localization S) := by infer_instance simpa [Localization.of] using (prime_of_localization_prime_primeGenerated_isLocalization (β := Localization S) (S := S) hS hp havoid hploc) @@ -378,7 +388,7 @@ theorem nagata_key_lemma_primeGenerated_isLocalization {α β : Type*} [CommRing α] [IsDomain α] {S : Submonoid α} [CommRing β] [Algebra α β] [IsDomain β] [_root_.IsLocalization S β] (hS : PrimeGenerated S) [UniqueFactorizationMonoid β] {p : α} (hp : Irreducible p) : Prime p := by - letI : Fact ((0 : α) ∉ S) := ⟨zero_notMem_of_primeGenerated hS⟩ + let : Fact ((0 : α) ∉ S) := ⟨zero_notMem_of_primeGenerated hS⟩ by_cases hmem : ∃ s : α, s ∈ S ∧ p ∣ s · rcases hmem with ⟨s, hs, hdiv⟩ exact prime_of_irreducible_of_dvd_mem_primeGenerated hS hp hs hdiv @@ -398,12 +408,12 @@ theorem nagata_key_lemma_primeGenerated {α : Type*} [CommRing α] [IsDomain α] (hUFD : @UniqueFactorizationMonoid (Localization S) (by - letI : Fact ((0 : α) ∉ S) := ⟨zero_notMem_of_primeGenerated hS⟩ + let : Fact ((0 : α) ∉ S) := ⟨zero_notMem_of_primeGenerated hS⟩ infer_instance)) {p : α} (hp : Irreducible p) : Prime p := by - letI : Fact ((0 : α) ∉ S) := ⟨zero_notMem_of_primeGenerated hS⟩ - letI : IsDomain (Localization S) := by infer_instance - letI : UniqueFactorizationMonoid (Localization S) := hUFD + let : Fact ((0 : α) ∉ S) := ⟨zero_notMem_of_primeGenerated hS⟩ + let : IsDomain (Localization S) := by infer_instance + let : UniqueFactorizationMonoid (Localization S) := hUFD simpa [Localization.of] using (nagata_key_lemma_primeGenerated_isLocalization (β := Localization S) (S := S) hS hp) @@ -418,10 +428,10 @@ theorem prime_of_irreducible_of_dvd_mem {α : Type*} [CommRing α] [IsDomain α] · exact False.elim (hp.not_isUnit (isUnit_of_dvd_unit hdiv hsUnit)) theorem localization_irreducible_of_irreducible_isLocalization {α β : Type*} - [CommRing α] [IsDomain α] {S : Submonoid α} [CommRing β] [Algebra α β] [IsDomain β] + [CommRing α] [IsDomain α] {S : Submonoid α} [CommRing β] [Algebra α β] [_root_.IsLocalization S β] (hS : ∀ s ∈ S, Prime s ∨ IsUnit s) {p : α} (hp : Irreducible p) (havoid : Avoids S p) : Irreducible (algebraMap α β p) := by - letI : Fact ((0 : α) ∉ S) := submonoidZeroNotMemFact hS + let : Fact ((0 : α) ∉ S) := submonoidZeroNotMemFact hS refine ⟨?_, ?_⟩ · intro hunit have hdiv : algebraMap α β p ∣ (1 : β) := by @@ -450,7 +460,7 @@ theorem localization_irreducible_of_irreducible_isLocalization {α β : Type*} _root_.IsLocalization.mk' β (a * b) ⟨s * t, S.mul_mem hs ht⟩ := by calc _root_.IsLocalization.mk' β p ⟨1, S.one_mem⟩ = algebraMap α β p := by - simpa using (_root_.IsLocalization.mk'_one (S := β) p) + convert (_root_.IsLocalization.mk'_one (S := β) p) using 1 _ = _root_.IsLocalization.mk' β (a * b) ⟨s * t, S.mul_mem hs ht⟩ := hEq simpa [mul_one] using (NagataFactoriality.IsLocalization.mk'_eq_iff @@ -489,7 +499,7 @@ theorem localization_irreducible_of_irreducible_isLocalization {α β : Type*} _root_.IsLocalization.mk' β a ⟨s, hs⟩ = _root_.IsLocalization.mk' β (t * d) ⟨1, S.one_mem⟩ := hx_eq_mk _ = algebraMap α β (t * d) := by - simpa using (_root_.IsLocalization.mk'_one (S := β) (t * d)) + convert (_root_.IsLocalization.mk'_one (S := β) (t * d)) using 1 rw [hx_eq] have htUnitLoc : IsUnit (algebraMap α β t) := NagataFactoriality.IsLocalization.isUnit_map_of_mem (S := S) (β := β) ht @@ -528,7 +538,7 @@ theorem localization_irreducible_of_irreducible_isLocalization {α β : Type*} _root_.IsLocalization.mk' β b ⟨t, ht⟩ = _root_.IsLocalization.mk' β (s * d) ⟨1, S.one_mem⟩ := hy_eq_mk _ = algebraMap α β (s * d) := by - simpa using (_root_.IsLocalization.mk'_one (S := β) (s * d)) + convert (_root_.IsLocalization.mk'_one (S := β) (s * d)) using 1 rw [hy_eq] have hsUnitLoc : IsUnit (algebraMap α β s) := NagataFactoriality.IsLocalization.isUnit_map_of_mem (S := S) (β := β) hs @@ -547,18 +557,18 @@ theorem localization_irreducible_of_irreducible_isLocalization {α β : Type*} theorem localization_irreducible_of_irreducible {α : Type*} [CommRing α] [IsDomain α] {S : Submonoid α} (hS : ∀ s ∈ S, Prime s ∨ IsUnit s) {p : α} (hp : Irreducible p) (havoid : Avoids S p) : Irreducible (Localization.of (S := S) p) := by - letI : Fact ((0 : α) ∉ S) := submonoidZeroNotMemFact hS - letI : IsDomain (Localization S) := by infer_instance + let : Fact ((0 : α) ∉ S) := submonoidZeroNotMemFact hS + let : IsDomain (Localization S) := by infer_instance simpa [Localization.of] using (localization_irreducible_of_irreducible_isLocalization (β := Localization S) (S := S) hS hp havoid) theorem dvd_of_localization_dvd_isLocalization {α β : Type*} - [CommRing α] [IsDomain α] {S : Submonoid α} [CommRing β] [Algebra α β] [IsDomain β] + [CommRing α] [IsDomain α] {S : Submonoid α} [CommRing β] [Algebra α β] [_root_.IsLocalization S β] (hS : ∀ s ∈ S, Prime s ∨ IsUnit s) {p a : α} (hp : Irreducible p) (havoid : Avoids S p) (hdiv : algebraMap α β p ∣ algebraMap α β a) : p ∣ a := by - letI : Fact ((0 : α) ∉ S) := submonoidZeroNotMemFact hS + let : Fact ((0 : α) ∉ S) := submonoidZeroNotMemFact hS rcases (NagataFactoriality.IsLocalization.dvd_map_iff (S := S) (β := β) (a := p) (b := a)).1 hdiv with ⟨s, hs, hsa⟩ rcases hsa with ⟨c, hc⟩ @@ -587,8 +597,8 @@ theorem dvd_of_localization_dvd_isLocalization {α β : Type*} theorem dvd_of_localization_dvd {α : Type*} [CommRing α] [IsDomain α] {S : Submonoid α} (hS : ∀ s ∈ S, Prime s ∨ IsUnit s) {p a : α} (hp : Irreducible p) (havoid : Avoids S p) (hdiv : Localization.of (S := S) p ∣ Localization.of (S := S) a) : p ∣ a := by - letI : Fact ((0 : α) ∉ S) := submonoidZeroNotMemFact hS - letI : IsDomain (Localization S) := by infer_instance + let : Fact ((0 : α) ∉ S) := submonoidZeroNotMemFact hS + let : IsDomain (Localization S) := by infer_instance simpa [Localization.of] using (dvd_of_localization_dvd_isLocalization (β := Localization S) (S := S) hS hp havoid hdiv) @@ -597,7 +607,7 @@ theorem prime_of_localization_prime_isLocalization {α β : Type*} [CommRing α] [IsDomain α] {S : Submonoid α} [CommRing β] [Algebra α β] [IsDomain β] [_root_.IsLocalization S β] (hS : ∀ s ∈ S, Prime s ∨ IsUnit s) {p : α} (hp : Irreducible p) (havoid : Avoids S p) (hploc : Prime (algebraMap α β p)) : Prime p := by - letI : Fact ((0 : α) ∉ S) := submonoidZeroNotMemFact hS + let : Fact ((0 : α) ∉ S) := submonoidZeroNotMemFact hS refine ⟨hp.ne_zero, hp.not_isUnit, ?_⟩ intro a b hdiv have hlocdiv : algebraMap α β p ∣ algebraMap α β (a * b) := by @@ -613,8 +623,8 @@ theorem prime_of_localization_prime_isLocalization {α β : Type*} theorem prime_of_localization_prime {α : Type*} [CommRing α] [IsDomain α] {S : Submonoid α} (hS : ∀ s ∈ S, Prime s ∨ IsUnit s) {p : α} (hp : Irreducible p) (havoid : Avoids S p) (hploc : Prime (Localization.of (S := S) p)) : Prime p := by - letI : Fact ((0 : α) ∉ S) := submonoidZeroNotMemFact hS - letI : IsDomain (Localization S) := by infer_instance + let : Fact ((0 : α) ∉ S) := submonoidZeroNotMemFact hS + let : IsDomain (Localization S) := by infer_instance simpa [Localization.of] using (prime_of_localization_prime_isLocalization (β := Localization S) (S := S) hS hp havoid hploc) @@ -623,7 +633,7 @@ theorem nagata_key_lemma_isLocalization {α β : Type*} [CommRing α] [IsDomain α] {S : Submonoid α} [CommRing β] [Algebra α β] [IsDomain β] [_root_.IsLocalization S β] (hS : ∀ s ∈ S, Prime s ∨ IsUnit s) [UniqueFactorizationMonoid β] {p : α} (hp : Irreducible p) : Prime p := by - letI : Fact ((0 : α) ∉ S) := submonoidZeroNotMemFact hS + let : Fact ((0 : α) ∉ S) := submonoidZeroNotMemFact hS by_cases hmem : ∃ s : α, s ∈ S ∧ p ∣ s · rcases hmem with ⟨s, hs, hdiv⟩ exact prime_of_irreducible_of_dvd_mem hS hp hs hdiv @@ -643,12 +653,12 @@ theorem nagata_key_lemma {α : Type*} [CommRing α] [IsDomain α] {S : Submonoid (hUFD : @UniqueFactorizationMonoid (Localization S) (by - letI : Fact ((0 : α) ∉ S) := submonoidZeroNotMemFact hS + let : Fact ((0 : α) ∉ S) := submonoidZeroNotMemFact hS infer_instance)) {p : α} (hp : Irreducible p) : Prime p := by - letI : Fact ((0 : α) ∉ S) := submonoidZeroNotMemFact hS - letI : IsDomain (Localization S) := by infer_instance - letI : UniqueFactorizationMonoid (Localization S) := hUFD + let : Fact ((0 : α) ∉ S) := submonoidZeroNotMemFact hS + let : IsDomain (Localization S) := by infer_instance + let : UniqueFactorizationMonoid (Localization S) := hUFD simpa [Localization.of] using (nagata_key_lemma_isLocalization (β := Localization S) (S := S) hS hp) diff --git a/LeanPool/NagataFactoriality/NagataFactoriality/Nagata/Theorem.lean b/LeanPool/NagataFactoriality/NagataFactoriality/Nagata/Theorem.lean index 84c8b212a8..a8c1c56ca7 100644 --- a/LeanPool/NagataFactoriality/NagataFactoriality/Nagata/Theorem.lean +++ b/LeanPool/NagataFactoriality/NagataFactoriality/Nagata/Theorem.lean @@ -1,10 +1,16 @@ /- -Copyright (c) 2026 Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina G. de Oliveira. All rights reserved. +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 -/ import LeanPool.NagataFactoriality.NagataFactoriality.Nagata.Lemmas +/-! +# Theorem + +Supporting results for Nagata’s factoriality theorem. +-/ + namespace NagataFactoriality theorem nagata_theorem {R : Type*} [CommRing R] [IsDomain R] [IsNoetherianRing R] @@ -12,11 +18,11 @@ theorem nagata_theorem {R : Type*} [CommRing R] [IsDomain R] [IsNoetherianRing R (hUFD : @UniqueFactorizationMonoid (Localization S) (by - letI : Fact ((0 : R) ∉ S) := ⟨zero_notMem_of_primeGenerated hS⟩ + let : Fact ((0 : R) ∉ S) := ⟨zero_notMem_of_primeGenerated hS⟩ infer_instance)) : UniqueFactorizationMonoid R := by - letI : Fact ((0 : R) ∉ S) := ⟨zero_notMem_of_primeGenerated hS⟩ - letI : UniqueFactorizationMonoid (Localization S) := hUFD + let : Fact ((0 : R) ∉ S) := ⟨zero_notMem_of_primeGenerated hS⟩ + let : UniqueFactorizationMonoid (Localization S) := hUFD exact ufd_of_factorization_and_primes (hasFactorization_of_noetherian (α := R)) (fun p hp => nagata_key_lemma_primeGenerated_isLocalization @@ -26,7 +32,7 @@ theorem nagata_theorem_isLocalization {R T : Type*} [CommRing R] [IsDomain R] [I (S : Submonoid R) [CommRing T] [Algebra R T] [_root_.IsLocalization S T] [IsDomain T] (hS : PrimeGenerated S) (hUFD : UniqueFactorizationMonoid T) : UniqueFactorizationMonoid R := by - letI : UniqueFactorizationMonoid T := hUFD + let : UniqueFactorizationMonoid T := hUFD exact ufd_of_factorization_and_primes (hasFactorization_of_noetherian (α := R)) (fun p hp => nagata_key_lemma_primeGenerated_isLocalization (S := S) (β := T) hS hp) @@ -37,7 +43,7 @@ theorem nagata_theorem_of_prime_generators {R : Type*} [CommRing R] [IsDomain R] @UniqueFactorizationMonoid (Localization (Submonoid.closure s)) (by let hS : PrimeGenerated (Submonoid.closure s) := primeGenerated_closure_of_primes hs - letI : Fact ((0 : R) ∉ Submonoid.closure s) := ⟨zero_notMem_of_primeGenerated hS⟩ + let : Fact ((0 : R) ∉ Submonoid.closure s) := ⟨zero_notMem_of_primeGenerated hS⟩ infer_instance)) : UniqueFactorizationMonoid R := by exact nagata_theorem (R := R) (Submonoid.closure s) (primeGenerated_closure_of_primes hs) hUFD @@ -57,7 +63,7 @@ theorem nagata_theorem_of_finite_prime_generators {R : Type*} [CommRing R] [IsDo (by let hS : PrimeGenerated (Submonoid.closure (↑s : Set R)) := primeGenerated_closure_finset_of_primes s hs - letI : Fact ((0 : R) ∉ Submonoid.closure (↑s : Set R)) := + let : Fact ((0 : R) ∉ Submonoid.closure (↑s : Set R)) := ⟨zero_notMem_of_primeGenerated hS⟩ infer_instance)) : UniqueFactorizationMonoid R := by @@ -76,11 +82,11 @@ theorem nagata_theorem_of_prime_or_unit {R : Type*} [CommRing R] [IsDomain R] [I (hUFD : @UniqueFactorizationMonoid (Localization S) (by - letI : Fact ((0 : R) ∉ S) := ⟨Submonoid.zero_notMem_of_prime_or_unit hS⟩ + let : Fact ((0 : R) ∉ S) := ⟨Submonoid.zero_notMem_of_prime_or_unit hS⟩ infer_instance)) : UniqueFactorizationMonoid R := by - letI : Fact ((0 : R) ∉ S) := ⟨Submonoid.zero_notMem_of_prime_or_unit hS⟩ - letI : UniqueFactorizationMonoid (Localization S) := hUFD + let : Fact ((0 : R) ∉ S) := ⟨Submonoid.zero_notMem_of_prime_or_unit hS⟩ + let : UniqueFactorizationMonoid (Localization S) := hUFD exact ufd_of_factorization_and_primes (hasFactorization_of_noetherian (α := R)) (fun p hp => nagata_key_lemma_isLocalization @@ -91,7 +97,7 @@ theorem nagata_theorem_of_prime_or_unit_isLocalization {R T : Type*} [_root_.IsLocalization S T] [IsDomain T] (hS : ∀ s ∈ S, Prime s ∨ IsUnit s) (hUFD : UniqueFactorizationMonoid T) : UniqueFactorizationMonoid R := by - letI : UniqueFactorizationMonoid T := hUFD + let : UniqueFactorizationMonoid T := hUFD exact ufd_of_factorization_and_primes (hasFactorization_of_noetherian (α := R)) (fun p hp => nagata_key_lemma_isLocalization (S := S) (β := T) hS hp) From 2035cffd8ab6473666ce5da1ee62744d50dc8bf6 Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Mon, 21 Sep 2026 18:38:59 +0000 Subject: [PATCH 3/8] Complete Nagata Lean 4.34 port and local code checks --- .../NagataFactoriality/Nagata/Lemmas.lean | 8 ++++---- .../NagataFactoriality/Nagata/Theorem.lean | 8 ++++---- 2 files changed, 8 insertions(+), 8 deletions(-) diff --git a/LeanPool/NagataFactoriality/NagataFactoriality/Nagata/Lemmas.lean b/LeanPool/NagataFactoriality/NagataFactoriality/Nagata/Lemmas.lean index 7fa82ca3cd..d6cc3a6ac1 100644 --- a/LeanPool/NagataFactoriality/NagataFactoriality/Nagata/Lemmas.lean +++ b/LeanPool/NagataFactoriality/NagataFactoriality/Nagata/Lemmas.lean @@ -357,7 +357,7 @@ theorem localization_irreducible_of_irreducible_primeGenerated {α : Type*} (β := Localization S) (S := S) hS hp havoid) theorem prime_of_localization_prime_primeGenerated_isLocalization {α β : Type*} - [CommRing α] [IsDomain α] {S : Submonoid α} [CommRing β] [Algebra α β] [IsDomain β] + [CommRing α] [IsDomain α] {S : Submonoid α} [CommRing β] [Algebra α β] [_root_.IsLocalization S β] (hS : PrimeGenerated S) {p : α} (hp : Irreducible p) (havoid : Avoids S p) (hploc : Prime (algebraMap α β p)) : Prime p := by let : Fact ((0 : α) ∉ S) := ⟨zero_notMem_of_primeGenerated hS⟩ @@ -385,7 +385,7 @@ theorem prime_of_localization_prime_primeGenerated {α : Type*} [CommRing α] [I (β := Localization S) (S := S) hS hp havoid hploc) theorem nagata_key_lemma_primeGenerated_isLocalization {α β : Type*} - [CommRing α] [IsDomain α] {S : Submonoid α} [CommRing β] [Algebra α β] [IsDomain β] + [CommRing α] [IsDomain α] {S : Submonoid α} [CommRing β] [Algebra α β] [_root_.IsLocalization S β] (hS : PrimeGenerated S) [UniqueFactorizationMonoid β] {p : α} (hp : Irreducible p) : Prime p := by let : Fact ((0 : α) ∉ S) := ⟨zero_notMem_of_primeGenerated hS⟩ @@ -604,7 +604,7 @@ theorem dvd_of_localization_dvd {α : Type*} [CommRing α] [IsDomain α] {S : Su (β := Localization S) (S := S) hS hp havoid hdiv) theorem prime_of_localization_prime_isLocalization {α β : Type*} - [CommRing α] [IsDomain α] {S : Submonoid α} [CommRing β] [Algebra α β] [IsDomain β] + [CommRing α] [IsDomain α] {S : Submonoid α} [CommRing β] [Algebra α β] [_root_.IsLocalization S β] (hS : ∀ s ∈ S, Prime s ∨ IsUnit s) {p : α} (hp : Irreducible p) (havoid : Avoids S p) (hploc : Prime (algebraMap α β p)) : Prime p := by let : Fact ((0 : α) ∉ S) := submonoidZeroNotMemFact hS @@ -630,7 +630,7 @@ theorem prime_of_localization_prime {α : Type*} [CommRing α] [IsDomain α] {S (β := Localization S) (S := S) hS hp havoid hploc) theorem nagata_key_lemma_isLocalization {α β : Type*} - [CommRing α] [IsDomain α] {S : Submonoid α} [CommRing β] [Algebra α β] [IsDomain β] + [CommRing α] [IsDomain α] {S : Submonoid α} [CommRing β] [Algebra α β] [_root_.IsLocalization S β] (hS : ∀ s ∈ S, Prime s ∨ IsUnit s) [UniqueFactorizationMonoid β] {p : α} (hp : Irreducible p) : Prime p := by let : Fact ((0 : α) ∉ S) := submonoidZeroNotMemFact hS diff --git a/LeanPool/NagataFactoriality/NagataFactoriality/Nagata/Theorem.lean b/LeanPool/NagataFactoriality/NagataFactoriality/Nagata/Theorem.lean index a8c1c56ca7..2bb7897b7d 100644 --- a/LeanPool/NagataFactoriality/NagataFactoriality/Nagata/Theorem.lean +++ b/LeanPool/NagataFactoriality/NagataFactoriality/Nagata/Theorem.lean @@ -30,7 +30,7 @@ theorem nagata_theorem {R : Type*} [CommRing R] [IsDomain R] [IsNoetherianRing R theorem nagata_theorem_isLocalization {R T : Type*} [CommRing R] [IsDomain R] [IsNoetherianRing R] (S : Submonoid R) [CommRing T] [Algebra R T] [_root_.IsLocalization S T] - [IsDomain T] (hS : PrimeGenerated S) (hUFD : UniqueFactorizationMonoid T) : + (hS : PrimeGenerated S) (hUFD : UniqueFactorizationMonoid T) : UniqueFactorizationMonoid R := by let : UniqueFactorizationMonoid T := hUFD exact ufd_of_factorization_and_primes @@ -50,7 +50,7 @@ theorem nagata_theorem_of_prime_generators {R : Type*} [CommRing R] [IsDomain R] theorem nagata_theorem_of_prime_generators_isLocalization {R T : Type*} [CommRing R] [IsDomain R] [IsNoetherianRing R] (s : Set R) [CommRing T] [Algebra R T] - [_root_.IsLocalization (Submonoid.closure s) T] [IsDomain T] + [_root_.IsLocalization (Submonoid.closure s) T] (hs : ∀ q ∈ s, Prime q) (hUFD : UniqueFactorizationMonoid T) : UniqueFactorizationMonoid R := by exact nagata_theorem_isLocalization (R := R) (T := T) (Submonoid.closure s) @@ -71,7 +71,7 @@ theorem nagata_theorem_of_finite_prime_generators {R : Type*} [CommRing R] [IsDo theorem nagata_theorem_of_finite_prime_generators_isLocalization {R T : Type*} [CommRing R] [IsDomain R] [IsNoetherianRing R] (s : Finset R) [CommRing T] [Algebra R T] - [_root_.IsLocalization (Submonoid.closure (↑s : Set R)) T] [IsDomain T] + [_root_.IsLocalization (Submonoid.closure (↑s : Set R)) T] (hs : ∀ q ∈ s, Prime q) (hUFD : UniqueFactorizationMonoid T) : UniqueFactorizationMonoid R := by exact nagata_theorem_of_prime_generators_isLocalization (R := R) (T := T) (s := (↑s : Set R)) @@ -94,7 +94,7 @@ theorem nagata_theorem_of_prime_or_unit {R : Type*} [CommRing R] [IsDomain R] [I theorem nagata_theorem_of_prime_or_unit_isLocalization {R T : Type*} [CommRing R] [IsDomain R] [IsNoetherianRing R] (S : Submonoid R) [CommRing T] [Algebra R T] - [_root_.IsLocalization S T] [IsDomain T] + [_root_.IsLocalization S T] (hS : ∀ s ∈ S, Prime s ∨ IsUnit s) (hUFD : UniqueFactorizationMonoid T) : UniqueFactorizationMonoid R := by let : UniqueFactorizationMonoid T := hUFD From a58605d22e8228ebc20846cd44dfc4a1da8717fb Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Fri, 25 Sep 2026 08:37:56 +0000 Subject: [PATCH 4/8] Migrate Nagata factoriality to public modules --- LeanPool/NagataFactoriality.lean | 43 +++++++++++-------- .../NagataFactoriality.lean | 13 ++++-- .../NagataFactoriality/Applications.lean | 13 ++++-- .../Applications/Examples.lean | 11 +++-- .../Applications/FractionField.lean | 15 ++++--- .../Applications/Gauss.lean | 11 +++-- .../Applications/Laurent.lean | 17 +++++--- .../NagataFactoriality/Basic.lean | 13 ++++-- .../Basic/Divisibility.lean | 9 +++- .../NagataFactoriality/Basic/Noetherian.lean | 9 +++- .../NagataFactoriality/Basic/Ring.lean | 11 +++-- .../NagataFactoriality/Basic/UFD.lean | 9 +++- .../NagataFactoriality/Localization.lean | 13 ++++-- .../Localization/IsLocalization.lean | 9 +++- .../Localization/Localization.lean | 9 +++- .../Localization/MultSet.lean | 7 ++- .../Localization/Properties.lean | 9 +++- .../NagataFactoriality/Nagata.lean | 9 +++- .../NagataFactoriality/Nagata/Lemmas.lean | 13 ++++-- .../NagataFactoriality/Nagata/Theorem.lean | 7 ++- 20 files changed, 175 insertions(+), 75 deletions(-) diff --git a/LeanPool/NagataFactoriality.lean b/LeanPool/NagataFactoriality.lean index 3e2dde0f4c..19b80cc378 100644 --- a/LeanPool/NagataFactoriality.lean +++ b/LeanPool/NagataFactoriality.lean @@ -4,25 +4,28 @@ 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 -/ -import LeanPool.NagataFactoriality.NagataFactoriality -import LeanPool.NagataFactoriality.NagataFactoriality.Applications -import LeanPool.NagataFactoriality.NagataFactoriality.Applications.Examples -import LeanPool.NagataFactoriality.NagataFactoriality.Applications.FractionField -import LeanPool.NagataFactoriality.NagataFactoriality.Applications.Gauss -import LeanPool.NagataFactoriality.NagataFactoriality.Applications.Laurent -import LeanPool.NagataFactoriality.NagataFactoriality.Basic -import LeanPool.NagataFactoriality.NagataFactoriality.Basic.Divisibility -import LeanPool.NagataFactoriality.NagataFactoriality.Basic.Noetherian -import LeanPool.NagataFactoriality.NagataFactoriality.Basic.Ring -import LeanPool.NagataFactoriality.NagataFactoriality.Basic.UFD -import LeanPool.NagataFactoriality.NagataFactoriality.Localization -import LeanPool.NagataFactoriality.NagataFactoriality.Localization.IsLocalization -import LeanPool.NagataFactoriality.NagataFactoriality.Localization.Localization -import LeanPool.NagataFactoriality.NagataFactoriality.Localization.MultSet -import LeanPool.NagataFactoriality.NagataFactoriality.Localization.Properties -import LeanPool.NagataFactoriality.NagataFactoriality.Nagata -import LeanPool.NagataFactoriality.NagataFactoriality.Nagata.Lemmas -import LeanPool.NagataFactoriality.NagataFactoriality.Nagata.Theorem +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 @@ -34,3 +37,5 @@ Main declarations: `NagataFactoriality.nagata_theorem` Tags: commutative-algebra MSC: 13F15 -/ + +@[expose] public section diff --git a/LeanPool/NagataFactoriality/NagataFactoriality.lean b/LeanPool/NagataFactoriality/NagataFactoriality.lean index 6b6cda70ec..f378380fe5 100644 --- a/LeanPool/NagataFactoriality/NagataFactoriality.lean +++ b/LeanPool/NagataFactoriality/NagataFactoriality.lean @@ -3,13 +3,18 @@ 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 -/ -import LeanPool.NagataFactoriality.NagataFactoriality.Basic -import LeanPool.NagataFactoriality.NagataFactoriality.Localization -import LeanPool.NagataFactoriality.NagataFactoriality.Nagata -import LeanPool.NagataFactoriality.NagataFactoriality.Applications +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 diff --git a/LeanPool/NagataFactoriality/NagataFactoriality/Applications.lean b/LeanPool/NagataFactoriality/NagataFactoriality/Applications.lean index 3fe2bc9396..9bc4addf82 100644 --- a/LeanPool/NagataFactoriality/NagataFactoriality/Applications.lean +++ b/LeanPool/NagataFactoriality/NagataFactoriality/Applications.lean @@ -3,13 +3,18 @@ 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 -/ -import LeanPool.NagataFactoriality.NagataFactoriality.Applications.Gauss -import LeanPool.NagataFactoriality.NagataFactoriality.Applications.Laurent -import LeanPool.NagataFactoriality.NagataFactoriality.Applications.FractionField -import LeanPool.NagataFactoriality.NagataFactoriality.Applications.Examples +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 diff --git a/LeanPool/NagataFactoriality/NagataFactoriality/Applications/Examples.lean b/LeanPool/NagataFactoriality/NagataFactoriality/Applications/Examples.lean index fdaf91bf67..68c404cd1b 100644 --- a/LeanPool/NagataFactoriality/NagataFactoriality/Applications/Examples.lean +++ b/LeanPool/NagataFactoriality/NagataFactoriality/Applications/Examples.lean @@ -3,9 +3,12 @@ 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 -/ -import Mathlib.Algebra.EuclideanDomain.Int -import Mathlib.RingTheory.PrincipalIdealDomain -import Mathlib.RingTheory.Polynomial.UniqueFactorization +module + +public import Mathlib.Algebra.EuclideanDomain.Int +public import Mathlib.RingTheory.PrincipalIdealDomain +public import Mathlib.RingTheory.Polynomial.UniqueFactorization + /-! # Examples @@ -13,6 +16,8 @@ import Mathlib.RingTheory.Polynomial.UniqueFactorization Supporting results for Nagata’s factoriality theorem. -/ +@[expose] public section + namespace NagataFactoriality open Polynomial diff --git a/LeanPool/NagataFactoriality/NagataFactoriality/Applications/FractionField.lean b/LeanPool/NagataFactoriality/NagataFactoriality/Applications/FractionField.lean index 0b8582dc09..3d828c70bc 100644 --- a/LeanPool/NagataFactoriality/NagataFactoriality/Applications/FractionField.lean +++ b/LeanPool/NagataFactoriality/NagataFactoriality/Applications/FractionField.lean @@ -3,11 +3,14 @@ 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 -/ -import Mathlib.RingTheory.Localization.Algebra -import Mathlib.RingTheory.Localization.FractionRing -import Mathlib.RingTheory.Polynomial.Basic -import Mathlib.RingTheory.Polynomial.UniqueFactorization -import LeanPool.NagataFactoriality.NagataFactoriality.Nagata.Theorem +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 @@ -38,6 +41,8 @@ with `R[T;T⁻¹]`. then `R[X]` is a UFD, proved by localizing at constant primes and using Nagata's theorem. -/ +@[expose] public section + noncomputable section namespace NagataFactoriality diff --git a/LeanPool/NagataFactoriality/NagataFactoriality/Applications/Gauss.lean b/LeanPool/NagataFactoriality/NagataFactoriality/Applications/Gauss.lean index d486bde547..0b4ec5b265 100644 --- a/LeanPool/NagataFactoriality/NagataFactoriality/Applications/Gauss.lean +++ b/LeanPool/NagataFactoriality/NagataFactoriality/Applications/Gauss.lean @@ -3,9 +3,12 @@ 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 -/ -import Mathlib.RingTheory.Polynomial.Content -import Mathlib.RingTheory.Polynomial.GaussLemma -import Mathlib.RingTheory.Polynomial.UniqueFactorization +module + +public import Mathlib.RingTheory.Polynomial.Content +public import Mathlib.RingTheory.Polynomial.GaussLemma +public import Mathlib.RingTheory.Polynomial.UniqueFactorization + /-! # Gauss @@ -13,6 +16,8 @@ import Mathlib.RingTheory.Polynomial.UniqueFactorization Supporting results for Nagata’s factoriality theorem. -/ +@[expose] public section + namespace NagataFactoriality open Polynomial diff --git a/LeanPool/NagataFactoriality/NagataFactoriality/Applications/Laurent.lean b/LeanPool/NagataFactoriality/NagataFactoriality/Applications/Laurent.lean index 2e7bf83d31..cd5fb2fac9 100644 --- a/LeanPool/NagataFactoriality/NagataFactoriality/Applications/Laurent.lean +++ b/LeanPool/NagataFactoriality/NagataFactoriality/Applications/Laurent.lean @@ -3,12 +3,15 @@ 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 -/ -import Mathlib.Algebra.Polynomial.Laurent -import Mathlib.Algebra.Polynomial.RingDivision -import Mathlib.RingTheory.Localization.Ideal -import Mathlib.RingTheory.Polynomial.UniqueFactorization -import LeanPool.NagataFactoriality.NagataFactoriality.Nagata.Lemmas -import LeanPool.NagataFactoriality.NagataFactoriality.Nagata.Theorem +module + +public import Mathlib.Algebra.Polynomial.Laurent +public import Mathlib.Algebra.Polynomial.RingDivision +public import Mathlib.RingTheory.Localization.Ideal +public import Mathlib.RingTheory.Polynomial.UniqueFactorization +public import LeanPool.NagataFactoriality.NagataFactoriality.Nagata.Lemmas +public import LeanPool.NagataFactoriality.NagataFactoriality.Nagata.Theorem + /-! # Laurent @@ -16,6 +19,8 @@ import LeanPool.NagataFactoriality.NagataFactoriality.Nagata.Theorem Supporting results for Nagata’s factoriality theorem. -/ +@[expose] public section + namespace NagataFactoriality open scoped LaurentPolynomial diff --git a/LeanPool/NagataFactoriality/NagataFactoriality/Basic.lean b/LeanPool/NagataFactoriality/NagataFactoriality/Basic.lean index ed1dfe14f8..fcd183f0cc 100644 --- a/LeanPool/NagataFactoriality/NagataFactoriality/Basic.lean +++ b/LeanPool/NagataFactoriality/NagataFactoriality/Basic.lean @@ -3,13 +3,18 @@ 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 -/ -import LeanPool.NagataFactoriality.NagataFactoriality.Basic.Ring -import LeanPool.NagataFactoriality.NagataFactoriality.Basic.Divisibility -import LeanPool.NagataFactoriality.NagataFactoriality.Basic.Noetherian -import LeanPool.NagataFactoriality.NagataFactoriality.Basic.UFD +module + +public import LeanPool.NagataFactoriality.NagataFactoriality.Basic.Ring +public import LeanPool.NagataFactoriality.NagataFactoriality.Basic.Divisibility +public import LeanPool.NagataFactoriality.NagataFactoriality.Basic.Noetherian +public import LeanPool.NagataFactoriality.NagataFactoriality.Basic.UFD + /-! # Basic Supporting results for Nagata’s factoriality theorem. -/ + +@[expose] public section diff --git a/LeanPool/NagataFactoriality/NagataFactoriality/Basic/Divisibility.lean b/LeanPool/NagataFactoriality/NagataFactoriality/Basic/Divisibility.lean index 87e7d7bf54..f035b408f4 100644 --- a/LeanPool/NagataFactoriality/NagataFactoriality/Basic/Divisibility.lean +++ b/LeanPool/NagataFactoriality/NagataFactoriality/Basic/Divisibility.lean @@ -3,8 +3,11 @@ 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 -/ -import Mathlib.RingTheory.Noetherian.UniqueFactorizationDomain -import LeanPool.NagataFactoriality.NagataFactoriality.Basic.Ring +module + +public import Mathlib.RingTheory.Noetherian.UniqueFactorizationDomain +public import LeanPool.NagataFactoriality.NagataFactoriality.Basic.Ring + /-! # Divisibility @@ -12,6 +15,8 @@ import LeanPool.NagataFactoriality.NagataFactoriality.Basic.Ring Supporting results for Nagata’s factoriality theorem. -/ +@[expose] public section + namespace NagataFactoriality open scoped BigOperators diff --git a/LeanPool/NagataFactoriality/NagataFactoriality/Basic/Noetherian.lean b/LeanPool/NagataFactoriality/NagataFactoriality/Basic/Noetherian.lean index 33620d844d..aa51b0ecf8 100644 --- a/LeanPool/NagataFactoriality/NagataFactoriality/Basic/Noetherian.lean +++ b/LeanPool/NagataFactoriality/NagataFactoriality/Basic/Noetherian.lean @@ -3,8 +3,11 @@ 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 -/ -import Mathlib.RingTheory.Noetherian.UniqueFactorizationDomain -import LeanPool.NagataFactoriality.NagataFactoriality.Basic.Divisibility +module + +public import Mathlib.RingTheory.Noetherian.UniqueFactorizationDomain +public import LeanPool.NagataFactoriality.NagataFactoriality.Basic.Divisibility + /-! # Noetherian @@ -12,6 +15,8 @@ import LeanPool.NagataFactoriality.NagataFactoriality.Basic.Divisibility Supporting results for Nagata’s factoriality theorem. -/ +@[expose] public section + namespace NagataFactoriality theorem hasFactorization_of_noetherian {α : Type*} [CommRing α] [IsDomain α] diff --git a/LeanPool/NagataFactoriality/NagataFactoriality/Basic/Ring.lean b/LeanPool/NagataFactoriality/NagataFactoriality/Basic/Ring.lean index 08ce5a9e56..1a4a875007 100644 --- a/LeanPool/NagataFactoriality/NagataFactoriality/Basic/Ring.lean +++ b/LeanPool/NagataFactoriality/NagataFactoriality/Basic/Ring.lean @@ -3,9 +3,12 @@ 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 -/ -import Mathlib.RingTheory.Noetherian.Basic -import Mathlib.RingTheory.UniqueFactorizationDomain.Basic -import Mathlib.Tactic +module + +public import Mathlib.RingTheory.Noetherian.Basic +public import Mathlib.RingTheory.UniqueFactorizationDomain.Basic +public import Mathlib.Tactic + /-! # Ring @@ -13,6 +16,8 @@ import Mathlib.Tactic Supporting results for Nagata’s factoriality theorem. -/ +@[expose] public section + namespace NagataFactoriality end NagataFactoriality diff --git a/LeanPool/NagataFactoriality/NagataFactoriality/Basic/UFD.lean b/LeanPool/NagataFactoriality/NagataFactoriality/Basic/UFD.lean index 6639e9f336..d2f7d64522 100644 --- a/LeanPool/NagataFactoriality/NagataFactoriality/Basic/UFD.lean +++ b/LeanPool/NagataFactoriality/NagataFactoriality/Basic/UFD.lean @@ -3,8 +3,11 @@ 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 -/ -import Mathlib.RingTheory.UniqueFactorizationDomain.Basic -import LeanPool.NagataFactoriality.NagataFactoriality.Basic.Noetherian +module + +public import Mathlib.RingTheory.UniqueFactorizationDomain.Basic +public import LeanPool.NagataFactoriality.NagataFactoriality.Basic.Noetherian + /-! # UFD @@ -12,6 +15,8 @@ import LeanPool.NagataFactoriality.NagataFactoriality.Basic.Noetherian Supporting results for Nagata’s factoriality theorem. -/ +@[expose] public section + namespace NagataFactoriality theorem ufd_iff_factorization_and_irreducibles_prime {α : Type*} [CommRing α] [IsDomain α] : diff --git a/LeanPool/NagataFactoriality/NagataFactoriality/Localization.lean b/LeanPool/NagataFactoriality/NagataFactoriality/Localization.lean index 0148e1cb9f..12f6fd7518 100644 --- a/LeanPool/NagataFactoriality/NagataFactoriality/Localization.lean +++ b/LeanPool/NagataFactoriality/NagataFactoriality/Localization.lean @@ -3,13 +3,18 @@ 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 -/ -import LeanPool.NagataFactoriality.NagataFactoriality.Localization.MultSet -import LeanPool.NagataFactoriality.NagataFactoriality.Localization.Localization -import LeanPool.NagataFactoriality.NagataFactoriality.Localization.IsLocalization -import LeanPool.NagataFactoriality.NagataFactoriality.Localization.Properties +module + +public import LeanPool.NagataFactoriality.NagataFactoriality.Localization.MultSet +public import LeanPool.NagataFactoriality.NagataFactoriality.Localization.Localization +public import LeanPool.NagataFactoriality.NagataFactoriality.Localization.IsLocalization +public import LeanPool.NagataFactoriality.NagataFactoriality.Localization.Properties + /-! # Localization Supporting results for Nagata’s factoriality theorem. -/ + +@[expose] public section diff --git a/LeanPool/NagataFactoriality/NagataFactoriality/Localization/IsLocalization.lean b/LeanPool/NagataFactoriality/NagataFactoriality/Localization/IsLocalization.lean index f02e2b7a98..d92130235c 100644 --- a/LeanPool/NagataFactoriality/NagataFactoriality/Localization/IsLocalization.lean +++ b/LeanPool/NagataFactoriality/NagataFactoriality/Localization/IsLocalization.lean @@ -3,8 +3,11 @@ 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 -/ -import Mathlib.RingTheory.Localization.Basic -import LeanPool.NagataFactoriality.NagataFactoriality.Localization.MultSet +module + +public import Mathlib.RingTheory.Localization.Basic +public import LeanPool.NagataFactoriality.NagataFactoriality.Localization.MultSet + /-! # IsLocalization @@ -12,6 +15,8 @@ import LeanPool.NagataFactoriality.NagataFactoriality.Localization.MultSet Supporting results for Nagata’s factoriality theorem. -/ +@[expose] public section + namespace NagataFactoriality namespace IsLocalization diff --git a/LeanPool/NagataFactoriality/NagataFactoriality/Localization/Localization.lean b/LeanPool/NagataFactoriality/NagataFactoriality/Localization/Localization.lean index 8d67cf27c9..2afcb86430 100644 --- a/LeanPool/NagataFactoriality/NagataFactoriality/Localization/Localization.lean +++ b/LeanPool/NagataFactoriality/NagataFactoriality/Localization/Localization.lean @@ -3,8 +3,11 @@ 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 -/ -import Mathlib.RingTheory.Localization.Basic -import LeanPool.NagataFactoriality.NagataFactoriality.Localization.MultSet +module + +public import Mathlib.RingTheory.Localization.Basic +public import LeanPool.NagataFactoriality.NagataFactoriality.Localization.MultSet + /-! # Localization @@ -12,6 +15,8 @@ import LeanPool.NagataFactoriality.NagataFactoriality.Localization.MultSet Supporting results for Nagata’s factoriality theorem. -/ +@[expose] public section + namespace NagataFactoriality /-- Localization of a commutative ring at a multiplicative submonoid. -/ diff --git a/LeanPool/NagataFactoriality/NagataFactoriality/Localization/MultSet.lean b/LeanPool/NagataFactoriality/NagataFactoriality/Localization/MultSet.lean index b4ce73995f..b7d4e1b868 100644 --- a/LeanPool/NagataFactoriality/NagataFactoriality/Localization/MultSet.lean +++ b/LeanPool/NagataFactoriality/NagataFactoriality/Localization/MultSet.lean @@ -3,7 +3,10 @@ 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 -/ -import LeanPool.NagataFactoriality.NagataFactoriality.Basic.Divisibility +module + +public import LeanPool.NagataFactoriality.NagataFactoriality.Basic.Divisibility + /-! # MultSet @@ -11,6 +14,8 @@ import LeanPool.NagataFactoriality.NagataFactoriality.Basic.Divisibility Supporting results for Nagata’s factoriality theorem. -/ +@[expose] public section + namespace NagataFactoriality namespace Submonoid diff --git a/LeanPool/NagataFactoriality/NagataFactoriality/Localization/Properties.lean b/LeanPool/NagataFactoriality/NagataFactoriality/Localization/Properties.lean index fedb34d26b..c7faabdce9 100644 --- a/LeanPool/NagataFactoriality/NagataFactoriality/Localization/Properties.lean +++ b/LeanPool/NagataFactoriality/NagataFactoriality/Localization/Properties.lean @@ -3,11 +3,16 @@ 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 -/ -import LeanPool.NagataFactoriality.NagataFactoriality.Localization.Localization -import LeanPool.NagataFactoriality.NagataFactoriality.Localization.IsLocalization +module + +public import LeanPool.NagataFactoriality.NagataFactoriality.Localization.Localization +public import LeanPool.NagataFactoriality.NagataFactoriality.Localization.IsLocalization + /-! # Properties Supporting results for Nagata’s factoriality theorem. -/ + +@[expose] public section diff --git a/LeanPool/NagataFactoriality/NagataFactoriality/Nagata.lean b/LeanPool/NagataFactoriality/NagataFactoriality/Nagata.lean index 998837771f..6f56ae214b 100644 --- a/LeanPool/NagataFactoriality/NagataFactoriality/Nagata.lean +++ b/LeanPool/NagataFactoriality/NagataFactoriality/Nagata.lean @@ -3,11 +3,16 @@ 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 -/ -import LeanPool.NagataFactoriality.NagataFactoriality.Nagata.Lemmas -import LeanPool.NagataFactoriality.NagataFactoriality.Nagata.Theorem +module + +public import LeanPool.NagataFactoriality.NagataFactoriality.Nagata.Lemmas +public import LeanPool.NagataFactoriality.NagataFactoriality.Nagata.Theorem + /-! # Nagata Supporting results for Nagata’s factoriality theorem. -/ + +@[expose] public section diff --git a/LeanPool/NagataFactoriality/NagataFactoriality/Nagata/Lemmas.lean b/LeanPool/NagataFactoriality/NagataFactoriality/Nagata/Lemmas.lean index d6cc3a6ac1..b7feeb7ca2 100644 --- a/LeanPool/NagataFactoriality/NagataFactoriality/Nagata/Lemmas.lean +++ b/LeanPool/NagataFactoriality/NagataFactoriality/Nagata/Lemmas.lean @@ -3,9 +3,12 @@ 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 -/ -import LeanPool.NagataFactoriality.NagataFactoriality.Localization.Properties -import LeanPool.NagataFactoriality.NagataFactoriality.Localization.IsLocalization -import LeanPool.NagataFactoriality.NagataFactoriality.Basic.UFD +module + +public import LeanPool.NagataFactoriality.NagataFactoriality.Localization.Properties +public import LeanPool.NagataFactoriality.NagataFactoriality.Localization.IsLocalization +public import LeanPool.NagataFactoriality.NagataFactoriality.Basic.UFD + /-! # Lemmas @@ -13,6 +16,8 @@ import LeanPool.NagataFactoriality.NagataFactoriality.Basic.UFD Supporting results for Nagata’s factoriality theorem. -/ +@[expose] public section + namespace NagataFactoriality /-- An element avoids a multiplicative set when it divides none of its members. -/ @@ -653,7 +658,7 @@ theorem nagata_key_lemma {α : Type*} [CommRing α] [IsDomain α] {S : Submonoid (hUFD : @UniqueFactorizationMonoid (Localization S) (by - let : Fact ((0 : α) ∉ S) := submonoidZeroNotMemFact hS + let : Fact ((0 : α) ∉ S) := ⟨Submonoid.zero_notMem_of_prime_or_unit hS⟩ infer_instance)) {p : α} (hp : Irreducible p) : Prime p := by let : Fact ((0 : α) ∉ S) := submonoidZeroNotMemFact hS diff --git a/LeanPool/NagataFactoriality/NagataFactoriality/Nagata/Theorem.lean b/LeanPool/NagataFactoriality/NagataFactoriality/Nagata/Theorem.lean index 2bb7897b7d..55c0b673a4 100644 --- a/LeanPool/NagataFactoriality/NagataFactoriality/Nagata/Theorem.lean +++ b/LeanPool/NagataFactoriality/NagataFactoriality/Nagata/Theorem.lean @@ -3,7 +3,10 @@ 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 -/ -import LeanPool.NagataFactoriality.NagataFactoriality.Nagata.Lemmas +module + +public import LeanPool.NagataFactoriality.NagataFactoriality.Nagata.Lemmas + /-! # Theorem @@ -11,6 +14,8 @@ import LeanPool.NagataFactoriality.NagataFactoriality.Nagata.Lemmas Supporting results for Nagata’s factoriality theorem. -/ +@[expose] public section + namespace NagataFactoriality theorem nagata_theorem {R : Type*} [CommRing R] [IsDomain R] [IsNoetherianRing R] From 6757e20742e423fa88a37b27d05dfe9145107575 Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Fri, 25 Sep 2026 18:36:57 +0000 Subject: [PATCH 5/8] Document Nagata proof provenance from upstream history --- LeanPool/projects.yml | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/LeanPool/projects.yml b/LeanPool/projects.yml index d2c067ed7a..10fcddd9b1 100644 --- a/LeanPool/projects.yml +++ b/LeanPool/projects.yml @@ -10126,6 +10126,16 @@ projects: commit: 2efdf7f86085972bd758449ca43c76a2e7bdf4af license: Apache-2.0 status: verified + provenance: AI + provenance_note: >- + Inferred from explicit Copilot coauthor trailers in the pinned upstream history: + 83.5% of surviving noncomment Lean code lines, including 94.8% of the core + localization lemmas and 96.6% of the theorem module, trace to those commits. + Commits 5b1698879b05fc76597723347544cb0b02c268c4 and + ef73ee27e4b0a8d1260350801c6915bfb56b6658 add substantial new proofs, including + prime-generated descent and the fraction-field polynomial application. + Coauthorship records support this classification but do not identify who + wrote each individual line. main_declarations: - NagataFactoriality.nagata_theorem main_results: From 08de88b3aa395e2b761c25ac860e61cd0ecdf379 Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Fri, 25 Sep 2026 18:42:46 +0000 Subject: [PATCH 6/8] Reuse the localization-at-units equivalence in Nagata proofs --- .../Localization/MultSet.lean | 8 ++ .../NagataFactoriality/Nagata/Lemmas.lean | 114 +----------------- 2 files changed, 12 insertions(+), 110 deletions(-) diff --git a/LeanPool/NagataFactoriality/NagataFactoriality/Localization/MultSet.lean b/LeanPool/NagataFactoriality/NagataFactoriality/Localization/MultSet.lean index b7d4e1b868..4e21c64f12 100644 --- a/LeanPool/NagataFactoriality/NagataFactoriality/Localization/MultSet.lean +++ b/LeanPool/NagataFactoriality/NagataFactoriality/Localization/MultSet.lean @@ -22,6 +22,14 @@ namespace Submonoid variable {α : Type*} [CommRing α] [IsDomain α] +/-- Closure under squaring forces every member of a prime-or-unit submonoid to be a unit. -/ +theorem le_isUnit_of_prime_or_unit {S : Submonoid α} + (hS : ∀ s ∈ S, Prime s ∨ IsUnit s) : S ≤ IsUnit.submonoid α := by + intro s hs + rcases hS (s * s) (S.mul_mem hs hs) with hprime | hunit + · exact ((prime_irreducible hprime).isUnit_or_isUnit rfl).elim id id + · exact isUnit_of_mul_isUnit_left hunit + theorem zero_notMem_of_prime_or_unit {S : Submonoid α} (hS : ∀ s ∈ S, Prime s ∨ IsUnit s) : (0 : α) ∉ S := by intro h0 diff --git a/LeanPool/NagataFactoriality/NagataFactoriality/Nagata/Lemmas.lean b/LeanPool/NagataFactoriality/NagataFactoriality/Nagata/Lemmas.lean index b7feeb7ca2..c8b817fff4 100644 --- a/LeanPool/NagataFactoriality/NagataFactoriality/Nagata/Lemmas.lean +++ b/LeanPool/NagataFactoriality/NagataFactoriality/Nagata/Lemmas.lean @@ -448,116 +448,10 @@ theorem localization_irreducible_of_irreducible_isLocalization {α β : Type*} (S := S) (β := β) (a := p) (b := 1)).1 hdiv' with ⟨s, hs, hps⟩ exact havoid s hs (by simpa using hps) · intro x y hxy - obtain ⟨a, s, hs, rfl⟩ := NagataFactoriality.IsLocalization.surj (S := S) (β := β) x - obtain ⟨b, t, ht, rfl⟩ := NagataFactoriality.IsLocalization.surj (S := S) (β := β) y - have hprod : p * (s * t) = a * b := by - have hEq : - algebraMap α β p = - _root_.IsLocalization.mk' β (a * b) ⟨s * t, S.mul_mem hs ht⟩ := by - calc - algebraMap α β p = - _root_.IsLocalization.mk' β a ⟨s, hs⟩ * _root_.IsLocalization.mk' β b ⟨t, ht⟩ := hxy - _ = _root_.IsLocalization.mk' β (a * b) ⟨s * t, S.mul_mem hs ht⟩ := by - simpa using (_root_.IsLocalization.mk'_mul - (M := S) (S := β) a b ⟨s, hs⟩ ⟨t, ht⟩).symm - have hEq' : - _root_.IsLocalization.mk' β p ⟨1, S.one_mem⟩ = - _root_.IsLocalization.mk' β (a * b) ⟨s * t, S.mul_mem hs ht⟩ := by - calc - _root_.IsLocalization.mk' β p ⟨1, S.one_mem⟩ = algebraMap α β p := by - convert (_root_.IsLocalization.mk'_one (S := β) p) using 1 - _ = _root_.IsLocalization.mk' β (a * b) ⟨s * t, S.mul_mem hs ht⟩ := hEq - simpa [mul_one] using - (NagataFactoriality.IsLocalization.mk'_eq_iff - (S := S) (β := β) (a := p) (b := a * b) - (s := 1) (t := s * t) S.one_mem (S.mul_mem hs ht)).1 hEq' - rcases hS (s * t) (S.mul_mem hs ht) with hstPrime | hstUnit - · have hstdiv : s * t ∣ a * b := by - refine ⟨p, ?_⟩ - calc - a * b = p * (s * t) := hprod.symm - _ = (s * t) * p := by ac_rfl - rcases hstPrime.2.2 a b hstdiv with hdiva | hdivb - · rcases hdiva with ⟨d, hd⟩ - have hst0 : s * t ≠ 0 := hstPrime.ne_zero - have hp_eq : p = d * b := by - apply mul_left_cancel₀ hst0 - calc - (s * t) * p = p * (s * t) := by ac_rfl - _ = a * b := hprod - _ = ((s * t) * d) * b := by rw [hd] - _ = (s * t) * (d * b) := by ac_rfl - rcases hp.isUnit_or_isUnit hp_eq with hdUnit | hbUnit - · left - have hx_eq_mk : - _root_.IsLocalization.mk' β a ⟨s, hs⟩ = - _root_.IsLocalization.mk' β (t * d) ⟨1, S.one_mem⟩ := by - apply (NagataFactoriality.IsLocalization.mk'_eq_iff - (S := S) (β := β) (a := a) (b := t * d) - (s := s) (t := 1) hs S.one_mem).2 - calc - a * 1 = a := by simp - _ = s * t * d := by rw [hd] - _ = (t * d) * s := by ac_rfl - have hx_eq : _root_.IsLocalization.mk' β a ⟨s, hs⟩ = algebraMap α β (t * d) := by - calc - _root_.IsLocalization.mk' β a ⟨s, hs⟩ = - _root_.IsLocalization.mk' β (t * d) ⟨1, S.one_mem⟩ := hx_eq_mk - _ = algebraMap α β (t * d) := by - convert (_root_.IsLocalization.mk'_one (S := β) (t * d)) using 1 - rw [hx_eq] - have htUnitLoc : IsUnit (algebraMap α β t) := - NagataFactoriality.IsLocalization.isUnit_map_of_mem (S := S) (β := β) ht - have hdUnitLoc : IsUnit (algebraMap α β d) := - NagataFactoriality.IsLocalization.isUnit_map_of_isUnit (β := β) hdUnit - simpa [map_mul] using isUnit_mul htUnitLoc hdUnitLoc - · right - exact NagataFactoriality.IsLocalization.isUnit_mk'_of_isUnit - (S := S) (β := β) hbUnit ht - · rcases hdivb with ⟨d, hd⟩ - have hst0 : s * t ≠ 0 := hstPrime.ne_zero - have hp_eq : p = a * d := by - apply mul_left_cancel₀ hst0 - calc - (s * t) * p = p * (s * t) := by ac_rfl - _ = a * b := hprod - _ = a * ((s * t) * d) := by rw [hd] - _ = (s * t) * (a * d) := by ac_rfl - rcases hp.isUnit_or_isUnit hp_eq with haUnit | hdUnit - · left - exact NagataFactoriality.IsLocalization.isUnit_mk'_of_isUnit - (S := S) (β := β) haUnit hs - · right - have hy_eq_mk : - _root_.IsLocalization.mk' β b ⟨t, ht⟩ = - _root_.IsLocalization.mk' β (s * d) ⟨1, S.one_mem⟩ := by - apply (NagataFactoriality.IsLocalization.mk'_eq_iff - (S := S) (β := β) (a := b) (b := s * d) - (s := t) (t := 1) ht S.one_mem).2 - calc - b * 1 = b := by simp - _ = s * t * d := by rw [hd] - _ = (s * d) * t := by ac_rfl - have hy_eq : _root_.IsLocalization.mk' β b ⟨t, ht⟩ = algebraMap α β (s * d) := by - calc - _root_.IsLocalization.mk' β b ⟨t, ht⟩ = - _root_.IsLocalization.mk' β (s * d) ⟨1, S.one_mem⟩ := hy_eq_mk - _ = algebraMap α β (s * d) := by - convert (_root_.IsLocalization.mk'_one (S := β) (s * d)) using 1 - rw [hy_eq] - have hsUnitLoc : IsUnit (algebraMap α β s) := - NagataFactoriality.IsLocalization.isUnit_map_of_mem (S := S) (β := β) hs - have hdUnitLoc : IsUnit (algebraMap α β d) := - NagataFactoriality.IsLocalization.isUnit_map_of_isUnit (β := β) hdUnit - simpa [map_mul] using isUnit_mul hsUnitLoc hdUnitLoc - · have hassoc : Associated p (a * b) := by - simpa [hprod] using associated_mul_unit_right p (s * t) hstUnit - have habIrred : Irreducible (a * b) := hassoc.irreducible hp - exact (habIrred.isUnit_or_isUnit rfl).elim - (fun haUnit => Or.inl <| - NagataFactoriality.IsLocalization.isUnit_mk'_of_isUnit (S := S) (β := β) haUnit hs) - (fun hbUnit => Or.inr <| - NagataFactoriality.IsLocalization.isUnit_mk'_of_isUnit (S := S) (β := β) hbUnit ht) + let e : α ≃ₐ[α] β := + _root_.IsLocalization.atUnits α S (Submonoid.le_isUnit_of_prime_or_unit hS) + have hmap : Irreducible (e p) := (MulEquiv.irreducible_iff e).mpr hp + exact hmap.isUnit_or_isUnit hxy theorem localization_irreducible_of_irreducible {α : Type*} [CommRing α] [IsDomain α] {S : Submonoid α} (hS : ∀ s ∈ S, Prime s ∨ IsUnit s) {p : α} (hp : Irreducible p) From 386caddb425214968c530b1283054465dbcf5d17 Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Sat, 26 Sep 2026 04:25:11 +0000 Subject: [PATCH 7/8] Refactor Nagata localization transport through existing equivalences --- .../Localization/Localization.lean | 74 +++----------- .../NagataFactoriality/Nagata/Lemmas.lean | 97 ++++--------------- 2 files changed, 31 insertions(+), 140 deletions(-) diff --git a/LeanPool/NagataFactoriality/NagataFactoriality/Localization/Localization.lean b/LeanPool/NagataFactoriality/NagataFactoriality/Localization/Localization.lean index 2afcb86430..0d958ff929 100644 --- a/LeanPool/NagataFactoriality/NagataFactoriality/Localization/Localization.lean +++ b/LeanPool/NagataFactoriality/NagataFactoriality/Localization/Localization.lean @@ -5,8 +5,7 @@ Authors: Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina G. de Oliveira -/ module -public import Mathlib.RingTheory.Localization.Basic -public import LeanPool.NagataFactoriality.NagataFactoriality.Localization.MultSet +public import LeanPool.NagataFactoriality.NagataFactoriality.Localization.IsLocalization /-! @@ -80,31 +79,15 @@ theorem algebraMap_injective : Function.Injective (algebraMap α (Localization S theorem mk_eq_iff {a b s t : α} (hs : s ∈ S) (ht : t ∈ S) : mk (S := S) a s hs = mk (S := S) b t ht ↔ a * t = b * s := by - constructor - · intro h - have h' : - algebraMap α (Localization S) (a * t) = algebraMap α (Localization S) (b * s) := by - have h'' : - IsLocalization.mk' (Localization S) a ⟨s, hs⟩ = - IsLocalization.mk' (Localization S) b ⟨t, ht⟩ := by - simpa [mk, _root_.Localization.mk_eq_mk'_apply] using h - exact (IsLocalization.mk'_eq_iff_eq' (M := S) (S := Localization S)).1 h'' - exact algebraMap_injective (S := S) <| - by simpa [map_mul, mul_assoc, mul_left_comm, mul_comm] using h' - · intro h - have h' : - IsLocalization.mk' (Localization S) a ⟨s, hs⟩ = - IsLocalization.mk' (Localization S) b ⟨t, ht⟩ := by - exact IsLocalization.mk'_eq_of_eq' (M := S) (S := Localization S) <| - by simpa [mul_assoc, mul_left_comm, mul_comm] using h.symm - simpa [mk, _root_.Localization.mk_eq_mk'_apply] using h' + simpa only [mk, _root_.Localization.mk_eq_mk'_apply] using + (NagataFactoriality.IsLocalization.mk'_eq_iff (S := S) (β := Localization S) hs ht) theorem of_eq_iff (a b : α) : of (S := S) a = of (S := S) b ↔ a = b := (algebraMap_injective (S := S)).eq_iff theorem mk_eq_zero_iff {a s : α} (hs : s ∈ S) : mk (S := S) a s hs = 0 ↔ a = 0 := by - have h := mk_eq_iff (S := S) (a := a) (b := 0) (s := s) (t := 1) hs S.one_mem - simpa [of] using h + simp only [mk, _root_.Localization.mk_eq_mk'_apply, + NagataFactoriality.IsLocalization.mk'_eq_zero_iff (S := S) (β := Localization S) hs] @[simp] theorem of_eq_zero_iff (a : α) : of (S := S) a = 0 ↔ a = 0 := by change algebraMap α (Localization S) a = 0 ↔ a = 0 @@ -121,8 +104,7 @@ end Nonzero @[simp] theorem of_mul_mk (a b s : α) (hs : s ∈ S) : of (S := S) a * mk (S := S) b s hs = mk (S := S) (a * b) s hs := by - simpa [mk, of, _root_.Localization.mk_eq_mk'_apply] using - (IsLocalization.mul_mk'_eq_mk'_of_mul (M := S) (S := Localization S) a b ⟨s, hs⟩) + simp [mk, of, _root_.Localization.mk_eq_mk'_apply] @[simp] theorem mk_mul_of (a b s : α) (hs : s ∈ S) : mk (S := S) a s hs * of (S := S) b = mk (S := S) (a * b) s hs := by @@ -134,10 +116,8 @@ end Nonzero theorem isUnit_mk_of_mem {a s : α} (ha : a ∈ S) (hs : s ∈ S) : IsUnit (mk (S := S) a s hs) := by - apply isUnit_iff_exists_inv.2 - refine ⟨mk (S := S) s a ha, ?_⟩ - simpa [mk, _root_.Localization.mk_eq_mk'_apply] using - (IsLocalization.mk'_mul_mk'_eq_one' (M := S) (S := Localization S) a ⟨s, hs⟩ ha) + simpa only [mk, _root_.Localization.mk_eq_mk'_apply] using + (NagataFactoriality.IsLocalization.isUnit_mk'_of_mem (β := Localization S) ha hs) theorem isUnit_of_mem {s : α} (hs : s ∈ S) : IsUnit (of (S := S) s) := by simpa [of] using (IsLocalization.map_units (S := Localization S) ⟨s, hs⟩) @@ -147,13 +127,8 @@ theorem isUnit_of_isUnit {a : α} (ha : IsUnit a) : IsUnit (of (S := S) a) := theorem isUnit_mk_of_isUnit {a s : α} (ha : IsUnit a) (hs : s ∈ S) : IsUnit (mk (S := S) a s hs) := by - have hmk : mk (S := S) a s hs = of (S := S) a * mk (S := S) 1 s hs := by - calc - mk (S := S) a s hs = mk (S := S) (a * 1) s hs := by simp - _ = of (S := S) a * mk (S := S) 1 s hs := by - rw [← of_mul_mk (S := S) a 1 s hs] - rw [hmk] - exact isUnit_mul (isUnit_of_isUnit (S := S) ha) (isUnit_mk_of_mem (S := S) S.one_mem hs) + simpa only [mk, _root_.Localization.mk_eq_mk'_apply] using + (NagataFactoriality.IsLocalization.isUnit_mk'_of_isUnit (β := Localization S) ha hs) section Nonzero @@ -161,34 +136,7 @@ variable [IsDomain α] [Fact ((0 : α) ∉ S)] theorem dvd_of_iff {a b : α} : of (S := S) a ∣ of (S := S) b ↔ ∃ s : α, s ∈ S ∧ a ∣ s * b := by - constructor - · rintro ⟨x, hx⟩ - obtain ⟨c, s, hs, rfl⟩ := surj (S := S) x - refine ⟨s, hs, ?_⟩ - have hEq : of (S := S) b = mk (S := S) (a * c) s hs := by - calc - of (S := S) b = of (S := S) a * mk (S := S) c s hs := hx - _ = mk (S := S) (a * c) s hs := of_mul_mk (S := S) a c s hs - have hCross : - algebraMap α (Localization S) (b * s) = algebraMap α (Localization S) (a * c) := by - have hCross' : - of (S := S) b * algebraMap α (Localization S) s = - algebraMap α (Localization S) (a * c) := by - exact (IsLocalization.eq_mk'_iff_mul_eq (M := S) (S := Localization S) - (z := of (S := S) b) (x := a * c) (y := ⟨s, hs⟩)).1 <| - by simpa [mk, of, _root_.Localization.mk_eq_mk'_apply] using hEq - simpa [of, map_mul, mul_assoc, mul_left_comm, mul_comm] using hCross' - have hEq' : b * s = a * c := (algebraMap_injective (S := S)) hCross - exact ⟨c, by simpa [mul_comm] using hEq'⟩ - · rintro ⟨s, hs, c, hc⟩ - refine ⟨mk (S := S) c s hs, ?_⟩ - symm - calc - of (S := S) a * mk (S := S) c s hs = mk (S := S) (a * c) s hs := - of_mul_mk (S := S) a c s hs - _ = of (S := S) b := by - apply (mk_eq_iff (S := S) (hs := hs) (ht := S.one_mem)).2 - simpa [mul_assoc, mul_left_comm, mul_comm] using hc.symm + exact NagataFactoriality.IsLocalization.dvd_map_iff (S := S) (β := Localization S) end Nonzero diff --git a/LeanPool/NagataFactoriality/NagataFactoriality/Nagata/Lemmas.lean b/LeanPool/NagataFactoriality/NagataFactoriality/Nagata/Lemmas.lean index c8b817fff4..8f135cfdde 100644 --- a/LeanPool/NagataFactoriality/NagataFactoriality/Nagata/Lemmas.lean +++ b/LeanPool/NagataFactoriality/NagataFactoriality/Nagata/Lemmas.lean @@ -208,7 +208,7 @@ theorem multiset_prod_mem_of_factors {α : Type*} [CommMonoid α] {S : Submonoid simpa using S.mul_mem hq (ih htail) theorem split_prime_factors_of_mul_eq {α : Type*} [CommRing α] [IsDomain α] - {f : Multiset α} (hf : ∀ q ∈ f, Prime q) {p a b : α} (_hp : Irreducible p) + {f : Multiset α} (hf : ∀ q ∈ f, Prime q) {p a b : α} (hEq : p * f.prod = a * b) : ∃ f₁ f₂ : Multiset α, ∃ a' b' : α, f₁ + f₂ = f ∧ @@ -318,7 +318,7 @@ theorem localization_irreducible_of_irreducible_primeGenerated_isLocalization { (S := S) (β := β) (a := p) (b := a * b) (s := 1) (t := s * t) S.one_mem (S.mul_mem hs ht)).1 hmk rcases hS (s * t) (S.mul_mem hs ht) with ⟨f, hf, hfprod⟩ - rcases split_prime_factors_of_mul_eq (fun q hq => (hf q hq).2) hp (by simpa [hfprod] using hEq) + rcases split_prime_factors_of_mul_eq (fun q hq => (hf q hq).2) (by simpa [hfprod] using hEq) with ⟨f₁, f₂, a', b', hpart, ha, hb, hpab⟩ rcases hp.isUnit_or_isUnit hpab with haUnit | hbUnit · left @@ -426,32 +426,16 @@ theorem nagata_key_lemma_primeGenerated {α : Type*} [CommRing α] [IsDomain α] theorem prime_of_irreducible_of_dvd_mem {α : Type*} [CommRing α] [IsDomain α] {S : Submonoid α} (hS : ∀ s ∈ S, Prime s ∨ IsUnit s) {p s : α} (hp : Irreducible p) (hs : s ∈ S) (hdiv : p ∣ s) : Prime p := by - rcases hS s hs with hsPrime | hsUnit - · have hsIrred : Irreducible s := prime_irreducible hsPrime - have hassoc : Associated p s := associated_of_irreducible_of_dvd hp hsIrred hdiv - exact prime_of_associated hsPrime (associated_symm hassoc) - · exact False.elim (hp.not_isUnit (isUnit_of_dvd_unit hdiv hsUnit)) + exact (hp.not_isUnit (isUnit_of_dvd_unit hdiv + (Submonoid.le_isUnit_of_prime_or_unit hS hs))).elim theorem localization_irreducible_of_irreducible_isLocalization {α β : Type*} [CommRing α] [IsDomain α] {S : Submonoid α} [CommRing β] [Algebra α β] [_root_.IsLocalization S β] (hS : ∀ s ∈ S, Prime s ∨ IsUnit s) {p : α} - (hp : Irreducible p) (havoid : Avoids S p) : Irreducible (algebraMap α β p) := by - let : Fact ((0 : α) ∉ S) := submonoidZeroNotMemFact hS - refine ⟨?_, ?_⟩ - · intro hunit - have hdiv : algebraMap α β p ∣ (1 : β) := by - rcases isUnit_iff_exists_inv.mp hunit with ⟨x, hx⟩ - exact ⟨x, hx.symm⟩ - have hdiv' : algebraMap α β p ∣ algebraMap α β (1 : α) := by - simpa using hdiv - rcases (NagataFactoriality.IsLocalization.dvd_map_iff - (S := S) (β := β) (a := p) (b := 1)).1 hdiv' with ⟨s, hs, hps⟩ - exact havoid s hs (by simpa using hps) - · intro x y hxy - let e : α ≃ₐ[α] β := - _root_.IsLocalization.atUnits α S (Submonoid.le_isUnit_of_prime_or_unit hS) - have hmap : Irreducible (e p) := (MulEquiv.irreducible_iff e).mpr hp - exact hmap.isUnit_or_isUnit hxy + (hp : Irreducible p) (_havoid : Avoids S p) : Irreducible (algebraMap α β p) := by + let e : α ≃ₐ[α] β := + _root_.IsLocalization.atUnits α S (Submonoid.le_isUnit_of_prime_or_unit hS) + exact (MulEquiv.irreducible_iff e).mpr hp theorem localization_irreducible_of_irreducible {α : Type*} [CommRing α] [IsDomain α] {S : Submonoid α} (hS : ∀ s ∈ S, Prime s ∨ IsUnit s) {p : α} (hp : Irreducible p) @@ -465,33 +449,11 @@ theorem localization_irreducible_of_irreducible {α : Type*} [CommRing α] [IsDo theorem dvd_of_localization_dvd_isLocalization {α β : Type*} [CommRing α] [IsDomain α] {S : Submonoid α} [CommRing β] [Algebra α β] [_root_.IsLocalization S β] (hS : ∀ s ∈ S, Prime s ∨ IsUnit s) {p a : α} - (hp : Irreducible p) (havoid : Avoids S p) (hdiv : algebraMap α β p ∣ algebraMap α β a) : + (_hp : Irreducible p) (_havoid : Avoids S p) (hdiv : algebraMap α β p ∣ algebraMap α β a) : p ∣ a := by - let : Fact ((0 : α) ∉ S) := submonoidZeroNotMemFact hS - rcases (NagataFactoriality.IsLocalization.dvd_map_iff - (S := S) (β := β) (a := p) (b := a)).1 hdiv with ⟨s, hs, hsa⟩ - rcases hsa with ⟨c, hc⟩ - rcases hS s hs with hsPrime | hsUnit - · have hsdiv : s ∣ p * c := ⟨a, hc.symm⟩ - rcases hsPrime.2.2 p c hsdiv with hsp | hsc - · have hsIrred : Irreducible s := prime_irreducible hsPrime - have hassoc : Associated s p := associated_of_irreducible_of_dvd hsIrred hp hsp - exact False.elim (havoid s hs (dvd_of_associated (associated_symm hassoc))) - · rcases hsc with ⟨d, hd⟩ - refine ⟨d, ?_⟩ - have hs0 : s ≠ 0 := hsPrime.ne_zero - have hcancel : s * a = s * (p * d) := by - calc - s * a = p * c := hc - _ = p * (s * d) := by rw [hd] - _ = s * (p * d) := by ac_rfl - exact mul_left_cancel₀ hs0 hcancel - · rcases hsUnit with ⟨u, rfl⟩ - refine ⟨(↑u⁻¹ : α) * c, ?_⟩ - calc - a = (↑u⁻¹ : α) * ((u : α) * a) := by simp - _ = (↑u⁻¹ : α) * (p * c) := by rw [hc] - _ = p * ((↑u⁻¹ : α) * c) := by ac_rfl + let e : α ≃ₐ[α] β := + _root_.IsLocalization.atUnits α S (Submonoid.le_isUnit_of_prime_or_unit hS) + exact (map_dvd_iff e).mp hdiv theorem dvd_of_localization_dvd {α : Type*} [CommRing α] [IsDomain α] {S : Submonoid α} (hS : ∀ s ∈ S, Prime s ∨ IsUnit s) {p a : α} (hp : Irreducible p) (havoid : Avoids S p) @@ -505,19 +467,10 @@ theorem dvd_of_localization_dvd {α : Type*} [CommRing α] [IsDomain α] {S : Su theorem prime_of_localization_prime_isLocalization {α β : Type*} [CommRing α] [IsDomain α] {S : Submonoid α} [CommRing β] [Algebra α β] [_root_.IsLocalization S β] (hS : ∀ s ∈ S, Prime s ∨ IsUnit s) {p : α} - (hp : Irreducible p) (havoid : Avoids S p) (hploc : Prime (algebraMap α β p)) : Prime p := by - let : Fact ((0 : α) ∉ S) := submonoidZeroNotMemFact hS - refine ⟨hp.ne_zero, hp.not_isUnit, ?_⟩ - intro a b hdiv - have hlocdiv : algebraMap α β p ∣ algebraMap α β (a * b) := by - rcases hdiv with ⟨c, hc⟩ - exact ⟨algebraMap α β c, by simp [map_mul, hc]⟩ - rcases hploc.2.2 (algebraMap α β a) (algebraMap α β b) - (by simpa [map_mul] using hlocdiv) with hpa | hpb - · left - exact dvd_of_localization_dvd_isLocalization (β := β) (S := S) hS hp havoid hpa - · right - exact dvd_of_localization_dvd_isLocalization (β := β) (S := S) hS hp havoid hpb + (_hp : Irreducible p) (_havoid : Avoids S p) (hploc : Prime (algebraMap α β p)) : Prime p := by + let e : α ≃ₐ[α] β := + _root_.IsLocalization.atUnits α S (Submonoid.le_isUnit_of_prime_or_unit hS) + exact (MulEquiv.prime_iff e).mp hploc theorem prime_of_localization_prime {α : Type*} [CommRing α] [IsDomain α] {S : Submonoid α} (hS : ∀ s ∈ S, Prime s ∨ IsUnit s) {p : α} (hp : Irreducible p) (havoid : Avoids S p) @@ -532,20 +485,10 @@ theorem nagata_key_lemma_isLocalization {α β : Type*} [CommRing α] [IsDomain α] {S : Submonoid α} [CommRing β] [Algebra α β] [_root_.IsLocalization S β] (hS : ∀ s ∈ S, Prime s ∨ IsUnit s) [UniqueFactorizationMonoid β] {p : α} (hp : Irreducible p) : Prime p := by - let : Fact ((0 : α) ∉ S) := submonoidZeroNotMemFact hS - by_cases hmem : ∃ s : α, s ∈ S ∧ p ∣ s - · rcases hmem with ⟨s, hs, hdiv⟩ - exact prime_of_irreducible_of_dvd_mem hS hp hs hdiv - · have havoid : Avoids S p := by - intro s hs hdiv - exact hmem ⟨s, hs, hdiv⟩ - have hlocIrred : Irreducible (algebraMap α β p) := - localization_irreducible_of_irreducible_isLocalization - (β := β) (S := S) hS hp havoid - have hlocPrime : Prime (algebraMap α β p) := - (UniqueFactorizationMonoid.irreducible_iff_prime).mp hlocIrred - exact prime_of_localization_prime_isLocalization - (β := β) (S := S) hS hp havoid hlocPrime + let e : α ≃ₐ[α] β := + _root_.IsLocalization.atUnits α S (Submonoid.le_isUnit_of_prime_or_unit hS) + exact (MulEquiv.prime_iff e).mp + (UniqueFactorizationMonoid.irreducible_iff_prime.mp ((MulEquiv.irreducible_iff e).mpr hp)) theorem nagata_key_lemma {α : Type*} [CommRing α] [IsDomain α] {S : Submonoid α} (hS : ∀ s ∈ S, Prime s ∨ IsUnit s) From b42d9df2a6973d6fafd69f1ea791380e25141845 Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Sat, 26 Sep 2026 17:51:30 +0000 Subject: [PATCH 8/8] refactor(NagataFactoriality): remove redundant localization premises --- .../Basic/Divisibility.lean | 16 --------------- .../NagataFactoriality/Nagata/Lemmas.lean | 20 +++++++++---------- .../NagataFactoriality/Nagata/Theorem.lean | 6 ------ 3 files changed, 10 insertions(+), 32 deletions(-) diff --git a/LeanPool/NagataFactoriality/NagataFactoriality/Basic/Divisibility.lean b/LeanPool/NagataFactoriality/NagataFactoriality/Basic/Divisibility.lean index f035b408f4..f0696f0dd8 100644 --- a/LeanPool/NagataFactoriality/NagataFactoriality/Basic/Divisibility.lean +++ b/LeanPool/NagataFactoriality/NagataFactoriality/Basic/Divisibility.lean @@ -21,22 +21,6 @@ namespace NagataFactoriality open scoped BigOperators -/-- The product of a finite list, defined recursively. -/ -def listProd {α : Type*} [CommMonoid α] : List α → α - | [] => 1 - | a :: as => a * listProd as - -@[simp] theorem listProd_nil {α : Type*} [CommMonoid α] : listProd ([] : List α) = 1 := rfl - -@[simp] theorem listProd_cons {α : Type*} [CommMonoid α] (a : α) (as : List α) : - listProd (a :: as) = a * listProd as := rfl - -theorem listProd_append {α : Type*} [CommMonoid α] (xs ys : List α) : - listProd (xs ++ ys) = listProd xs * listProd ys := by - induction xs with - | nil => simp [listProd] - | cons x xs ih => simp [listProd, ih, mul_assoc] - theorem dvd_refl {α : Type*} [CommMonoid α] (a : α) : a ∣ a := dvd_rfl theorem dvd_trans {α : Type*} [CommMonoid α] {a b c : α} : diff --git a/LeanPool/NagataFactoriality/NagataFactoriality/Nagata/Lemmas.lean b/LeanPool/NagataFactoriality/NagataFactoriality/Nagata/Lemmas.lean index 8f135cfdde..6f9fb0f44b 100644 --- a/LeanPool/NagataFactoriality/NagataFactoriality/Nagata/Lemmas.lean +++ b/LeanPool/NagataFactoriality/NagataFactoriality/Nagata/Lemmas.lean @@ -432,54 +432,54 @@ theorem prime_of_irreducible_of_dvd_mem {α : Type*} [CommRing α] [IsDomain α] theorem localization_irreducible_of_irreducible_isLocalization {α β : Type*} [CommRing α] [IsDomain α] {S : Submonoid α} [CommRing β] [Algebra α β] [_root_.IsLocalization S β] (hS : ∀ s ∈ S, Prime s ∨ IsUnit s) {p : α} - (hp : Irreducible p) (_havoid : Avoids S p) : Irreducible (algebraMap α β p) := by + (hp : Irreducible p) : Irreducible (algebraMap α β p) := by let e : α ≃ₐ[α] β := _root_.IsLocalization.atUnits α S (Submonoid.le_isUnit_of_prime_or_unit hS) exact (MulEquiv.irreducible_iff e).mpr hp theorem localization_irreducible_of_irreducible {α : Type*} [CommRing α] [IsDomain α] - {S : Submonoid α} (hS : ∀ s ∈ S, Prime s ∨ IsUnit s) {p : α} (hp : Irreducible p) - (havoid : Avoids S p) : Irreducible (Localization.of (S := S) p) := by + {S : Submonoid α} (hS : ∀ s ∈ S, Prime s ∨ IsUnit s) {p : α} (hp : Irreducible p) : + Irreducible (Localization.of (S := S) p) := by let : Fact ((0 : α) ∉ S) := submonoidZeroNotMemFact hS let : IsDomain (Localization S) := by infer_instance simpa [Localization.of] using (localization_irreducible_of_irreducible_isLocalization - (β := Localization S) (S := S) hS hp havoid) + (β := Localization S) (S := S) hS hp) theorem dvd_of_localization_dvd_isLocalization {α β : Type*} [CommRing α] [IsDomain α] {S : Submonoid α} [CommRing β] [Algebra α β] [_root_.IsLocalization S β] (hS : ∀ s ∈ S, Prime s ∨ IsUnit s) {p a : α} - (_hp : Irreducible p) (_havoid : Avoids S p) (hdiv : algebraMap α β p ∣ algebraMap α β a) : + (hdiv : algebraMap α β p ∣ algebraMap α β a) : p ∣ a := by let e : α ≃ₐ[α] β := _root_.IsLocalization.atUnits α S (Submonoid.le_isUnit_of_prime_or_unit hS) exact (map_dvd_iff e).mp hdiv theorem dvd_of_localization_dvd {α : Type*} [CommRing α] [IsDomain α] {S : Submonoid α} - (hS : ∀ s ∈ S, Prime s ∨ IsUnit s) {p a : α} (hp : Irreducible p) (havoid : Avoids S p) + (hS : ∀ s ∈ S, Prime s ∨ IsUnit s) {p a : α} (hdiv : Localization.of (S := S) p ∣ Localization.of (S := S) a) : p ∣ a := by let : Fact ((0 : α) ∉ S) := submonoidZeroNotMemFact hS let : IsDomain (Localization S) := by infer_instance simpa [Localization.of] using (dvd_of_localization_dvd_isLocalization - (β := Localization S) (S := S) hS hp havoid hdiv) + (β := Localization S) (S := S) hS hdiv) theorem prime_of_localization_prime_isLocalization {α β : Type*} [CommRing α] [IsDomain α] {S : Submonoid α} [CommRing β] [Algebra α β] [_root_.IsLocalization S β] (hS : ∀ s ∈ S, Prime s ∨ IsUnit s) {p : α} - (_hp : Irreducible p) (_havoid : Avoids S p) (hploc : Prime (algebraMap α β p)) : Prime p := by + (hploc : Prime (algebraMap α β p)) : Prime p := by let e : α ≃ₐ[α] β := _root_.IsLocalization.atUnits α S (Submonoid.le_isUnit_of_prime_or_unit hS) exact (MulEquiv.prime_iff e).mp hploc theorem prime_of_localization_prime {α : Type*} [CommRing α] [IsDomain α] {S : Submonoid α} - (hS : ∀ s ∈ S, Prime s ∨ IsUnit s) {p : α} (hp : Irreducible p) (havoid : Avoids S p) + (hS : ∀ s ∈ S, Prime s ∨ IsUnit s) {p : α} (hploc : Prime (Localization.of (S := S) p)) : Prime p := by let : Fact ((0 : α) ∉ S) := submonoidZeroNotMemFact hS let : IsDomain (Localization S) := by infer_instance simpa [Localization.of] using (prime_of_localization_prime_isLocalization - (β := Localization S) (S := S) hS hp havoid hploc) + (β := Localization S) (S := S) hS hploc) theorem nagata_key_lemma_isLocalization {α β : Type*} [CommRing α] [IsDomain α] {S : Submonoid α} [CommRing β] [Algebra α β] diff --git a/LeanPool/NagataFactoriality/NagataFactoriality/Nagata/Theorem.lean b/LeanPool/NagataFactoriality/NagataFactoriality/Nagata/Theorem.lean index 55c0b673a4..956952a401 100644 --- a/LeanPool/NagataFactoriality/NagataFactoriality/Nagata/Theorem.lean +++ b/LeanPool/NagataFactoriality/NagataFactoriality/Nagata/Theorem.lean @@ -107,10 +107,4 @@ theorem nagata_theorem_of_prime_or_unit_isLocalization {R T : Type*} (hasFactorization_of_noetherian (α := R)) (fun p hp => nagata_key_lemma_isLocalization (S := S) (β := T) hS hp) -theorem ufd_of_factorization_and_prime_irreducibles {α : Type*} [CommRing α] [IsDomain α] - (hfac : WfDvdMonoid α) - (hprime : ∀ p : α, Irreducible p → Prime p) : - UniqueFactorizationMonoid α := - ufd_of_factorization_and_primes hfac hprime - end NagataFactoriality