image_comap_C_basicOpen — Mathlib

English

For a multivariate polynomial f, the image of the basic open set defined by f under the comap map C is exactly the complement of the zero locus of the set of all coefficients of f.

Русский

Для базового открытого множества, заданного по f, образ через отображение C в противоположном направлении равен дополнению нулевой локусы множества всех коэффициентов f.

LaTeX

$$$\\operatorname{comap} C '' \\operatorname{basicOpen} f = \\big( \\operatorname{zeroLocus} (\\operatorname{Set.range} f.coeff) \\big)^c$$$

Lean4

theorem image_comap_C_basicOpen (f : MvPolynomial σ R) :
    comap (C (σ := σ)) '' basicOpen f = (zeroLocus (Set.range f.coeff))ᶜ :=
  by
  ext p
  rw [mem_image_comap_C_basicOpen]
  simp [Set.range_subset_iff]

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