le_zeroLocus_iff_le_vanishingIdeal

English

anti-monotone version: if V ⊆ W then zeroLocus(W) ⊆ zeroLocus(V) for vanishing ideals.

Русский

анти-монотоничность: если V ⊆ W, то Z(W) ⊆ Z(V) для vanishingIdeal.

LaTeX

$$$V \\le W \\Rightarrow \\mathrm{zeroLocus}(K,W) \\le \\mathrm{zeroLocus}(K,V)$$$

Lean4

theorem le_zeroLocus_iff_le_vanishingIdeal {V : Set (σ → K)} {I : Ideal (MvPolynomial σ k)} :
    V ≤ zeroLocus K I ↔ I ≤ vanishingIdeal k V :=
  zeroLocus_vanishingIdeal_galoisConnection.le_iff_le

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