radical_eq — Mathlib

English

The radical of a homogeneous ideal is itself homogeneous.

Русский

Радикал гомогенного идеала сам по себе гомогенный.

LaTeX

$$$$ \text{If } I \text{ is homogeneous, then } I.radical \ is \ homogeneous. $$$$

Lean4

theorem radical_eq {I : Ideal A} (hI : I.IsHomogeneous 𝒜) :
    I.radical = InfSet.sInf {J | Ideal.IsHomogeneous 𝒜 J ∧ I ≤ J ∧ J.IsPrime} :=
  by
  rw [Ideal.radical_eq_sInf]
  apply le_antisymm
  · exact sInf_le_sInf fun J => And.right
  · refine sInf_le_sInf_of_isCoinitialFor ?_
    rintro J ⟨HJ₁, HJ₂⟩
    refine ⟨(J.homogeneousCore 𝒜).toIdeal, ?_, J.toIdeal_homogeneousCore_le _⟩
    refine ⟨HomogeneousIdeal.isHomogeneous _, ?_, HJ₂.homogeneousCore⟩
    exact hI.toIdeal_homogeneousCore_eq_self.symm.trans_le (Ideal.homogeneousCore_mono _ HJ₁)

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