subset_zeroLocus_iff_subset_vanishingIdeal

English

Let t be a subset of the prime spectrum of a ring R and s a subset of R. Then t is contained in the zero locus of s if and only if s is contained in the vanishing ideal of t.

Русский

Пусть t — подмножество спектра Прайма кольца R, а s — подмножество элементов кольца. Тогда t ⊆ zeroLocus(s) тогда и только тогда, когда s ⊆ vanishingIdeal(t).

LaTeX

$$$ t \subseteq \operatorname{zeroLocus}(s) \;\iff\; s \subseteq \operatorname{vanishingIdeal}(t) $$$

Lean4

theorem subset_zeroLocus_iff_subset_vanishingIdeal (t : Set (PrimeSpectrum R)) (s : Set R) :
    t ⊆ zeroLocus s ↔ s ⊆ vanishingIdeal t :=
  (gc_set R) s t

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