isHomogeneous_iff_subset_iInter — Mathlib

English

I is homogeneous with respect to 𝒜 iff I is contained in the intersection over i of the preimages of I under each graded projection.

Русский

I гомогенен по 𝒜 тогда и только тогда, когда I ⊆ ⋂i GradedRing.proj 𝒜 i^{-1} (I).

LaTeX

$$I.IsHomogeneous 𝒜 ⇔ I ⊆ ⋂ i, GradedRing.proj 𝒜 i ⁻¹' ↑I$$

Lean4

theorem isHomogeneous_iff_subset_iInter : I.IsHomogeneous 𝒜 ↔ (I : Set A) ⊆ ⋂ i, GradedRing.proj 𝒜 i ⁻¹' ↑I :=
  subset_iInter_iff.symm

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