mul_homogeneous_element_mem_of_mem

English

If s is a set of elements each homogeneous, then the ideal span(s) is homogeneous with respect to 𝒜.

Русский

Если s состоит из однородных элементов, порожденный ими идеал является однородным по 𝒜.

LaTeX

$$Ideal.IsHomogeneous 𝒜 (Ideal.span s)$$

Lean4

theorem mul_homogeneous_element_mem_of_mem {I : Ideal A} (r x : A) (hx₁ : SetLike.IsHomogeneousElem 𝒜 x) (hx₂ : x ∈ I)
    (j : ι) : GradedRing.proj 𝒜 j (r * x) ∈ I := by
  classical
  rw [← DirectSum.sum_support_decompose 𝒜 r, Finset.sum_mul, map_sum]
  apply Ideal.sum_mem
  intro k _
  obtain ⟨i, hi⟩ := hx₁
  have mem₁ : (DirectSum.decompose 𝒜 r k : A) * x ∈ 𝒜 (k + i) := GradedMul.mul_mem (SetLike.coe_mem _) hi
  rw [GradedRing.proj_apply, DirectSum.decompose_of_mem 𝒜 mem₁, coe_of_apply]
  split_ifs
  · exact I.mul_mem_left _ hx₂
  · exact I.zero_mem

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