toIdeal_homogeneousCore_eq_self — Mathlib

English

An ideal is homogeneous iff its homogeneousCore coincides with the original ideal.

Русский

Идеал гомогенен тогда и только тогда, когда его homogeneousCore совпадает с исходным идеалом.

LaTeX

$$Ideal.IsHomogeneous 𝒜 I ⇔ (Ideal.homogeneousCore 𝒜 I).toIdeal = I$$

Lean4

theorem toIdeal_homogeneousCore_eq_self (h : I.IsHomogeneous 𝒜) : (I.homogeneousCore 𝒜).toIdeal = I :=
  by
  apply le_antisymm (I.homogeneousCore'_le 𝒜) _
  intro x hx
  classical
  rw [← DirectSum.sum_support_decompose 𝒜 x]
  exact Ideal.sum_mem _ fun j _ => Ideal.subset_span ⟨⟨_, isHomogeneousElem_coe _⟩, h _ hx, rfl⟩

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