Definition of associated primes

Stream: mathlib4

[Thomas Browning]

Currently the definition of an associated prime is:

def IsAssociatedPrime : Prop :=
  I.IsPrime ∧ ∃ x : M, I = ker (toSpanSingleton R M x)

but my vague understanding of primary decomposition in the non-Noetherian case is that you actually want to throw in a radical:

def IsAssociatedPrime : Prop :=
  I.IsPrime ∧ ∃ x : M, I = radical (ker (toSpanSingleton R M x))

Does this seems right? Or is there some reason to prefer the current definition?

[Thomas Browning]

(In particular, I think that it's the second definition actually gives the set of associated primes in any primary decomposition, but the two definitions are equivalent in the Noetherian case)

[Junyan Xu]

not familiar with this notion, but (3) of stacks#0566 looks relevant

[Thomas Browning]

Ah, maybe weakly associated is what I'm looking for.

[Thomas Browning]

Actually, perhaps not. At least, for rings I know that it's these radicals of annihilators that are precisely the primes that occur in a primary decomposition.

[Thomas Browning]

So I'm not sure why people care about weakly associated primes.