chore: split out Ideal.IsPrimary (#12296)

This splits out a small but self-contained part of RingTheory.Ideal.Operations.
leanprover-community · Apr 24, 2024 · 234e285 · 234e285
1 parent 83e6e98
commit 234e285
Show file tree

Hide file tree

Showing 6 changed files with 63 additions and 41 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -3390,6 +3390,7 @@ import Mathlib.RingTheory.Ideal.Basis
 import Mathlib.RingTheory.Ideal.Colon
 import Mathlib.RingTheory.Ideal.Cotangent
 import Mathlib.RingTheory.Ideal.IdempotentFG
+import Mathlib.RingTheory.Ideal.IsPrimary
 import Mathlib.RingTheory.Ideal.LocalRing
 import Mathlib.RingTheory.Ideal.MinimalPrime
 import Mathlib.RingTheory.Ideal.Norm

diff --git a/Mathlib/RingTheory/Ideal/AssociatedPrime.lean b/Mathlib/RingTheory/Ideal/AssociatedPrime.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Andrew Yang
 -/
 import Mathlib.LinearAlgebra.Span
-import Mathlib.RingTheory.Ideal.Operations
+import Mathlib.RingTheory.Ideal.IsPrimary
 import Mathlib.RingTheory.Ideal.QuotientOperations
 import Mathlib.RingTheory.Noetherian
 

diff --git a/Mathlib/RingTheory/Ideal/IsPrimary.lean b/Mathlib/RingTheory/Ideal/IsPrimary.lean
@@ -0,0 +1,59 @@
+/-
+Copyright (c) 2019 Kenny Lau. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kenny Lau
+-/
+import Mathlib.RingTheory.Ideal.Operations
+
+#align_import ring_theory.ideal.operations from "leanprover-community/mathlib"@"e7f0ddbf65bd7181a85edb74b64bdc35ba4bdc74"
+
+/-!
+# Primary ideals
+
+A proper ideal `I` is primary iff `xy ∈ I` implies `x ∈ I` or `y ∈ radical I`.
+
+## Main definitions
+
+- `Ideal.IsPrimary`
+
+-/
+
+namespace Ideal
+
+variable {R : Type*} [CommSemiring R]
+
+/-- A proper ideal `I` is primary iff `xy ∈ I` implies `x ∈ I` or `y ∈ radical I`. -/
+def IsPrimary (I : Ideal R) : Prop :=
+  I ≠ ⊤ ∧ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ radical I
+#align ideal.is_primary Ideal.IsPrimary
+
+theorem IsPrime.isPrimary {I : Ideal R} (hi : IsPrime I) : IsPrimary I :=
+  ⟨hi.1, fun {_ _} hxy => (hi.mem_or_mem hxy).imp id fun hyi => le_radical hyi⟩
+#align ideal.is_prime.is_primary Ideal.IsPrime.isPrimary
+
+theorem mem_radical_of_pow_mem {I : Ideal R} {x : R} {m : ℕ} (hx : x ^ m ∈ radical I) :
+    x ∈ radical I :=
+  radical_idem I ▸ ⟨m, hx⟩
+#align ideal.mem_radical_of_pow_mem Ideal.mem_radical_of_pow_mem
+
+theorem isPrime_radical {I : Ideal R} (hi : IsPrimary I) : IsPrime (radical I) :=
+  ⟨mt radical_eq_top.1 hi.1,
+   fun {x y} ⟨m, hxy⟩ => by
+    rw [mul_pow] at hxy; cases' hi.2 hxy with h h
+    · exact Or.inl ⟨m, h⟩
+    · exact Or.inr (mem_radical_of_pow_mem h)⟩
+#align ideal.is_prime_radical Ideal.isPrime_radical
+
+theorem isPrimary_inf {I J : Ideal R} (hi : IsPrimary I) (hj : IsPrimary J)
+    (hij : radical I = radical J) : IsPrimary (I ⊓ J) :=
+  ⟨ne_of_lt <| lt_of_le_of_lt inf_le_left (lt_top_iff_ne_top.2 hi.1),
+   fun {x y} ⟨hxyi, hxyj⟩ => by
+    rw [radical_inf, hij, inf_idem]
+    cases' hi.2 hxyi with hxi hyi; cases' hj.2 hxyj with hxj hyj
+    · exact Or.inl ⟨hxi, hxj⟩
+    · exact Or.inr hyj
+    · rw [hij] at hyi
+      exact Or.inr hyi⟩
+#align ideal.is_primary_inf Ideal.isPrimary_inf
+
+end Ideal
diff --git a/Mathlib/RingTheory/Ideal/MinimalPrime.lean b/Mathlib/RingTheory/Ideal/MinimalPrime.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Andrew Yang. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Andrew Yang
 -/
+import Mathlib.RingTheory.Ideal.IsPrimary
 import Mathlib.RingTheory.Localization.AtPrime
 import Mathlib.Order.Minimal
 

diff --git a/Mathlib/RingTheory/Ideal/Operations.lean b/Mathlib/RingTheory/Ideal/Operations.lean
@@ -1870,46 +1870,6 @@ end CommRing
 
 end MapAndComap
 
-section IsPrimary
-
-variable {R : Type u} [CommSemiring R]
-
-/-- A proper ideal `I` is primary iff `xy ∈ I` implies `x ∈ I` or `y ∈ radical I`. -/
-def IsPrimary (I : Ideal R) : Prop :=
-  I ≠ ⊤ ∧ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ radical I
-#align ideal.is_primary Ideal.IsPrimary
-
-theorem IsPrime.isPrimary {I : Ideal R} (hi : IsPrime I) : IsPrimary I :=
-  ⟨hi.1, fun {_ _} hxy => (hi.mem_or_mem hxy).imp id fun hyi => le_radical hyi⟩
-#align ideal.is_prime.is_primary Ideal.IsPrime.isPrimary
-
-theorem mem_radical_of_pow_mem {I : Ideal R} {x : R} {m : ℕ} (hx : x ^ m ∈ radical I) :
-    x ∈ radical I :=
-  radical_idem I ▸ ⟨m, hx⟩
-#align ideal.mem_radical_of_pow_mem Ideal.mem_radical_of_pow_mem
-
-theorem isPrime_radical {I : Ideal R} (hi : IsPrimary I) : IsPrime (radical I) :=
-  ⟨mt radical_eq_top.1 hi.1,
-   fun {x y} ⟨m, hxy⟩ => by
-    rw [mul_pow] at hxy; cases' hi.2 hxy with h h
-    · exact Or.inl ⟨m, h⟩
-    · exact Or.inr (mem_radical_of_pow_mem h)⟩
-#align ideal.is_prime_radical Ideal.isPrime_radical
-
-theorem isPrimary_inf {I J : Ideal R} (hi : IsPrimary I) (hj : IsPrimary J)
-    (hij : radical I = radical J) : IsPrimary (I ⊓ J) :=
-  ⟨ne_of_lt <| lt_of_le_of_lt inf_le_left (lt_top_iff_ne_top.2 hi.1),
-   fun {x y} ⟨hxyi, hxyj⟩ => by
-    rw [radical_inf, hij, inf_idem]
-    cases' hi.2 hxyi with hxi hyi; cases' hj.2 hxyj with hxj hyj
-    · exact Or.inl ⟨hxi, hxj⟩
-    · exact Or.inr hyj
-    · rw [hij] at hyi
-      exact Or.inr hyi⟩
-#align ideal.is_primary_inf Ideal.isPrimary_inf
-
-end IsPrimary
-
 section Total
 
 variable (ι : Type*)

diff --git a/Mathlib/RingTheory/JacobsonIdeal.lean b/Mathlib/RingTheory/JacobsonIdeal.lean
@@ -3,6 +3,7 @@ Copyright (c) 2020 Devon Tuma. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau, Devon Tuma
 -/
+import Mathlib.RingTheory.Ideal.IsPrimary
 import Mathlib.RingTheory.Ideal.Quotient
 import Mathlib.RingTheory.Polynomial.Quotient