homogeneousHull — Mathlib

English

For any ideal I in A, Ideal.homogeneousHull 𝒜 is the smallest homogeneous ideal containing I.

Русский

Для любого идеала I в A, Ideal.homogeneousHull 𝒜 есть наименьший однородный идеал, содержащий I.

LaTeX

$$$ \text{homogeneousHull } 𝒜 I = \text{the smallest homogeneous ideal containing } I$$$

Lean4

/-- For any `I : Ideal A`, not necessarily homogeneous, `I.homogeneousHull 𝒜` is
the smallest homogeneous ideal containing `I`. -/
def homogeneousHull : HomogeneousIdeal 𝒜 :=
  ⟨Ideal.span {r : A | ∃ (i : ι) (x : I), (DirectSum.decompose 𝒜 (x : A) i : A) = r},
    by
    refine Ideal.homogeneous_span _ _ fun x hx => ?_
    obtain ⟨i, x, rfl⟩ := hx
    apply SetLike.isHomogeneousElem_coe⟩

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