Zulip Chat Archive
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:

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.

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 (nonworking) 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?
 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 copypaste some examples from zulip discussions and make them run, but when I tried to refer to it asR
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
 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 copypaste some examples from zulip discussions and make them run, but when I tried to refer to it asR
after doing adef 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