biUnion_associatedPrimes_eq_compl_regular

English

For a Noetherian ring R and an R-module M, the union over all associated primes p of M of p equals the complement of the set of regular scalars on M. In symbols, ⋃_{p ∈ Ass(R,M)} p = {r ∈ R | IsSMulRegular M r}^c.

Русский

Для кольца Нётерово R и модуля M над R объединение всех ассоциированных простых p в M равно дополнению множества регулярных элементов на M: ⋃_{p ∈ Ass(R,M)} p = {r ∈ R | IsSMulRegular M r}^c.

LaTeX

$$$\bigcup_{p \in \operatorname{associatedPrimes}(R,M)} p = \{ r \in R \mid \lnot IsSMulRegular(M,r) \}.$$$

Lean4

theorem biUnion_associatedPrimes_eq_compl_regular [IsNoetherianRing R] :
    ⋃ p ∈ associatedPrimes R M, p = {r : R | IsSMulRegular M r}ᶜ :=
  Eq.trans (biUnion_associatedPrimes_eq_zero_divisors R M) <| by
    simp_rw [Set.compl_setOf, isSMulRegular_iff_right_eq_zero_of_smul, not_forall, exists_prop, and_comm]

Похожие утверждения