chore(RingTheory/PrincipalIdealDomain): PID implies Noetherian (#18382)

Also, generalize `IsPrincipal.generator` to `Semiring R` and `AddCommMonoid M` Co-authored-by: Yakov Pechersky <[email protected]>
leanprover-community · Oct 30, 2024 · 72cd706 · 72cd706
1 parent e15c6eb
commit 72cd706
Show file tree

Hide file tree

Showing 4 changed files with 23 additions and 18 deletions.
diff --git a/Mathlib/RingTheory/Bezout.lean b/Mathlib/RingTheory/Bezout.lean
@@ -51,7 +51,7 @@ theorem TFAE [IsBezout R] [IsDomain R] :
     [IsNoetherianRing R, IsPrincipalIdealRing R, UniqueFactorizationMonoid R, WfDvdMonoid R] := by
   classical
     tfae_have 1 → 2
-    | H => ⟨fun I => isPrincipal_of_FG _ (IsNoetherian.noetherian _)⟩
+    | _ => inferInstance
     tfae_have 2 → 3
     | _ => inferInstance
     tfae_have 3 → 4

diff --git a/Mathlib/RingTheory/LocalRing/Quotient.lean b/Mathlib/RingTheory/LocalRing/Quotient.lean
@@ -7,7 +7,9 @@ Authors: Andrew Yang, Riccardo Brasca
 import Mathlib.LinearAlgebra.Dimension.DivisionRing
 import Mathlib.LinearAlgebra.FreeModule.PID
 import Mathlib.LinearAlgebra.FreeModule.StrongRankCondition
-import Mathlib.RingTheory.DiscreteValuationRing.TFAE
+import Mathlib.RingTheory.Ideal.Over
+import Mathlib.RingTheory.Nakayama
+import Mathlib.RingTheory.Valuation.ValuationRing
 
 /-!
 

diff --git a/Mathlib/RingTheory/PrincipalIdealDomain.lean b/Mathlib/RingTheory/PrincipalIdealDomain.lean
@@ -22,7 +22,7 @@ Theorems about PID's are in the `principal_ideal_ring` namespace.
 - `IsPrincipalIdealRing`: a predicate on rings, saying that every left ideal is principal.
 - `IsBezout`: the predicate saying that every finitely generated left ideal is principal.
 - `generator`: a generator of a principal ideal (or more generally submodule)
-- `to_unique_factorization_monoid`: a PID is a unique factorization domain
+- `to_uniqueFactorizationMonoid`: a PID is a unique factorization domain
 
 # Main results
 
@@ -43,7 +43,7 @@ open Submodule
 
 section
 
-variable [Ring R] [AddCommGroup M] [Module R M]
+variable [Semiring R] [AddCommGroup M] [Module R M]
 
 instance bot_isPrincipal : (⊥ : Submodule R M).IsPrincipal :=
   ⟨⟨0, by simp⟩⟩
@@ -72,11 +72,11 @@ end
 
 namespace Submodule.IsPrincipal
 
-variable [AddCommGroup M]
+variable [AddCommMonoid M]
 
-section Ring
+section Semiring
 
-variable [Ring R] [Module R M]
+variable [Semiring R] [Module R M]
 
 /-- `generator I`, if `I` is a principal submodule, is an `x ∈ M` such that `span R {x} = I` -/
 noncomputable def generator (S : Submodule R M) [S.IsPrincipal] : M :=
@@ -103,7 +103,20 @@ theorem mem_iff_eq_smul_generator (S : Submodule R M) [S.IsPrincipal] {x : M} :
 theorem eq_bot_iff_generator_eq_zero (S : Submodule R M) [S.IsPrincipal] :
     S = ⊥ ↔ generator S = 0 := by rw [← @span_singleton_eq_bot R M, span_singleton_generator]
 
-end Ring
+protected lemma fg {S : Submodule R M} (h : S.IsPrincipal) : S.FG :=
+  ⟨{h.generator}, by simp only [Finset.coe_singleton, span_singleton_generator]⟩
+
+-- See note [lower instance priority]
+instance (priority := 100) _root_.PrincipalIdealRing.isNoetherianRing [IsPrincipalIdealRing R] :
+    IsNoetherianRing R where
+  noetherian S := (IsPrincipalIdealRing.principal S).fg
+
+-- See note [lower instance priority]
+instance (priority := 100) _root_.IsPrincipalIdealRing.of_isNoetherianRing_of_isBezout
+    [IsNoetherianRing R] [IsBezout R] : IsPrincipalIdealRing R where
+  principal S := IsBezout.isPrincipal_of_FG S (IsNoetherian.noetherian S)
+
+end Semiring
 
 section CommRing
 
@@ -278,15 +291,6 @@ namespace PrincipalIdealRing
 
 open IsPrincipalIdealRing
 
--- see Note [lower instance priority]
-instance (priority := 100) isNoetherianRing [Ring R] [IsPrincipalIdealRing R] :
-    IsNoetherianRing R :=
-  isNoetherianRing_iff.2
-    ⟨fun s : Ideal R => by
-      rcases (IsPrincipalIdealRing.principal s).principal with ⟨a, rfl⟩
-      rw [← Finset.coe_singleton]
-      exact ⟨{a}, SetLike.coe_injective rfl⟩⟩
-
 theorem isMaximal_of_irreducible [CommRing R] [IsPrincipalIdealRing R] {p : R}
     (hp : Irreducible p) : Ideal.IsMaximal (span R ({p} : Set R)) :=
   ⟨⟨mt Ideal.span_singleton_eq_top.1 hp.1, fun I hI => by

diff --git a/Mathlib/RingTheory/UniqueFactorizationDomain.lean b/Mathlib/RingTheory/UniqueFactorizationDomain.lean
@@ -195,7 +195,6 @@ class UniqueFactorizationMonoid (α : Type*) [CancelCommMonoidWithZero α] exten
     IsWellFounded α DvdNotUnit : Prop where
   protected irreducible_iff_prime : ∀ {a : α}, Irreducible a ↔ Prime a
 
-/-- Can't be an instance because it would cause a loop `ufm → WfDvdMonoid → ufm → ...`. -/
 instance (priority := 100) ufm_of_decomposition_of_wfDvdMonoid
     [CancelCommMonoidWithZero α] [WfDvdMonoid α] [DecompositionMonoid α] :
     UniqueFactorizationMonoid α :=