eq_singleton_of_isPrimary — Mathlib

English

For Noetherian rings, Ass_R(R/I) is the singleton { rad(I) } when I is primary.

Русский

Для Noetherian кольца Ass_R(R/I) состоит из одного элемента { rad(I) } если I примарен.

LaTeX

$$$\\operatorname{Ass}_R(R/I) = \\{ \\sqrt{I} \\}.$$$

Lean4

theorem eq_singleton_of_isPrimary [IsNoetherianRing R] (hI : I.IsPrimary) :
    associatedPrimes R (R ⧸ I) = { I.radical } := by
  ext J
  rw [Set.mem_singleton_iff]
  refine ⟨IsAssociatedPrime.eq_radical hI, ?_⟩
  rintro rfl
  haveI : Nontrivial (R ⧸ I) :=
    by
    refine ⟨(Ideal.Quotient.mk I :) 1, (Ideal.Quotient.mk I :) 0, ?_⟩
    rw [Ne, Ideal.Quotient.eq, sub_zero, ← Ideal.eq_top_iff_one]
    exact hI.1
  obtain ⟨a, ha⟩ := associatedPrimes.nonempty R (R ⧸ I)
  exact ha.eq_radical hI ▸ ha

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