English
Over a Noetherian ring, for any nonzero x ∈ M there exists an associated prime P of M such that ker(toSpanSingleton R M x) ≤ P.
Русский
Для кольца noetherian, для любого ненулевого x ∈ M существует ассоциированный простой P такой, что ker(toSpanSingleton x) ≤ P.
LaTeX
$$$$\exists P:\text{Ideal } R,\ IsAssociatedPrime P M \land \ker(\text{toSpanSingleton } R M x) \le P.$$$$
Lean4
theorem exists_le_isAssociatedPrime_of_isNoetherianRing [H : IsNoetherianRing R] (x : M) (hx : x ≠ 0) :
∃ P : Ideal R, IsAssociatedPrime P M ∧ ker (toSpanSingleton R M x) ≤ P :=
by
have : ker (toSpanSingleton R M x) ≠ ⊤ := by rwa [Ne, Ideal.eq_top_iff_one, mem_ker, toSpanSingleton_apply, one_smul]
obtain ⟨P, ⟨l, h₁, y, rfl⟩, h₃⟩ :=
set_has_maximal_iff_noetherian.mpr H
{P | ker (toSpanSingleton R M x) ≤ P ∧ P ≠ ⊤ ∧ ∃ y : M, P = ker (toSpanSingleton R M y)} ⟨_, rfl.le, this, x, rfl⟩
refine ⟨_, ⟨⟨h₁, ?_⟩, y, rfl⟩, l⟩
intro a b hab
rw [or_iff_not_imp_left]
intro ha
rw [mem_ker, toSpanSingleton_apply] at ha hab
have H₁ : ker (toSpanSingleton R M y) ≤ ker (toSpanSingleton R M (a • y)) :=
by
intro c hc
rw [mem_ker, toSpanSingleton_apply] at hc ⊢
rw [smul_comm, hc, smul_zero]
have H₂ : ker (toSpanSingleton R M (a • y)) ≠ ⊤ := by rwa [Ne, ker_eq_top, toSpanSingleton_eq_zero_iff]
rwa [H₁.eq_of_not_lt (h₃ _ ⟨l.trans H₁, H₂, _, rfl⟩), mem_ker, toSpanSingleton_apply, smul_comm, smul_smul]
