Define a multivariate polynomial from an existential proof

Stream: new members

[Daniel Patiño]

I have been working with multivariate polynomials and exploring Hilbert's Nullstellensatz. A central concept in this context is the variety defined by MvPolynomial.zeroLocus . In my formalization, I introduced a variation of this definition restricted to a specific set. My definitions are as follows:

variable {K σ : Type*} [Field K]  [Fintype σ]
variable (A : Finset K) (I : Ideal (MvPolynomial σ K))

/--
This defines the variety V^A(I) = {x ∈ A^n | p(x) = 0, ∀p ∈ I}.
-/
def zeroLocus_on : Set (σ → K) :=
  zeroLocus K I ∩ {x : σ → K | ∀ i , x i ∈ A}

def zeroLocus_on_compl : Set (σ → K) :=
  {x : σ → K | ∀ i, x i ∈ A} \ (zeroLocus_on A I)

Since A is a finite subset of K, I can establish several relevant properties, such as the finiteness of the complement:

lemma zeroLocus_on_compl_finite : (zeroLocus_on_compl A I).Finite := by sorry

/--
Given an ideal I generated by a finite set of polynomials S (`I = Ideal.span S`),
if a point x lies in `zeroLocus_on_compl A I`, then there exists a generator p ∈ S
that does not vanish at x (i.e., p(x) ≠ 0).
-/
lemma zeroLocus_on_compl_mem
    (x : σ → K) (S : Finset (MvPolynomial σ K)) (hI : I = Ideal.span S) :
    x ∈ zeroLocus_on_compl A I → ∃ p ∈ S, p.eval x ≠ 0 := by sorry

By applying zeroLocus_on_compl_mem in conjunction with Classical.choose, I can define a selector that assigns a polynomial to each x in zeroLocus_on_compl:

noncomputable def selector_j {A I}
  (S : Finset (MvPolynomial σ K))
  (hI : I = Ideal.span S)
  (x : σ → K)
  (hx : x ∈ zeroLocus_on_compl A I) : MvPolynomial σ K :=
  Classical.choose (zeroLocus_on_compl_mem x S hI hx)

To summarize, I have established that:

$$x \in \texttt{zeroLocus\_on\_compl A I} \implies \exists j_x \in S, j_x (x) \neq 0$$

and my goal is to construct the following polynomial:

$$\prod_{b \in B} (j_b - j_b (b)) \quad \text{where } B = \texttt{zeroLocus\_on\_compl A I}$$

I would appreciate any assistance with this construction. I am currently stuck on how to formally define this polynomial in Lean, and I am also concerned that the resulting definition might be too unwieldy to use in subsequent proofs.

Any suggestions or guidance would be very helpful. Thank you.

[Eric Wieser]

It probably doesn't help here, but note that {x : σ → K | ∀ i , x i ∈ A} can be replaced with Finset.univ.pi fun _ : σ => A, which lets you define your locii as Finsets directly.

[Kevin Buzzard]

You can use docs#finprod to make your product.

[Eric Wieser]

Oh I didn't read, actually my suggestion is very relevant to your problem. Something like this is the alternative to Kevin's suggestion:

import Mathlib

variable {K σ : Type*} [Field K]  [Fintype σ]
variable (A : Finset K) (I : Ideal (MvPolynomial σ K))

open MvPolynomial

noncomputable def zeroLocus_on : Finset (σ → K) :=
  open Classical in
  {x ∈ Fintype.piFinset fun _ : σ => A | x ∈ zeroLocus K I}

noncomputable def zeroLocus_on_compl : Finset (σ → K) :=
  open Classical in
  {x ∈ Fintype.piFinset fun _ : σ => A | x ∉ zeroLocus K I}

lemma zeroLocus_on_compl_finite : Set.Finite (zeroLocus_on_compl A I : Set (σ → K)) := by simp

variable {A I}

lemma zeroLocus_on_compl_mem
    (x : σ → K) (S : Finset (MvPolynomial σ K)) (hI : I = Ideal.span S) :
    x ∈ zeroLocus_on_compl A I → ∃ p ∈ S, p.eval x ≠ 0 := by sorry

noncomputable def selector_j {A I}
  (S : Finset (MvPolynomial σ K))
  (hI : I = Ideal.span S)
  (x : σ → K)
  (hx : x ∈ zeroLocus_on_compl A I) : MvPolynomial σ K :=
  Classical.choose (zeroLocus_on_compl_mem x S hI hx)

noncomputable example (S : Finset (MvPolynomial σ K))
    (hI : I = Ideal.span S) :=
  ∏ b : zeroLocus_on_compl A I, (selector_j S hI b b.prop - C ((selector_j S hI b b.prop).eval b))

[Daniel Patiño]

Thank you so much @Eric Wieser and @Kevin Buzzard, your help has been invaluable to me. I am currently formalizing Hilbert's Nullstellensatz for finite fields, and defining that polynomial was the biggest obstacle in my work. Thanks to your assistance, I can now continue with the formalization.