Commit 2026-02-24 15:42 9b52ac75

refactor(RingTheory/Ideal/AssociatedPrime/Basic): redefine associated primes to include a radical (#34221) This PR redefines associated primes from I.IsPrime ∧ ∃ x : M, I = colon ⊥ {x} to I.IsPrime ∧ ∃ x : M, I = (colon ⊥ {x}).radical. This new definition is slightly nonstandard but is the correct definition in the non-Noetherian setting because these are exactly the prime ideals of any minimal primary decomposition. I.e., one can prove the following theorem (see the change to Lasker.lean):

lemma IsMinimalPrimaryDecomposition.image_radical_eq_associated_primes
    {R M : Type*} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq (Submodule R M)]
    {I : Submodule R M} {t : Finset (Submodule R M)} (ht : I.IsMinimalPrimaryDecomposition t) :
    (fun J ↦ (J.colon Set.univ).radical) '' t = I.associatedPrimes :=

I also added a new definition N.IsAssociatedPrime := I.IsPrime ∧ ∃ x : M, I = (colon N {x}).radical for submodules because that's actually the definition needed for the above theorem (you can't write associatedPrimes R (M ⧸ N) when M is only an AddCommMonoid). And also the proof that the radical doesn't matter when the ring is Noetherian generalizes to this case.