English
If I is primary and J is the associated prime of R/I, then J = sqrt(I).
Русский
Если I примарный и J ассоциирован к R/I, тогда J = sqrt(I).
LaTeX
$$$ J = \\sqrt{I} $.$$
Lean4
theorem eq_radical (hI : I.IsPrimary) (h : IsAssociatedPrime J (R ⧸ I)) : J = I.radical :=
by
obtain ⟨hJ, x, e⟩ := h
have : x ≠ 0 := by
rintro rfl
apply hJ.1
rwa [toSpanSingleton_zero, ker_zero] at e
obtain ⟨x, rfl⟩ := Ideal.Quotient.mkₐ_surjective R _ x
replace e : ∀ {y}, y ∈ J ↔ x * y ∈ I := by
intro y
rw [e, mem_ker, toSpanSingleton_apply, ← map_smul, smul_eq_mul, mul_comm, Ideal.Quotient.mkₐ_eq_mk, ←
Ideal.Quotient.mk_eq_mk, Submodule.Quotient.mk_eq_zero]
apply le_antisymm
· intro y hy
exact ((Ideal.isPrimary_iff.1 hI).2 <| e.mp hy).resolve_left ((Submodule.Quotient.mk_eq_zero I).not.mp this)
· rw [hJ.radical_le_iff]
intro y hy
exact e.mpr (I.mul_mem_left x hy)
