isLocal_of_isMaximal_radical — Mathlib

English

If the radical of I is maximal, then I is a local ideal.

Русский

Если радикал I максимален, то I является локальным идеалом.

LaTeX

$$I.\mathrm{radical}.IsMaximal \Rightarrow I.IsLocal$$

Lean4

theorem isLocal_of_isMaximal_radical {I : Ideal R} (hi : IsMaximal (radical I)) : IsLocal I :=
  ⟨have : radical I = jacobson I :=
      le_antisymm (le_sInf fun _ ⟨him, hm⟩ => hm.isPrime.radical_le_iff.2 him) (sInf_le ⟨le_radical, hi⟩)
    show IsMaximal (jacobson I) from this ▸ hi⟩

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