radical_eq_maximalIdeal — Mathlib

English

In a local ring R, for any ideal I not equal to the whole ring, the radical of I is the maximal ideal of R.

Русский

В локальном кольце R радикал любого идеала I, отличный от всего кольца, равен максимальному идеалу R.

LaTeX

$$$[\\text{IsLocalRing } R]\\;\\forall I:\\mathord{\\mathsf{Ideal}}(R),\\; I \\neq R \\Rightarrow I^{\\radical} = \\operatorname{maximalIdeal}R$$$

Lean4

theorem radical_eq_maximalIdeal [IsLocalRing R] (I : Ideal R) (hI : I ≠ ⊤) : I.radical = IsLocalRing.maximalIdeal R :=
  by
  rw [Ideal.radical_eq_sInf]
  refine (sInf_le ?_).antisymm (le_sInf ?_)
  · exact ⟨IsLocalRing.le_maximalIdeal hI, inferInstance⟩
  · rintro J ⟨h₁, h₂⟩
    exact (Ring.KrullDimLE.eq_maximalIdeal_of_isPrime J).ge

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