feat(RingTheory/IsPrimary): connection between IsPrimary and radicals of colons (leanprover-community#34140)

This PR adds a couple API lemmas connecting `IsPrimary` and radicals of colons, in preparation for uniqueness of primary decomposition.

Co-authored-by: tb65536 <thomas.l.browning@gmail.com>

Author: tb65536

Mathlib/Algebra/Module/Submodule/Lattice.lean

@@ -136,6 +136,10 @@ instance : Top (Submodule R M) :=
 theorem top_coe : ((⊤ : Submodule R M) : Set M) = Set.univ :=
   rfl
 
+@[simp]
+theorem coe_eq_univ : (p : Set M) = Set.univ ↔ p = ⊤ := by
+  rw [iff_comm, ← SetLike.coe_set_eq, top_coe]
+
 @[simp] lemma mem_top {x : M} : x ∈ (⊤ : Submodule R M) := trivial
 
 @[simp]

Mathlib/Algebra/Module/Submodule/Union.lean

@@ -40,7 +40,7 @@ lemma Submodule.iUnion_ssubset_of_forall_ne_top_of_card_lt (s : Finset ι) (p :
   | insert j s hj hj' =>
     simp only [ssubset_univ_iff] at hj' ⊢
     rcases s.eq_empty_or_nonempty with rfl | hs
-    · simpa [← SetLike.coe_ne_coe] using h₁ j
+    · simpa using h₁ j
     replace h₂ : s.card + 1 < ENat.card K := by simpa [Finset.card_insert_of_notMem hj] using h₂
     specialize hj' (lt_trans ENat.natCast_lt_succ h₂)
     contrapose! hj'

Mathlib/RingTheory/Ideal/IsPrimary.lean

@@ -46,11 +46,7 @@ theorem IsPrime.isPrimary {I : Ideal R} (hi : IsPrime I) : I.IsPrimary :=
   ⟨hi.1, fun {_ _} hxy => (hi.mem_or_mem hxy).imp id fun hyi => le_radical hyi⟩
 
 theorem isPrime_radical {I : Ideal R} (hi : I.IsPrimary) : IsPrime (radical I) :=
-  ⟨mt radical_eq_top.1 hi.1,
-   fun {x y} ⟨m, hxy⟩ => by
-    rw [mul_pow] at hxy; rcases (isPrimary_iff.mp hi).2 hxy with h | h
-    · exact Or.inl ⟨m, h⟩
-    · exact Or.inr (mem_radical_of_pow_mem h)⟩
+  I.colon_univ ▸ hi.isPrime_radical_colon
 
 theorem isPrimary_of_isMaximal_radical {I : Ideal R} (hi : IsMaximal (radical I)) :
     I.IsPrimary := by

Mathlib/RingTheory/Ideal/Operations.lean

@@ -826,6 +826,7 @@ theorem IsRadical.radical_le_iff (hJ : J.IsRadical) : I.radical ≤ J ↔ I ≤
 theorem radical_le_radical_iff : radical I ≤ radical J ↔ I ≤ radical J :=
   (radical_isRadical J).radical_le_iff
 
+@[simp]
 theorem radical_eq_top : radical I = ⊤ ↔ I = ⊤ :=
   ⟨fun h =>
     (eq_top_iff_one _).2 <|

Mathlib/RingTheory/IsPrimary.lean

@@ -40,6 +40,8 @@ open Pointwise
 
 namespace Submodule
 
+open Ideal
+
 section CommSemiring
 
 variable {R M : Type*} [CommSemiring R] [AddCommMonoid M] [Module R M]
@@ -87,6 +89,19 @@ lemma isPrimary_finsetInf {ι : Type*} {s : Finset ι} {f : ι → Submodule R M
     rw [colon_finsetInf, Ideal.radical_finset_inf hy H,
       hs' (mem_insert_self _ _), hs' (mem_insert_of_mem hy)]
 
+theorem IsPrimary.isPrime_radical_colon (hI : S.IsPrimary) : (S.colon .univ).radical.IsPrime := by
+  refine isPrime_iff.mpr <| hI.imp (by simp) fun h x y ⟨n, hn⟩ ↦ ?_
+  simp_rw [← mem_colon_iff_le, ← mem_radical_iff] at h
+  refine or_iff_not_imp_left.mpr fun hx ↦ ⟨n, ?_⟩
+  simp only [mul_pow, mem_colon, Set.mem_univ, true_imp_iff, mul_smul] at hn ⊢
+  exact fun p ↦ (h (hn p)).resolve_right (mt mem_radical_of_pow_mem hx)
+
+theorem IsPrimary.radical_colon_singleton_of_notMem (hI : S.IsPrimary) {m : M} (hm : m ∉ S) :
+    (S.colon {m}).radical = (S.colon Set.univ).radical :=
+  le_antisymm (radical_le_radical_iff.mpr fun _ hy ↦
+    (hI.2 (Submodule.mem_colon_singleton.mp hy)).resolve_left hm)
+    (radical_mono (Submodule.colon_mono le_rfl (Set.subset_univ {m})))
+
 end CommSemiring
 
 section CommRing