pointToPoint_zeroLocus_le — Mathlib

English

The image of the zero locus under pointToPoint is contained in the zero locus of I.

Русский

Образ нулевой зоны через pointToPoint содержится в нулевой зоне идеала I.

LaTeX

$$pointToPoint( k := K) '' MvPolynomial.zeroLocus K I ≤ PrimeSpectrum.zeroLocus I$$

Lean4

theorem pointToPoint_zeroLocus_le (I : Ideal (MvPolynomial σ K)) :
    pointToPoint (k := K) '' MvPolynomial.zeroLocus K I ≤ PrimeSpectrum.zeroLocus I := fun J hJ =>
  let ⟨_, hx⟩ := hJ
  (le_trans (le_vanishingIdeal_zeroLocus (K := K) I)
      (hx.2 ▸ vanishingIdeal_anti_mono (Set.singleton_subset_iff.2 hx.1)) :
    I ≤ J.asIdeal)

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