Combinatorial Nullstellensatz

Stream: maths

[Iván Sadofschi Costa]

Hi! I'm working on a proof of the Combinatorial Nullstellensatz:

theorem combinatorial_nullstellensatz { n : ℕ } {F : Type u} [field F]
    (f : mv_polynomial (fin n) F) (t : fin n →₀ ℕ) (h_max : max_degree_monomial t f)
    (S : fin n → finset F) (h_card_S : ∀ i : fin n, t i < (S i).card) :
    ∃ s : fin n → F, (∀ i : fin n, s i ∈ S i ) ∧ eval s f ≠ 0 :=

A possible way to define max_degree_monomial would be the following (is this definition reasonable?):

def monomial_degree {s : Type} (t : s →₀ ℕ) : ℕ := ∑ i in t.support, t i

def max_degree_monomial  { n : ℕ } {F : Type u} [field F]
(t : fin n →₀ ℕ) (f : mv_polynomial (fin n) F) : Prop :=
t ∈ f.support ∧ monomial_degree t = total_degree f

I am following Alon's original paper which is available at http://www.math.tau.ac.il/~nogaa/PDFS/null2.pdf

Most of the machinery needed to prove this result is already on mathlib (e.g polynomial.card_roots, mv_polynomial.fin_succ_equiv).

To complete the proof I still have to prove many smaller lemmas about coeff, degree_of, total_degree.

For the moment I have a complete proof of Lemma 2.1 in Alon's paper which already seems something nice to have in Mathlib:

-- What is a reasonable name for this one?
lemma lemma_2_1 { n : ℕ } {F : Type u} [field F]
  (f : mv_polynomial (fin n) F) (S : fin n → finset F)
  (hS : ∀ i : fin n, degree_of i f < (S i).card)
  (hz : ∀ s : fin n → F, (∀ i : fin n, s i ∈ S i ) → eval s f = 0) :
  f = 0

In order to prove this result I had to state and prove many lemmas about polynomials and mv_polynomials that seem useful, for example the following:

lemma fin_succ_equiv_coeff_coeff {n : ℕ} {R : Type u} [comm_semiring R]
  (m : fin n →₀  ℕ) (f : mv_polynomial (fin (n+1)) R ) (i : ℕ) :
  coeff m (polynomial.coeff (fin_succ_equiv R n f) i) = coeff (fin.finsupp.cons i m) f

It seems that cons and tail were not yet defined for maps fin n →₀ ℕ:

def fin.finsupp.tail {n: ℕ } (s : fin (n+1) →₀ ℕ ) : fin n →₀ ℕ

def fin.finsupp.cons {n:ℕ} (y : ℕ) (s : fin n →₀  ℕ) : fin (n+1) →₀ ℕ

If these are not already on mathlib, should I open a PR with cons, tail and their properties? I'm not sure where to put these.

[Alex J. Best]

You probably have seen it but you should definitely check out https://github.com/leanprover-community/mathlib/blob/master/src/data/mv_polynomial/variables.lean if you haven't already.
In https://github.com/leanprover-community/flt-regular/blob/master/src/ring_theory/polynomial/homogenization.lean I've been proving a lot of related things about the sum of leading terms, total degrees, supports, homogenizations etc. I'm now PRing this stuff to mathlib, but maybe some of it is useful for you already.

[Alex J. Best]

It seems a bit strange to talk about fin n →₀ ℕ, after all fin n is finite, and so finitely supported functions on fin n are just functions on fin n, can you rephrase things to be about functions on fin n instead, then maybe there will be more api there for you

[Alex J. Best]

We also tend to try and use general fintypes where possible rather than specializing to fin n for main results. Of course along the way it might be easier to deal with fin n, and then to prove the main result in general at the end by picking an equivalence between a finite type and fin n. But I'd definitely encourage you to see which of the lemmas are about fin n and which are about some general fintype.

[Alex J. Best]

Its really cool that you are working on this!

[Iván Sadofschi Costa]

Alex J. Best said:

You probably have seen it but you should definitely check out https://github.com/leanprover-community/mathlib/blob/master/src/data/mv_polynomial/variables.lean if you haven't already.
In https://github.com/leanprover-community/flt-regular/blob/master/src/ring_theory/polynomial/homogenization.lean I've been proving a lot of related things about the sum of leading terms, total degrees, supports, homogenizations etc. I'm now PRing this stuff to mathlib, but maybe some of it is useful for you already.

Thanks, it seems that many of this will be useful here too!

[Iván Sadofschi Costa]

Alex J. Best said:

It seems a bit strange to talk about fin n →₀ ℕ, after all fin n is finite, and so finitely supported functions on fin n are just functions on fin n, can you rephrase things to be about functions on fin n instead, then maybe there will be more api there for you

Yes, I agree that this is strange. I used fin n and fin (n+1) here following the definition of fin_succ_equiv:

def fin_succ_equiv (n : ℕ) :
  mv_polynomial (fin (n + 1)) R ≃ₐ[R] polynomial (mv_polynomial (fin n) R)

This leads to considering maps s:fin n →₀ ℕ as the X^s. Is there a way to apply the usual cons and tail directly to these maps?

[Iván Sadofschi Costa]

I've finished the proof some days ago: https://github.com/isadofschi/combinatorial_nullstellensatz
There is a lot that I have to tidy before submitting the main results, but I'm happy that it works!
For now I'm sending PR's with lemmas about mv_polynomials.
Many results from flt-regular were useful in the proof. Thanks @Alex J. Best for pointing me to homogenization.lean!