Degrees of polynomials in many variables

Stream: maths

[Antoine Chambert-Loir]

The definition of #mv_polynomial.degrees looks very strange to me, at least I had never encountered it in mathematics.
It defines, for example, the degrees of $P = x^2y+y^3$ to be the multiset $\{x,x,y,y,y\}$ whose product gives $x^2y^3$, a least common multiple of the monomials that appear in the polynomial $P$.

From the perspective of computer algebra, I would have imagined that the degrees of $P$ would be either $\{x^2y,y^3\}$ or $\{ (2,1), (0,3)\}$, the set of (uncoefficiented) monomials or of exponents.

What is the reason it was introduced in this way?

[Eric Wieser]

What would you expect the degree of $P = x^2y + y^3 + y$ to be?

[Eric Wieser]

(also, you need docs before the # for the link to work)

[Antoine Chambert-Loir]

There are many degrees available, the three obvious ones are the degree with respect to $x$ (2 in this case), the one with respect to $y$ (3), or the total degree (3 as well). But you can assign weights to variables and you get many other, of a similar vein.

These degrees do not give rise to a total ordering of monomials, and the theory of Gröbner bases proposes that you fix a total ordering of the monomials, and then the degree would be the exponent of the highest monomial.
One way to get such an ordering consists in fixing weights which are linearly independent over Q, and taking the degree then. But the lexicographic orderings, or their opposite, are also pretty much studied. (So the degree could be $x^2y$ if you take the variables in the standard order, or $y^3$ if you start from $y$.)

[Kevin Buzzard]

The definition was made by Johannes Hoelzl who has a computer science background and might well know very little about what mathematicians use multivariable polynomials for. I wouldn't take the definition too seriously Antoine -- Johannes might just have come up with an arbitrary definition which happened to basically agree with the usual definition in the single variable case. Polynomials were in a very experimental state four years ago.

[Antoine Chambert-Loir]

OK, so since @María Inés de Frutos Fernández and I are revisiting that in order to define more general weights on polynomial algebras (in order to define the the divided power algebra of a module, we could also revise this as well. It does not seem to be much used anyway.

[Kevin Buzzard]

Jujian Zhang has made projective space in Lean but I think weighted projective space would also be a welcome addition -- perhaps not by you two, who are doing more important stuff, but please bear it in mind if you're going to make new definitions of degree :-)

[Antoine Chambert-Loir]

Indeed…

[Junyan Xu]

Antoine Chambert-Loir said:

From the perspective of computer algebra, I would have imagined that the degrees of $P$ would be either $\{x^2y,y^3\}$ or $\{ (2,1), (0,3)\}$, the set of (uncoefficiented) monomials or of exponents.

This is basically docs#mv_polynomial.support.

There are many degrees available, the three obvious ones are the degree with respect to xx (2 in this case), the one with respect to yy (3), or the total degree (3 as well).

docs#mv_polynomial.degree_of and docs#mv_polynomial.total_degree

But you can assign weights to variables and you get many other, of a similar vein.
But the lexicographic orderings, or their opposite, are also pretty much studied.

#15296 and #16127 (not yet merged) by @Damiano Testa

[Damiano Testa]

My recollection was that there was some resistance on introducing "degrees" for general add_monoid_algebras. It may be quicker to define degree in the special case of mv_polynomials and then worry later if/when more general notions of degrees are desired.

Partially related: there is also a counterexamples file where there is some reasoning about "exponent vectors" of add_monoid_algebras. For instance zero_divisors_of_periodic and zero_divisors_of_torsion in counterexamples/zero_divisors_in_add_monoid_algebras.

[Damiano Testa]

I also have other PRs open with a proof that mv_polynomials only have trivial zero divisors when the base-ring does, but am not pushing them to get merged, since

• I currently do not have much time;
• would rather focus on the port, if/when I will have time!

[Junyan Xu]

Just found out that PRs #17855 and #17956 are now open.

[Yaël Dillies]

#17856, you mean?

[Antoine Chambert-Loir]

Junyan Xu said:

Just found out that PRs #17855 and #17956 #17856 are now open.

Yes, these are the PRs in which @María Inés de Frutos Fernández and me
1/ defined weighted degrees on mv_polynomial, associated to weights on the indeterminates (they can take value in any additive monoid)
2/ refactored the notion of a homogeneous polynomial in these terms (all the weights are 1 : nat).

(But this only related to the thread by the fact that it involves polynomials in several variables.)