homogeneousCore_eq_sSup — Mathlib

English

For a graded ring 𝒜 and I an ideal, I.homogeneousCore 𝒜 equals the supremum (least upper bound) of all homogeneous ideals J with J.toIdeal ≤ I.

Русский

Для 𝒜 и идеала I, I.homogeneousCore 𝒜 равен наименьшей верхней границе всех однородных идеалов J с J.toIdeal ≤ I.

LaTeX

$$$ I.homogeneousCore 𝒜 = \inf \{ J : HomogeneousIdeal 𝒜 \mid J.toIdeal \le I \}$$$

Lean4

theorem homogeneousCore_eq_sSup : I.homogeneousCore 𝒜 = sSup {J : HomogeneousIdeal 𝒜 | J.toIdeal ≤ I} :=
  Eq.symm <| IsLUB.sSup_eq <| (Ideal.homogeneousCore.gc 𝒜).isGreatest_u.isLUB

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