sup — Mathlib

English

Let I and J be homogeneous ideals with respect to the graded ring 𝒜. Then their join I ⊔ J is again homogeneous.

Русский

Пусть I и J — однородные идеалы относительно градационного кольца 𝒜. Тогда их объединение I ⊔ J тоже однородно.

LaTeX

$$$IsHomogeneous(\\mathcal{A}, I) \\wedge IsHomogeneous(\\mathcal{A}, J) \\Rightarrow IsHomogeneous(\\mathcal{A}, I \\sqcup J)$$$

Lean4

theorem sup {I J : Ideal A} (HI : I.IsHomogeneous 𝒜) (HJ : J.IsHomogeneous 𝒜) : (I ⊔ J).IsHomogeneous 𝒜 :=
  by
  rw [iff_exists] at HI HJ ⊢
  obtain ⟨⟨s₁, rfl⟩, ⟨s₂, rfl⟩⟩ := HI, HJ
  refine ⟨s₁ ∪ s₂, ?_⟩
  rw [Set.image_union]
  exact (Submodule.span_union _ _).symm

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