3 basic definitions

Stream: PR reviews

[Kenny Lau]

1. #26192 : Symmetric tensor power
2. #26060 : Grassmannians of a module
3. #26285 : Resultant of two polynomials

I think these three basic definitions have been sitting for a while. Let me summarise the main controversy:

1. It has been suggested that Fin n should be generalised to an arbitrary Fintype (or even type), but I don't think this is necessary (the one that this depends on, which is tensor power, also uses Fin n).
2. There's a submodule-definition and quotient-definition, I'm now convinced that we should include both at some point, so I've named this Module.Grassmannian to make space for a future definition using submodule-convention.
3. I don't think there's any big issue. The only comment there is naming sylvester into sylvesterMatrix but I think a shorter name is better.

[Andrew Yang]

has been sitting for a while

If you look at the #queueboard, then there are 100+ PRs that has got no reviews for weeks and if the queue is a genuine FIFO then they will have to be reviewed before yours is. I would admit that this is very unfortunate, but pointing out the problem doesn’t really solve it and several people are working really hard on trying to increase the review capacity of mathlib. In the meantime I think you might need to be a bit more patient.

[Yaël Dillies]

... or review PRs yourself, to take pressure off the official reviewers :innocent:

[Kenny Lau]

@Andrew Yang I apologise for bringing more trouble. I understand that people are busy. I'll tune down the frequency, and review some other PR's.

[Michael Rothgang]

I also understand the frustration that very basic or straightforward PRs can take very long!

[Michael Rothgang]

In my experience, the best way to get your PRs in is to (a) reciprocate, i.e. review other PRs, and (b) find somebody else who finds this PR or the eventual goal exciting and hence is willing to review yours. Both of these have some barrier to entry, sadly.

[Kenny Lau]

@Yaël Dillies Thanks for your comments on the resultant. As explained there, I think I would prefer to do the left versions in a later PR where I prove a commutativity formula, which hinges on a future PR of the sign of the permutation Fin(m+n) to itself flipping the m and n part.

[Yaël Dillies]

Already replied :wink:

[Kenny Lau]

@Yaël Dillies and changed :slight_smile:

[Wrenna Robson]

@Michael Rothgang OOI, is there some special permission or qualification we need to review other people's PRs? I don't do it because I felt I hadn't been given responsibility or, more crucially, permission to do so.

[Aaron Liu]

From the pull request review guide:

While the mathlib maintainers are the only users with authority to merge pull requests, everyone is welcome, and even encouraged, to review pull requests. (Note: there is in fact another category of people, mathlib reviewers, who have shown that they can provide valuable PR reviews; approving reviews from these users with maintainer merge are more quickly merged by maintainers).

[Ruben Van de Velde]

So, yes please, if there's a PR you're interested in, any signal that a second person has looked at the code (and especially if they're happy about it) is helpful

[Michael Rothgang]

What Aaron and Ruben said - reviews are very very welcome!

[Michael Rothgang]

Mathlib needs more reviewers, and since these don't simply grow on trees, one of the most useful contributions to mathlib is to review others' work.

[Michael Rothgang]

(Another useful avenue is doing PR triage. If that's your thing, DM me and we can talk.)

[Kenny Lau]

Let's discuss the thing about #26192 Sym^n[R] M here. Basically, I've defined it using Fin n as the indexing set, because symmetric power is a quotient of the tensor power, and tensor power uses Fin n.

@Andrew Yang @Antoine Chambert-Loir What are your opinions on this? Do we need an arbitrary indexing?

[Antoine Chambert-Loir]

I am not sure it is needed, but that would give more flexibility in applications. However, as soon as you use docs#TensorPower, you would have to refactor the latter first. Maybe that's not the most urgent thing to do. In the TODO section, you indicate planning to define the graded structure; then it's not clear to me how you would frame it (the sum of fintypes?) but it will be necessary for applications to have the indexation by natural numbers as well.

[Wrenna Robson]

@Michael Rothgang alright! I will try and do more reviews. What is the pathway to being recognised as a reviewer - do well at that a lot?

[Michael Rothgang]

Becoming an official reviewer is a bit like the hollywood principle: if you provide good reviews, you will be asked to join the reviewers group, at some point. At the same time, you don't have to be an official reviewer to provide helpful reviews!

[Michael Rothgang]

If you looked at a PR and everything looks good to me, you can create a thread in this stream to raise attention to it; even a short message "this PR looks good to me, would a reviewer like to take a look" can do. A (still too) significant share of PRs get overlooked to easily, and surfacing them is helpful.

[Michael Rothgang]

Over time, people may ask you for your opinion on PRs (say, if you commented on similar PRs before).

[Michael Rothgang]

In any case: it's great to hear you're willing to help out here. Don't forget to have fun, and don't hesitate to ask if anything is unclear!

[Kenny Lau]

Antoine Chambert-Loir said:

then it's not clear to me how you would frame it (the sum of fintypes?) but it will be necessary for applications to have the indexation by natural numbers as well.

a map from Sym^i M x Sym^j M to Sym^(i+j) M.

Note that this is another reason I'm opposed to the arbitrary fintype approach: in the grading thing you're doing a sum anyway, the gradedRing API literally requires you to use addition

[Andrew Yang]

The point is you don't need fintypes to define symmetric power.
I don't see how you cannot recover the original behaviour if you feed it Fin n; it is strictly more general.

[Kenny Lau]

well the main thing is still that this would require me to refactor TensorPower first and who knows how long that PR will take

[Antoine Chambert-Loir]

Indeed. And this is a general issue for mathlib, that one cannot put too much on people the responsability of refactoring previous works of others so that they get the optimal generality. On the other hand, if nobody does that, mathlib might get blocked by unsufficient general definitions/theorems.

[Antoine Chambert-Loir]

In this case, this looks straightforward, except possibly for the graded structure, and docs#TensorProduct.gsemiring would take the form

instance gsemiring : DirectSum.GSemiring fun i => ⨂[R]^(Fin i) M :=
...

Do we want that? @Eric Wieser

[Antoine Chambert-Loir]

Or do we want to keep the notation for the tensor powers of Fin n only? Or have a special notation for this case?

[Eric Wieser]

I don't feel strongly either way

[Kenny Lau]

@Matthew Ballard sorry, I didn't quite understand your comment

[Kenny Lau]

what should I add to the description?

[Matthew Ballard]

We will have two competing ways to handle the difference between a multi-linear module and the algebra the direct sum forms. For docs#TensorProduct and docs#TensorAlgebra, both types are built in natural ways and then the equivalence between the two is given. For docs#ExteriorAlgebra and docs#ExteriorPower, the latter devolves from the former as a span.

We already have docs#SymmetricAlgebra and this PR goes along the tensor path.

Each approach has advantages and disadvantages.

It would be good to record why this approach was chosen for future reference. This can include specific immediate applications in mind. It would also be good to leave some breadcrumbs for future readers so they understand the pattern and can better see the holes in the API.

Don't document the mathematics itself so much but the reasoning for the design choices and the motivation for the choices.

[Kenny Lau]

I'm not sure there's one canonical reason why we do A and not B, as you said, both have advantages and disadvantages, it's pretty arbitrary imo

[Matthew Ballard]

Sure but there are answers of the form "I want to establish X for which the shape of this type is better suited".

That one yields a term of size an order of magnitude larger than the other is most compelling to me here so it can be simpler to work with this definition if I am mainly concerned about the module structure of each symmetric power instead of things relating to multiplying symmetric terms.

[Kenny Lau]

@Matthew Ballard I think building the stuff about symmetric multilinear maps will be easier using this definition. I have (already) included this goal in the PR description.

[Kenny Lau]

Also, I feel like this comment doesn't even apply now, since we have generalised symmetric powers away from finite indexes.

[Kenny Lau]

there's no choice anymore, you can't build the infinite symmetric power out of the symmetric algebra

[Kenny Lau]

I mean, I think that infinite symmetric power is not a verywell-motivated mathematical object, but that's besides the point

[Kenny Lau]

Is #26192 ready?