vanishingIdeal_pointToPoint — Mathlib

English

The vanishing ideal of the image of a set V under the map pointToPoint equals the vanishing ideal of V.

Русский

Нулевая идеал образа множества V под отображением pointToPoint равен нулевой идеалV.

LaTeX

$$PrimeSpectrum.vanishingIdeal (pointToPoint '' V) = MvPolynomial.vanishingIdeal(k, V)$$

Lean4

@[simp]
theorem vanishingIdeal_pointToPoint (V : Set (σ → K)) :
    PrimeSpectrum.vanishingIdeal (pointToPoint '' V) = MvPolynomial.vanishingIdeal k V :=
  le_antisymm
    (fun _ hp x hx =>
      (((PrimeSpectrum.mem_vanishingIdeal _ _).1 hp) ⟨vanishingIdeal k { x }, by infer_instance⟩ (⟨x, hx, rfl⟩ : _)) x
        rfl)
    fun _ hp =>
    (PrimeSpectrum.mem_vanishingIdeal _ _).2 fun _ hI =>
      let ⟨x, hx⟩ := hI
      hx.2 ▸ fun _ hx' => (Set.mem_singleton_iff.1 hx').symm ▸ hp x hx.1

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