homogeneousCore' — Mathlib

English

The homogeneous core construction is monotone with respect to set inclusion.

Русский

Гомогенный ядро сохраняет включения; если I ≤ J, то Core'(I) ≤ Core'(J).

LaTeX

$$Monotone(Ideal.homogeneousCore' 𝒜)$$

Lean4

/-- For any `I : Ideal A`, not necessarily homogeneous, `I.homogeneousCore' 𝒜`
is the largest homogeneous ideal of `A` contained in `I`, as an ideal. -/
def homogeneousCore' (I : Ideal A) : Ideal A :=
  Ideal.span ((↑) '' (((↑) : Subtype (SetLike.IsHomogeneousElem 𝒜) → A) ⁻¹' I))

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