## Stream: new members

### Topic: Ideal membership in multivariate polynomial rings

#### Manoj Kummini (Jul 10 2021 at 19:19):

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?

1. 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
1. 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 (Jul 10 2021 at 19:23):

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 (Jul 10 2021 at 19:24):

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 (Jul 10 2021 at 19:25):

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 (Jul 10 2021 at 19:25):

If you use notation, I would suggest local notation.

#### Manoj Kummini (Jul 10 2021 at 19:39):

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 (Jul 10 2021 at 20:04):

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 (Jul 11 2021 at 00:49):

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

Last updated: Dec 20 2023 at 11:08 UTC