Formalization of multideg, division, etc. of MvPolynomial

Stream: general

[Hagb (Junyu Guo)]

Based on section 2 of the book Ideals, Varieties, and Algorithms, I have formalized something about multivariable polynomial in Lean4 (here is the source code repository and my previous zulip topic):

• Term order (modified from Mathlib4 and the answer from Anne Baanen )
• Multidegree and some of its properties
• DIvision of multivariable polynomials and its properties
• Gröbner basis (Groebner basis) and a few properties of it

Are they possible to be feedbacked to Mathlib(4)? (But I think that my codes are probably very naive.)
I am new to both Lean(4) and computational algebraic geometry. Any suggestion will be valuable to me.

[Scott Morrison]

Yes, we'd love to have this material in mathlib4. While the port is still going on it's probably best that "new lemmas for old files" instead get put in new files, along with careful notes about where they should eventually be moved. This is a bit awkward, but hopefully we will only be in this phase briefly.

[Scott Morrison]

I'm a bit confused having an initial look at your work. What is the purpose of the TermOrder type synonym? Don't you need different synonyms for each of the different term orderings? (Or a TermOrder type with additional "unused argument" parameters that specify the term ordering?)

[Hagb (Junyu Guo)]

Scott Morrison said:

I'm a bit confused having an initial look at your work. What is the purpose of the TermOrder type synonym? Don't you need different synonyms for each of the different term orderings? (Or a TermOrder type with additional "unused argument" parameters that specify the term ordering?)

My initial idea was that TermOrder is used to avoid confusion with the original ≤ and < on Finsupp. At the same time, a different term order can be specified through a different TermOrderClass, but I think it is a bad idea that can cause a lot of inconvenience in the future. (I just didn't have better idea at that time.)

Thanks very much for your idea! How about having a LinearOrder argument for TermOrder and let TermOrderClass get LinearOrder as an instance class? (Define TermOrder as def TermOrder (LinearOrder α) (α : Type _) := α and TermOrderClass as class TermOrderClass (β : Type _) [LinearOrder β] ..., and set the LinearOrder α as an instance of LinearOrder (TermOrder α), so we can use TermOrder a_linear_order (σ→₀ℕ) and TermOrderClass (TermOrder a_linear_order (σ→₀ℕ)).)

(Sorry for my bad English, if there is any wrong expression.)

[Scott Morrison]

It seems complicated. I had imagined that we would just be defining lex, deglex, degrevlex, etc, all just as synonyms of σ→₀ℕ, and then defining different linear orders on each of them.

[Hagb (Junyu Guo)]

Scott Morrison said：

It seems complicated. I had imagined that we would just be defining lex, deglex, degrevlex, etc, all just as synonyms of σ→₀ℕ, and then defining different linear orders on each of them.

Each of them has its own multideg, division and so on. How to deal with them?

[Scott Morrison]

Isn't division (of monomials) always just subtraction in σ→₀ℕ? So you need to have those typeclasses "leak" through the synonym. Perhaps I'm misunderstanding what you want, still.

[Yaël Dillies]

@Shing Tak Lam and I have thought about this problem for a while. He's good at Gröbner bases and I'm good at order theory. We'll be done with our exams in 10 days, so watch out.

[Heather Macbeth]

@Yaël Dillies Perhaps you can start by reviewing @Hagb (Junyu Guo)'s code.

[Yaël Dillies]

Yes of course :grinning_face_with_smiling_eyes: but I have zero time right now

[Eric Wieser]

Scott Morrison said:

Isn't division (of monomials) always just subtraction in σ→₀ℕ? So you need to have those typeclasses "leak" through the synonym. Perhaps I'm misunderstanding what you want, still.

I think the difficulty arises with $\frac{x + 2y + 3z}{x+y+z}$, and whether you want the result to be 1, 2, or 3?

[Eric Wieser]

Each of them has its own multideg, division and so on. How to deal with them?

Maybe:

• p.multideg rel, where rel : (σ →₀ ℕ) → (σ →₀ ℕ) → Prop and is_total rel
• p.multideg embedding, where embedding : (σ →₀ ℕ) ↪ L and linear_order L

[Hagb (Junyu Guo)]

Scott Morrison said：

Isn't division (of monomials) always just subtraction in σ→₀ℕ? So you need to have those typeclasses "leak" through the synonym. Perhaps I'm misunderstanding what you want, still.

Sorry for the confusion. When I said "division", I meant this kind of division (or theorem 3 on page 64 of the book Ideals, Varieties, and Algorithms). It depends on the term order, and different term orders can lead to different results.

[Hagb (Junyu Guo)]

Yaël Dillies said：

Yes of course :grinning_face_with_smiling_eyes: but I have zero time right now

Thanks. I will also finish my exams in about 10 days. I will add more comments and documents as soon as I have time.

[Hagb (Junyu Guo)]

Eric Wieser said：

Each of them has its own multideg, division and so on. How to deal with them?

p.multideg rel (where rel : (σ →₀ ℕ) → (σ →₀ ℕ) → Prop and is_total rel), or perhaps p.multideg embedding (where embedding : (σ →₀ ℕ) ↪ L and linear_order L) ?

TermOrder (σ →₀ ℕ) rel and p.multideg rel : TermOrder (σ →₀ ℕ) rel?
One of the reasons I use type synonym TermOrder is to use ≤ for the term order, so that le_xxx lemmas (and many other things) that require something like [Preorder α] can be used to deal with term order.

[Eric Wieser]

Sure, that approach would be reasonable; though I suspect it might be overkill vs just stating things like rel (p.multideg rel) ((X * p).multideg ) instead of p.multideg rel ≤ (X * p).multideg rel

[Eric Wieser]

You can always make local notation in the file, especially if all these constructions are just for intermediate results