isHomogeneous_iff_forall_subset — Mathlib

English

An ideal I is homogeneous with respect to 𝒜 iff it satisfies a per-degree subset condition relating projections to I.

Русский

Идеал I гомогенен по 𝒜 тогда и только тогда, когда выполняется условие подмножеств по степеням и проекциям на I.

LaTeX

$$I.IsHomogeneous 𝒜 ⇔ ∀ i, (I : Set A) ⊆ GradedRing.proj 𝒜 i ⁻¹' ↑I$$

Lean4

theorem isHomogeneous_iff_forall_subset : I.IsHomogeneous 𝒜 ↔ ∀ i, (I : Set A) ⊆ GradedRing.proj 𝒜 i ⁻¹' I :=
  Iff.rfl

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