homogeneousCore — Mathlib

English

The underlying ideal of the homogeneous core is contained in the original ideal.

Русский

Базовый идеал гомогенного ядра содержится в исходном идеале.

LaTeX

$$(I.homogeneousCore 𝒜 I).toIdeal ≤ I$$

Lean4

/-- For any `I : Ideal A`, not necessarily homogeneous, `I.homogeneousCore' 𝒜`
is the largest homogeneous ideal of `A` contained in `I`. -/
def homogeneousCore : HomogeneousIdeal 𝒜 :=
  ⟨Ideal.homogeneousCore' 𝒜 I,
    Ideal.homogeneous_span _ _ fun _ h =>
      by
      have := Subtype.image_preimage_coe (setOf (SetLike.IsHomogeneousElem 𝒜)) (I : Set A)
      exact (cast congr(_ ∈ $this) h).1⟩

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