homogeneousHull_eq_iSup — Mathlib

English

The hull equals the supremum over index i of homogeneous ideals generated by the projected pieces: I.homogeneousHull 𝒜 = ⨆ i, ⟨ span( GradedRing.proj 𝒜 i '' I ), homogeneous_span 𝒜 _ (...) ⟩.

Русский

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

LaTeX

$$$ I.homogeneousHull 𝒜 = \bigsqcup_i \; \langle \text{Ideal.span}(\text{GradedRing.proj } 𝒜 i '' I), \text{Ideal.homogeneous_span 𝒜 _ (proof)} \rangle $$$

Lean4

theorem homogeneousHull_eq_iSup :
    I.homogeneousHull 𝒜 =
      ⨆ i,
        ⟨Ideal.span (GradedRing.proj 𝒜 i '' I),
          Ideal.homogeneous_span 𝒜 _
            (by
              rintro _ ⟨x, -, rfl⟩
              apply SetLike.isHomogeneousElem_coe)⟩ :=
  by
  ext1
  rw [Ideal.toIdeal_homogeneousHull_eq_iSup, toIdeal_iSup]

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