Ideal membership in multivariate polynomial rings

Stream: new members

[Manoj Kummini]

I am trying to write a formal proof that a polynomial $f$ in a multivariate polynomial ring $R$ is a member of an ideal $I$ of $R$. This is typically done using Grobner bases. I am relatively new to lean. Looking at old discussions, I understood the following:

1. There is no Grobner basis tactic in mathlib, so a suggested approach is to compute a Grobner basis of $I$ and a candidate expression that writes $f \in I$ using some other program and verify this expression in lean.

2. I tried to do this for a small example: show that $X_0^2 + X_1^2$ belongs to the ideal $(X_0,X_1)$ of the ring $F_2[X_0, X_1]$. Though this particular example can be done in more general commutative rings using rw pow_two, I tried the following (non-working) minimal example in lean:

import data.mv_polynomial.basic
import data.mv_polynomial.comm_ring
import data.zmod.basic

open mv_polynomial

def R := mv_polynomial (fin 2) (zmod 2)

example :
  let f :=  (X 0)^2 + (X 1)^2,
      f1 := X 0,
      f2 := X 1,
      in
      f = (X 0) * f1 + (X 1) * f2 :=
begin
  sorry
end

Lean did not recognize X. What should I be doing?

3. Is it possible to refer to mv_polynomial (fin 3) (zmod 2) by some easier name within my code? E.g., I was able to copy-paste some examples from zulip discussions and make them run, but when I tried to refer to it as R after doing a

def R := mv_polynomial (fin 2) (zmod 2)

I got some errors. Here is an example.

import data.mv_polynomial.basic
import data.mv_polynomial.comm_ring
import data.zmod.basic

open mv_polynomial

example :
  let I := ideal.span { x : mv_polynomial (fin 3) (zmod 2) | ∃ (i : fin 3), x = X i} in
  (X 0 : mv_polynomial (fin 3) (zmod 2)) ∈ I :=
begin
  sorry,
  -- I get "goals accomplished" at this step.
end

-- I would like to give a name to the ring.
def R:= mv_polynomial (fin 3) (zmod 2)
#check R

example :
  let I := ideal.span { x :  R | ∃ (i : fin 3), x = X i} in
  (X 0 : R) ∈ I :=
begin
  -- there is a red squiggly line below the word `ideal' above
  -- I get an error failed to synthesize type class instance for
  -- ⊢ semiring R
  sorry,
  -- no "goals accomplished" message at this step.
end

4. Is it possible to check in Lean whether a set of polynomials is a Grobner basis (e.g. using Buchberger's theorem)? In the proof I would like to formalise, I need to show that $f \not \in I$ and $X_if \in I$ for every variable $X_i$. To do this, one strategy would be to compute a Grobner basis $G$ of $I$ and the remainder $\tilde{f}$ of $f$ after reducing it modulo $G$ using some other program , prove in lean that it indeed is a Grobner basis, and then show that the leading terms do not divide the leading term of $\tilde{f}$.

Thanks.

[Johan Commelin]

Lean did not recognize X. What should I be doing?

It doesn't know that you want f to be a term of type R. If you write let f : R := ... I think things will be better.

[Hanting Zhang]

AFAIK using def a := b will not carry the instances on b to a; you can try defining it as local notation instead

[Johan Commelin]

Is it possible to refer to mv_polynomial (fin 3) (zmod 2) by some easier name within my code? E.g., I was able to copy-paste some examples from zulip discussions and make them run, but when I tried to refer to it as R after doing a

def R := mv_polynomial (fin 2) (zmod 2)

I got some errors

The problem is that you gave a new definition, and Lean does not automatically see through this (for good reasons). So now it doesn't know anything about R.

Solutions could be to use notation or abbreviation instead.

[Johan Commelin]

If you use notation, I would suggest local notation.

[Manoj Kummini]

Thanks. The following code worked.

import data.mv_polynomial.basic
import data.mv_polynomial.comm_ring
import data.zmod.basic

open mv_polynomial

abbreviation R := mv_polynomial (fin 2) (zmod 2)

example :
  let f : R :=  (X 0)^2 + (X 1)^2,
      f1 : R := X 0,
      f2 : R := X 1
      in
      f = (X 0) * f1 + (X 1) * f2 :=
begin
  ring,
  rw pow_two,
  rw pow_two,
end

[Kevin Buzzard]

begin
  ring_exp,
end

is a shortcut (or even by ring_exp) -- this is a variant of ring which knows more about the arithmetic of exponents.

[Manoj Kummini]

Thank you. ring_exp is substantially faster; ring takes about a minute to rewrite the goal.