mathlib

mathlib copied to clipboard

This PR defines

1. the sup_degree of an add_monoid_algebra, graded by a semilattice_sup;
2. the inf_degree of an add_monoid_algebra, graded by a semilattice_inf;
3. the max_degree of an add_monoid_algebra, graded by a linear_order with a bottom element;
4. the min_degree of an add_monoid_algebra, graded by a linear_order with a top element.

It also proves that under addition and multiplication in the add_monoid_algebra, each degree behaves as expected.

The lemmas are there simply to give a sample usage of the new definition.

Please, let me know which of these definitions seems more useful, or whether you think that different assumptions would be better.

---

• [x] depends on: #15413

Good point about trailing degrees! I added the definition and the result about the trailing_degree of a product.

Sorry about the confusion: I've made a mess with Git. I will try to fix it!

In case you are curious, you can take a look at this diff for an immediate application of the results in this file: proving that degrees of actual polynomials "sub-multiply", using the general theory.

Once more results for general degrees of add_monoid_algebras are in, I think that there will be more simplifications and also these lemmas will work equally well for Laurent polynomials and I am hoping also for mv_polynomials. However, I have not played much with mv_polynomials, so I cannot say for sure.

Maybe we should define a degree for every map (ideally homomorphism) from the add_monoid to an arbitrary linear_ordered_monoid. This would unify multiple notions: for polynomials and Laurent polynomials, the linear_ordered_monoid would be ℕ or ℤ with the order (≤) or (≥) depending on whether you want the max or min degree. For mv_polynomial, total_degree would be obtained using the sum homomorphism to ℕ, and you can also obtain degree in individual variables using projection to that variable. This is an argument that needs both the max and min total_degree, which I formalized. We can also develop some theory of grading around it, and maybe filtration (which seems lacking in mathlib).

@alreadydone: aren't you just advocating for giving a name to x.support.sup f? Do we need a new name for that idea?

@alreadydone I had a similar reaction as you and if you look higher up, you'll see that Eric already made his point.

I agree with Eric, though: the generic stuff "just works" and has a short enough spelling that I like it. The most used versions will likely be min_degree, max_degree and maybe a couple more specialized ones for mv_polynomials involving a choice of variable. These will get special support and custom made lemmas. The rest will be supported, but using the "generic" form.

At least, this is how I view it and how I interpreted Eric's remark!

@adomani I only just subscribed to this PR so I am not aware of the prior discussions; can you point to the relevant ones? I wonder why you didn't prove the inequality between the degree of f + g and the sup of degrees. I see that you work with the more general semilattice_sup instead of linear_order, and min_degree could be unified with max_degree if you use with_top.to_dual_bot, though you chose not to do so. However, mv_polynomial.total_degree cannot be easily fit into this framework, because the sup of (1,2), (2,1) would be (2,2) with total degree 4, but xy^2-yx^2 is homogeneous of degree 3; if you map x and y to the same variable and take polynomial.degree, it cancels out and we get bot as the degree. If you want the degree in a certain variable, you can indeed use mv_polynomial.option_equiv_left to map it to a single-variable polynomial ring, but that's certainly cumbersome. I'm just suggesting that a small generalization of the approach here that would allow unifying multiple notions and possibly get rid of some code duplication. Using hom to a linear_ordered_comm_monoid also seems clearer than using covariant classes.

I wonder why you didn't prove the inequality between the degree of f + g and the sup of degrees.

I agree this would be a good result to include

I see that you work with the more general semilattice_sup instead of linear_order, and min_degree could be unified with max_degree if you use with_top.to_dual_bot, though you chose not to do so.

We could unify ⨅ and ⨆ globally too via order duals, but we don't because that would be annoying!

However, mv_polynomial.total_degree cannot be easily fit into this framework, because the sup of (1,2), (2,1) would be (2,2) with total degree 4, but xy^2-yx^2 is homogeneous of degree 3; if you map x and y to the same variable and take polynomial.degree, it cancels out and we get bot as the degree.

The "total degree" operation is spelt x.sup (λ x, x.1 + x.2), which still works with the lemma in this PR I think.

(whoops, mobile misclick!)

@alreadydone I'll answer better tomorrow: I'm going to bed now! I only included one result, since I wanted to focus more on the definition, than on the lemmas. I intend to prove the sum result that you mention, as well as all the lemmas that make degree look like valuations. Off to bed now!

The "total degree" operation is spelt x.sup (λ x, x.1 + x.2), which still works with the lemma in this PR I think.

Oh indeed, thanks for pointing that out! I had the wrong picture how finset.sup works in this case. Now I think the theory developed here is at maximal generality. Though it may be too general, so that you have to carry around the covariant classes and D0, Dm. I think it's best to provide a version of the lemmas with linear_ordered_add_comm_monoid B and D being a add_monoid_hom, which is probably the most useful case.

@alreadydone I agree that, most of the times, "degree" refers to an integer associated to a (mv_)polynomial and that for such applications a linearly ordered additive commutative monoid (possibly with top or bottom) will be enough.

However, non-linearly ordered target monoids do show up in maths as well. You can search for multigraded {rings, ideals, Hilbert series,...} to see some of these. In these situations, various quotients of the grading monoid can be useful, not just the linearly ordered ones.

To conclude, in my view the current file is a good representation of what should happen, except for relative sizes. There are the general results about sups (e.g. sup_support_mul_le) with lots of hypotheses. Then there are the specialized lemmas (e.g. max_degree_mul_le, le_min_degree_mul) with the most common usage. Note that these two lemmas are indeed proved using the same generic lemma, thanks to order_dual.

Of course, I imagine quite a few more lemmas to be added to this file! :smile:

I hope that this clears up the directions where I think/hope I am going!

However, non-linearly ordered target monoids do show up in maths as well. You can search for multigraded {rings, ideals, Hilbert series,...} to see some of these. In these situations, various quotients of the grading monoid can be useful, not just the linearly ordered ones.

@adomani: I'm not convinced that non-linearly ordered targets are useful. Can you elaborate on your examples? We have add_monoid_algebra.grade_by.graded_algebra to deal with gradings, which doesn't require any order, but degree seems to be a different matter. linear_order ensures that sup is max, so degree = n means that the element decomposes into a nonzero purely degree-n piece plus some pieces of strictly lower degree, but if it's only a semilattice_sup, the degree-n piece may be zero (as in the xy^2-yx^2 example above), so the degree doesn't seem very useful notion in this case. Note that linear_order is also necessary to carry out the argument of yours I mentioned above.

@alreadydone, maybe I should make a distinction. I personally do not even know the exact definition of semilattice_sup and I was viewing it as a way of generalizing a partial_order. As for partial orders, imagine that you have a polynomial ring $R = \mathbb{Q}[x_1, \ldots , x_n]$ in several variables and an ideal $I \subset R$. If you want to compute the elimination ideal of $I$ with respect to the variables ${x_1, \ldots , x_i }$, you usually choose an appropriate total ordering on the monomials so that the variables ${x_1, \ldots , x_i }$ are first (or last), the remaining are last (or first) and you compute the initial ideal.

This argument uses total orders. However, there is no need to give a relative ordering the variables ${x_1, \ldots , x_i }$ or the remaining variables: any appropriate partial order where $a \in \{1,\ldots,i\}, \; b \in \{i+1,\ldots,n\} \; \Rightarrow \; x_a < x_b$ would do. These kinds of "obvious" reductions can be painful to formalize, but would work smoothly with a more general background. Of course, you could formalize this by going via an identification of all the first variables to a single element and all the last variables to a different one... but why, if you can avoid it?

As for defending semilattice_sup: maybe you are right and it will never be useful. But would the proofs so far have gotten easier with a stronger assumption?

But would the proofs so far have gotten easier with a stronger assumption?

The proofs may not get easier, but the statements will certainly be shorter with [linear_ordered_add_comm_monoid B] and D : A →+ B (or add_hom A B for some lemmas; these would impose equalities map_add, map_zero instead of inequalities, but I can't think of examples where equalities don't hold).

As for the example you gave:

• You seem to be thinking about ordering on A instead of on B, and I agree that the natural order on A is often not total, but I think when you want to talk about degrees you'd map it to some total order B.

• You talk about monomials; a monomial certainly has a well-defined degree independent of the choice of an ordering, and IMO that belongs to the theory of gradings instead of the theory of degrees.

• If you have multiple monomials and want to express that all of them have degree ≤ x, you can write f.support.map D ⊆ set.Iic x, which doesn't require the existence of sup; requiring the sup of the support to be equal to x seems to bear no special meaning, unless B is a linear order so a monomial of degree x is guaranteed to exist.

• In commutative algebra algorithms like the one you mentioned, I think one usually wants to choose a monomial of maximal degree, not a possibly non-existent monomial at the sup degree, e.g. for xy^2-yx^2 no monomial exists in the sup degree (2,2), so you'd upgrade to a linear order so that either (1,2) or (2,1) becomes the max.

In summary, I think assigning a degree to a finset of monomials just doesn't make much sense unless the degree takes values in a total order.

In summary, I think assigning a degree to a finset of monomials just doesn't make much sense unless the degree takes values in a total order.

I think we should be proving the lemmas about sup (support x) in the most general setting, whether or not that setting seems interesting.

I do see your point that having max_degree and min_degree work without a total order is less useful; what exactly are you suggesting we do instead?

I thought I was reviewing this PR, but actually left the comments on #15376! Would you mind addressing the relevant comments in this PR?

I don't think there's any particular need to split the two PRs, but at the same time it;s fine if you want to.

I felt that it was easier to discuss about the definitions with fewer lemmas around, but since the discussion is going on anyway, I'll commit your changes to the other branch, merge it into this one and close the other PR.

@eric-wieser, I applied the changes that you suggested in the other PR and have closed the other PR. Sorry about the confusion: I hoped that it would create less clutter to open a new one containing only lemmas, but it achieved the opposite!

@eric-wieser and @alreadydone On the topic of which generality to define degrees. Currently, the only degrees that appear in mathlib are the standard nat-valued one on polynomials, the int-valued on laurent_polynomials and possibly a couple of variations for mv_polynomials. I cannot come up with a good example of a partial order that is not total where degrees would be important. I have a slight feeling that for multivariable polynomials, it could be useful to have an order that is the componentwise less than or equal on the list of exponents. However, I agree that currently, and maybe for quite some time this would not be used. It is probably easy to make either choice now and change it, if needed, later on, so I am not particularly pushing in either direction.

I have an impression that whenever I have added unnecessary hypotheses to a definition, I later regretted it. I am also thinking of people wanting ideals over comm_ring, then over comm_semirings, then over semirings and similar generalizations in the order-hierarchy.

Anyway, let me know if you want to change the definition of min/max_degree and I will do it!

I suppose the super conservative thing to do would be to not define min_degree and max_degree at all in this PR, and define them later if it turns out we need them.

My understanding is that the main value in this PR is that it should permit us to golf the proofs of various statements about the types of degree @adomani mentions for derived types; in which case, we don't get much value from these definitions anyway.

@eric-wieser, @alreadydone

This diff (just the file on degree of polynomials), is the kind of use that I have in mind for the lemmas in the current file. I would probably never guess the way to golf these results if they were not packaged so nicely with min/max_degree, but, once you know where to look, the name is irrelevant. After all, the proofs are simple specializations and the definitions are defeq.

The conclusion is that I would find it more user-friendly to have the definitions in place, but I agree that they are there mostly for psychological value, not for anything else. I do think that someone might look for some form of "degree" defined on an add_monoid_algebra with some not insanely general assumptions. Whether it is reasonable that they should find something or not, I am not too sure!

I'm not against generality; in fact, I just found one use case in mathlib where B is not a linear_order: mv_polynomial.degrees, so I'm in favor of keeping the smilattice_inf versions (D is still a homomorphism though.)

I do think the current lemmas would be more convenient to use if specialized to the linear_order case. If they're gonna be used in 3 situations that all have B being linear_order then we should probably do the specialization here instead at each of the 3 situations. Maybe we should reserve max_degree and min_degree for the linear_order case, and rename them to sup_degree and inf_degree in the semilattice_sup/inf case. The linear_order version would be stated using [linear_ordered_add_comm_monoid B] and D : A →+ B, which would be more convenient to use, as the D0, Dm hypotheses cannot be supplied by typeclass inference.

There are also many lemmas that hold for linear_order but not general semilattice_inf; polynomial.degree_add_eq_left_of_degree_lt (consider p = xy^2-yx^2 and q = yx^2), and ~~polynomial.degree_mul' (leading_coeff only really makes sense in linear_order case)~~ (sorry, can't really state it this way unless D is injective; would need to use graded_ring.proj/decompose).

I like the point that the current definition of max_degree should really be named sup_degree.

I just pushed a version containing the two options that we have been discussing.

• I renamed max/min_degree to sup/inf_degree.
• I created two new definitions of max/min_degree using linear orders.

I think that having both versions is excessive, so this is simply for comparing the two: I plan to remove one of the two pairs of definitions.

I probably prefer the linear order version (which was also the very first version that I had in this PR). My only slight worry is that we might regret later the artificially crippled generality, but I can live with the idea of a possible refactor, should it be useful.

@eric-wieser, @alreadydone which version do you prefer? Do you have any other suggestions?

Can you split out all the lemmas about .support.sup and .support.inf to a new PR (without any of the new definitions) so that we can get those merged?

The correct choice for the max/min/sup/inf_degree convenience aliases is clearly contentious, and so I think it makes sense to factor out the non-contentious bit to a new PR.

@eric-wieser: #15413 Splitting seems like a very good idea!

This PR/issue depends on:

• ~~leanprover-community/mathlib#15413~~ By Dependent Issues (🤖). Happy coding!

Can you please merge master to see if it still works?

@riccardobrasca merging master worked with no changes!

What's the status of this?

I was under the impression that, as the basic assumptions for the definitions were controversial, this PR may have stayed a PR until someone had a compelling reason to force a choice.

Several months later, mathport started.

I've mathport oneshot'd creating a branch which @adomani will turn into a Mathlib4 PR.