iSup — Mathlib

English

If a family of ideals (f i) consists of homogeneous ideals, then their supremum ⨆ i f i is homogeneous.

Русский

Пусть последовательность идеалов (f_i) состоит из однородных идеалов; их наибольшая верхняя граница ⨆ i f_i тоже однородна.

LaTeX

$$$(\\forall i, IsHomogeneous(\\mathcal{A}, f(i))) \\Rightarrow IsHomogeneous(\\mathcal{A}, \\big(\\bigsqcup_i f(i)\\big))$$$

Lean4

protected theorem iSup {κ : Sort*} {f : κ → Ideal A} (h : ∀ i, (f i).IsHomogeneous 𝒜) : (⨆ i, f i).IsHomogeneous 𝒜 :=
  by
  simp_rw [iff_exists] at h ⊢
  choose s hs using h
  refine ⟨⋃ i, s i, ?_⟩
  simp_rw [Set.image_iUnion, Ideal.span_iUnion]
  congr
  exact funext hs

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