biUnion_associatedPrimes_eq_zero_divisors

English

For Noetherian R, the union over p in Ass_R(M) of p equals the set of zero divisors on M: { r ∈ R | ∃ x ∈ M, x ≠ 0, r·x = 0 }.

Русский

Для Noetherian кольца R объединение по p из Ass_R(M) всех p равно множеству нулевых делителей на M: { r ∈ R | ∃ x ∈ M, x ≠ 0, r·x = 0 }.

LaTeX

$$$\\bigcup_{p \\in \\operatorname{Ass}_R(M)} p = \\{ r \\in R \\mid \\exists x \\in M, x \\ne 0 \\land r x = 0\\}. $$$

Lean4

theorem biUnion_associatedPrimes_eq_zero_divisors [IsNoetherianRing R] :
    ⋃ p ∈ associatedPrimes R M, p = {r : R | ∃ x : M, x ≠ 0 ∧ r • x = 0} :=
  by
  refine subset_antisymm (Set.iUnion₂_subset ?_) ?_
  · rintro _ ⟨h, x, ⟨⟩⟩ r h'
    refine ⟨x, ne_of_eq_of_ne (one_smul R x).symm ?_, h'⟩
    exact (Ideal.ne_top_iff_one _).mp h.ne_top
  · intro r ⟨x, h, h'⟩
    obtain ⟨P, hP, hx⟩ := exists_le_isAssociatedPrime_of_isNoetherianRing R x h
    exact Set.mem_biUnion hP (hx h')

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