vanishingIdeal_iUnion — Mathlib

English

The vanishing ideal of a union over an index equals the infimum of the vanishing ideals over the index.

Русский

Идеал нулевых значений объединения по индексу равен инфимууму по индексу.

LaTeX

$$$ \operatorname{vanishingIdeal}\left(\bigcup_i t_i\right) = \bigwedge_i \operatorname{vanishingIdeal}(t_i) $$$

Lean4

theorem vanishingIdeal_iUnion {γ : Sort*} (t : γ → Set (ProjectiveSpectrum 𝒜)) :
    vanishingIdeal (⋃ i, t i) = ⨅ i, vanishingIdeal (t i) :=
  HomogeneousIdeal.toIdeal_injective <| by convert (gc_ideal 𝒜).u_iInf; exact HomogeneousIdeal.toIdeal_iInf _

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