English
Radical I equals the infimum of all primes containing I.
Русский
Радикал I равен инфимуму всех простых, содержащих I.
LaTeX
$$radical I = sInf {J : Ideal R | I ≤ J ∧ J IsPrime}$$
Lean4
theorem radical_eq_sInf (I : Ideal R) : radical I = sInf {J : Ideal R | I ≤ J ∧ IsPrime J} :=
le_antisymm (le_sInf fun _ hJ ↦ hJ.2.radical_le_iff.2 hJ.1) fun r hr ↦
by_contradiction fun hri ↦
let ⟨m, hIm, hm⟩ :=
zorn_le_nonempty₀ {K : Ideal R | r ∉ radical K}
(fun c hc hcc y hyc =>
⟨sSup c, fun ⟨n, hrnc⟩ =>
let ⟨_, hyc, hrny⟩ := (Submodule.mem_sSup_of_directed ⟨y, hyc⟩ hcc.directedOn).1 hrnc
hc hyc ⟨n, hrny⟩,
fun _ => le_sSup⟩)
I hri
have hrm : r ∉ radical m := hm.prop
have : ∀ x ∉ m, r ∈ radical (m ⊔ span { x }) := fun x hxm =>
by_contradiction fun hrmx =>
hxm <| by
rw [hm.eq_of_le hrmx le_sup_left]
exact Submodule.mem_sup_right <| mem_span_singleton_self x
have : IsPrime m :=
⟨by rintro rfl; rw [radical_top] at hrm; exact hrm trivial, fun {x y} hxym =>
or_iff_not_imp_left.2 fun hxm =>
by_contradiction fun hym =>
let ⟨n, hrn⟩ := this _ hxm
let ⟨p, hpm, q, hq, hpqrn⟩ := Submodule.mem_sup.1 hrn
let ⟨c, hcxq⟩ := mem_span_singleton'.1 hq
let ⟨k, hrk⟩ := this _ hym
let ⟨f, hfm, g, hg, hfgrk⟩ := Submodule.mem_sup.1 hrk
let ⟨d, hdyg⟩ := mem_span_singleton'.1 hg
hrm
⟨n + k,
by
rw [pow_add, ← hpqrn, ← hcxq, ← hfgrk, ← hdyg, add_mul, mul_add (c * x), mul_assoc c x (d * y),
mul_left_comm x, ← mul_assoc]
refine m.add_mem (m.mul_mem_right _ hpm) (m.add_mem (m.mul_mem_left _ hfm) (m.mul_mem_left _ hxym))⟩⟩
hrm <| this.radical.symm ▸ (sInf_le ⟨hIm, this⟩ : sInf {J : Ideal R | I ≤ J ∧ IsPrime J} ≤ m) hr
