toIdeal_homogeneousHull_eq_iSup — Mathlib

English

The hull equals the supremum of span of graded projections: (I.homogeneousHull 𝒜).toIdeal = ⨆ i, Ideal.span (GradedRing.proj 𝒜 i '' I).

Русский

Оболочка равна сверху над спаном проекций Граде́дированных: (I.homogeneousHull 𝒜).toIdeal = ⨆ i, Ideal.span (GradedRing.proj 𝒜 i '' I).

LaTeX

$$$ (I.homogeneousHull 𝒜).toIdeal = \bigsqcup_i \; Ideal.span( GradedRing.proj 𝒜 i '' I ) $$$

Lean4

theorem toIdeal_homogeneousHull_eq_iSup : (I.homogeneousHull 𝒜).toIdeal = ⨆ i, Ideal.span (GradedRing.proj 𝒜 i '' I) :=
  by
  rw [← Ideal.span_iUnion]
  apply congr_arg Ideal.span _
  ext1
  simp only [Set.mem_iUnion, Set.mem_image, mem_setOf_eq, GradedRing.proj_apply, SetLike.exists, exists_prop,
    SetLike.mem_coe]

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