Symmetric Functions

Stream: Is there code for X?

[Jesse Selover]

Is there any code related to symmetric functions or symmetric polynomials in mathlib?

[Heather Macbeth]

There's a draft PR of @Johan Commelin, #3169

[Jesse Selover]

Thanks! I'll take a look

[Alessandro Iraci]

Is anyone still working on this? I'm aware of #3169 but it seems like there has been no progress in a while. I would be interested in joining / restarting this project!

[Kevin Buzzard]

That's a mathlib3 PR. We have docs#MvPolynomial.IsSymmetric in mathlib4.

[Alessandro Iraci]

Cool, thanks! It seems to me that there is still nothing for symmetric functions though? My long term goal would be to have Macdonald polynomials and plethysm, but symmetric functions would be a good starting point.

[Ruben Van de Velde]

Maybe #6593 is of interest to you?

[Yaël Dillies]

Actually Terence Tao proved quite a few things related to symmetric polynomials

[Alessandro Iraci]

Interesting! So, symmetric functions are the colimit in n, in the category of graded rings (this is important), of symmetric polynomials in n variables. This implies that pretty much all the results about symmetric polynomials can be deduced from more general statements about symmetric functions.

I think it should be feasible to have a working implementation of symmetric functions relatively quickly, considering that some stuff about symmetric polynomials is already in the library. There is a fairly large community in algebraic combinatorics that I'm sure would be very into it. I'm a beginner though, so I don't know where I should start from.

From that one could build up and define plethysm (which I am very much interested into), Macdonald polynomials, and ideally the most important stuff appearing in https://www.symmetricfunctions.com/index.htm. Having lambda-rings and Hopf algebras might also be useful.

[Alessandro Iraci]

Hi again. I tried starting scribbling something. It seems to me that the easiest way to define the algebra is to define it as the free commutative graded polynomial algebra on countably many indeterminates e_1, e_2, .... I think I can do it, but I do not understand how to define the grading so that e_n has degree n. I tried looking at the examples but couldn't find anything.

Can anyone help? Is this the correct place where to ask? Thanks!

[Riccardo Brasca]

I think it is already there, in some form. We have docs#AddMonoidAlgebra.grade.gradedAlgebra that looks very promising

[Riccardo Brasca]

Mmm, no, maybe it's not what you want exaclty. Do you want to define the ring $R[x_0, x_1, \ldots]$ and putting a graded ring structure on it?

[Alessandro Iraci]

Sort of? I want to define the ring $R[e_1, e_2, \dots]$, graded in a way so that $\deg(e_n) = n$, and then show that this is (isomorphic to?) the ring of symmetric functions I want (I don't know how exactly, maybe as limit or colimit of the appropriate graded rings... but that's a problem for later).

[Alessandro Iraci]

In the message above, $e_n$ is the elementary symmetric function of degree $n$. It is already implemented in https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/MvPolynomial/Symmetric.html#Multiset.esymm for a finite number of variables, but I think it's easier to realise the symmetric function algebra (in infinitely many variables) as free algebra on the $e_n$ elements rather than as a formal power series ring.

[Junyan Xu]

The (commutative) free algebra is just docs#MvPolynomial, and we have docs#MvPolynomial.IsWeightedHomogeneous.WeightedHomogeneousSubmodule.gcomm_monoid so you can use stuff in that file to put a graded algebra structure on MvPolynomial ℕ R such that the nth variable has degree n. I'm also convinced that this is isomorphic to the ring of symmetric functions, and I'm curious why it's not explicitly mentioned on Wikipedia or the two SE questions. Maybe it's more important to show it's the limit / colimit, or that it admits an explicit realization as a graded subalgebra of docs#MvPowerSeries.

I think as a first step we should define the graded AlgHoms between rings of symmetric polynomials in both directions, which may depend on #6593. It seems mathlib doesn't currently have a bundled graded AlgHom type, and we should probably define it, otherwise it's hard to talk about (co)limits in the category of graded algebras. Also, given so many definitions, we should probably think about applications and decide which one to emphasize.

[Antoine Chambert-Loir]

It's not mentioned in Wikipedia because Wikipedia is not optimal at the level you're interested in.

It's present (slightly implicitly) in Lang's Algebra (pages 195ff), in Macdonald's Symmetric functions and Hall polynomials (page 22, at the infinite level where the situation is even clearer), and in many other good sources.

[Antoine Chambert-Loir]

Mathlib knows about the graded ring structure on a ring of polynomials with respect to any weight function on the indeterminates (@María Inés de Frutos Fernández and I did PR that for our work on divided powers), see docs#MvPolynomial.weightedHomogeneousComponent for example.

[Kevin Buzzard]

Just another example of the power of doing things "the right way" the first time -- other people can reuse your ideas.

[Alessandro Iraci]

Thanks for the insight, that's useful! I agree we should think about applications first, but there are just so many, it's a bit overwhelming. In my field, the most relevant one is probably plethysm; for that we might want to have Lambda Rings first, but there are other equivalent definitions.

My gut feeling is that "free graded algebra on $e_n$" is the way to go, as it is very flexible, but then there is a bit of work to do to define all the relevant base changes, which will probably come from the colimit structure. What we definitely do NOT want is "formal power series in countably many variables that are symmetric", which is very hard to work with.

[Alessandro Iraci]

#6593 seems very relevant, I agree that we need it.

[Junyan Xu]

I agree that defining lambda rings and provide some examples would be a good first project to test the API on symmetric functions to be built. Symmetric functions and big Witt vectors are probably the two most prominent examples. I came across this MO answer that explains the connection between big Witt vectors and the Hopf algebra of symmetric functions. Note that docs#WittVector is the p-typical Witt vectors, not the big ones (I think they're the projection of the big Witt vectors to the p^n-th components; Commelin--Lewis lists big Witt vectors as a future project).

I looked into the definition of lambda rings and though some axioms are identical to those of divided power structures, the others depend on certain polynomials to be defined, for example the $P_n$ in the picture below (from this blog post). It seems this identity as a whole only makes sense in the power series ring with infinitely many variables, though if you want to compute the coefficient of $T^n$ it suffices to truncate the product to $1 \le i \le n, 1 \le j \le n$. So it seems to me the power series representation of symmetric functions seems to be the most natural in this situation, and useful for proving things.

image.png

[Johan Commelin]

I will also quote

-- Mathlib/RingTheory/Polynomial/Dickson.lean :: L116-126

/-!

### A Lambda structure on `ℤ[X]`

Mathlib doesn't currently know what a Lambda ring is.
But once it does, we can endow `ℤ[X]` with a Lambda structure
in terms of the `dickson 1 1` polynomials defined below.
There is exactly one other Lambda structure on `ℤ[X]` in terms of binomial polynomials.

-/

[Kevin Buzzard]

And I'll mention that #10079 (which I'm currently working on) will bring us Hopf algebras.

[Alessandro Iraci]

It could be useful to have the power series representation for Sym (the algebra of symmetric functions - it's about time to give it a name), but I still think it's very inconvenient to use it as a definition. In my experience, when working with symmetric functions, what you really need to know is how to change basis, which will follow from the finite case; the symmetric variables are almost always left implicit.

For most use cases it's going to be enough to look at the "finitely many variables" case, which we still need to do if we want all the limit/colimit structure (and we definitely do). It's probably worth it to show that Sym is isomorphic to the symmetric power series of bounded degree in the X variables, but I'm reasonably confident that it's better to have it as a theorem rather than using it as an actual definition.

Moreover, already in your picture we see instances of identities among symmetric functions that involve different sets of variables. If we leave the variables implicit, everything can be easily expressed as a tensor product, and specialized later if needed.

Finally, the expression $\prod (1 + X_i Y_j T)$ is pretty much ubiquitous (it's the antipode of the Cauchy kernel), and you can easily express it without the variables. This might not be precise, but up to some small tweak, I believe that if you replace the elementary symmetric functions on the LHS with the complete homogeneous symmetric functions (say, using $h_i \otimes 1$ instead of $E_i$, and $1 \otimes h_i$ for $F_i$), you get $\sum_{\lambda \vdash n} T^n s_\lambda \otimes s_\lambda$, where the sum is over all partitions and $s_\lambda$ denotes the Schur function.

Overall, I'm strongly against using the power series representation in the definition of Sym, but I'm open to other opinions if some strong argument for it appears.

[Alessandro Iraci]

I'm really happy that this thread is getting active, there have been a lot of cool ideas and I can see this be a thing in some time! :)

[Riccardo Brasca]

Maybe you can choose a mathematically very easy lemma, and try to prove it using the formulation you prefer, just to check if it is a reasonable choice. Sometimes what is convenient (or inconvenient) in real world math and Lean are different things.

[Alessandro Iraci]

The problem is, I have to implement a whole bunch of structure before I can actually prove anything. At the very least, the limit/colimit structure, as a standard way to prove things is by "lifting" statements that hold in finitely many variables.

Anyway, I'm suggesting the "free polynomial algebra over $e_n$" implementation exactly because normally computers are good with symbolic manipulation.

[Riccardo Brasca]

I mean something completely ridiculously trivial for a mathematician. Like what happens with zero variables.

[Riccardo Brasca]

Or one variable. Using multivariate polynomials in one variable (that is not the same as polynomials in one variable) is a not so pleasant experience

[Riccardo Brasca]

What I mean is that we can keep on discussing forever. If you want to start a project sooner or later you have to make a decision

[Riccardo Brasca]

Even if it turns out it's not the best choice we've learned something anyway (for example in the LTE we proved the snake lemma in like 3 different formulations, all mathematically completely identical, and the version that ended in mathlib is completely different)

[Kevin Buzzard]

Schemes and group cohomology were also like that -- I think the mathlib version is v3 in both cases. But as we go on with this project of formalising mathematics, the community is getting better at getting the answer right earlier. That's why it's worth coming up with a sample problem or two, so the community can start experimenting with actual code.

[Junyan Xu]

A smaller first project would be defining the $\rho_n$ (maybe call it ofSucc) and $\phi_n$ (toSucc) in the Wikipedia page (see screenshot below), and also the maps from the symmetric functions to the symmetric polynomials and vice versa, and show the triangles are commutative; once we define graded homs, we can go on to show these form limit and colimit diagrams. A question is whether to take the MvPolynomial rings (in finitely many variables) or the subring of symmetric polynomials as the domain and codomain of these maps; we know they're isomorphic by #6593. Maybe use the former to define $\phi_n$ and the latter to define $\rho_n$ so the definitions don't depend on #6593? But we need to use the same thing in order to state $\rho_n \circ \phi_n = \text{id}$, which is probably necessary to show the inverse diagram is a limit. (It should be pretty trivial to show the directed diagram is a colimit in this formulation, assuming that we define the symmetric functions as Alessandro suggests.)

image.png

[Alessandro Iraci]

I was thinking the same! It's definitely needed and probably a useful exercise. Let's start with that.

[Junyan Xu]

I think it's not substantially harder to define maps between any two algebras of symmetric polynomials (not just consecutive ones), so you actually get a docs#DirectedSystem (there's no InverseSystem in mathlib as of yet though, but you can use docs#CategoryTheory.Limits.IsLimit). The docs#PerfectClosure API is built using only the consecutive maps, but we need not mimic that ...

[Antoine Chambert-Loir]

I believe the first thing to prove is that symmetric polynomials in $n$ variables are freely generated by the elementary symmetric polynomials (with coefficients in any commutative ring), and weights correspond with degrees.

[Kevin Buzzard]

Have we _really_ still not got this? I have set about three student projects on this topic and it's also on the undergraduate problem list...(but we might well not have it...)

[Ruben Van de Velde]

Is that the fundamental theorem that's been sitting in a PR for months?

[Ruben Van de Velde]

#6593

[Antoine Chambert-Loir]

Does it make sense to ask for the proof that this isomorphism respect degrees (with appropriate weights)?

[Junyan Xu]

Ruben Van de Velde said:

Is that the fundamental theorem that's been sitting in a PR for months?

Yeah sorry I've been unmotivated to do the chore that we decided should be done in the prerequisite PR #7173 for months, but there's definitely some fresh motivation from this thread :)

[Junyan Xu]

Does it make sense to ask for the proof that this isomorphism respect degrees (with appropriate weights)?

Browsing through the graded API, I could phrase this result at two levels:

1. If a MvPolynomial (Fin n) R IsWeightedHomogeneous of degree k, then its evaluation at the elementary symmetric polynomials (i.e. its image under the isomorphism) IsHomogeneous of degree k.
2. The isomorphism sends docs#MvPolynomial.weightedHomogeneousSubmodule of degree k into docs#MvPolynomial.homogeneousSubmodule of degree k. (This can be taken to the definition of graded homs, but in this case we need to take comap Subalgebra.val of the homogeneousSubmodule to get submodules of the symmetricSubalgebra.

which should not be hard to prove. It appears that we don't have docs#GradedRing structures on MvPolynomial yet (either weighted or unweighted), and there are two unmerged mathlib3 PRs mathlib#8913 and mathlib#10119 doing the unweighted. I think we do need the missing piece DirectSum.Decomposition (i.e. the map from the direct sum of graded pieces to the whole algebra is bijective, with an explicit inverse decompose) to show that if a graded hom is an Equiv, then its inverse is also a graded hom.

[Johan Commelin]

We do have a GradedMonoid instance: https://github.com/leanprover-community/mathlib4/blob/8d817bbea3313e497d6f65f9757dc1b40bc9fc53/Mathlib/RingTheory/MvPolynomial/Homogeneous.lean#L381-L383

[Johan Commelin]

And the two examples below it hint at some graded ring structure being inferred

[Alessandro Iraci]

It seems there is some backlog on pull requests that might really help with all this stuff. Is there anything useful I can do in the meantime? Say, define complete homogeneous, monomial, and power sum symmetric functions in the finite case?

Do we have integer partitions/compositions in Lean? How about Young tableaux?

[Johan Commelin]

Yes, Young tableaux are there

[Johan Commelin]

See the directory Mathlib/Combinatorics/Young

[Junyan Xu]

docs#MvPolynomial.psum is the power sum symmetric polynomials, and we have Newton‘s identities (Zulip). I don't think we have complete homogeneous and monomial symmetric polynomials in mathlib.

And the two examples below it hint at some graded ring structure being inferred

The two examples show there is a ring structure on the direct sum, but it's not yet known to mathlib that MvPolynomial is isomorphic to the direct sum, for which you need to show the graded pieces are "linearly independent" and span the whole space, or better, give an explicit inverse to the map from the direct sum to the whole space. docs#GradedRing is the composite of two typeclasses GradedMonoid and DirectSum.Decomposition, and the latter exactly consists of the data of such an inverse. GradedRing instances were constructed in the two PRs I mentioned.

It seems there is some backlog on pull requests that might really help with all this stuff.

Before I get back to the PRs, you could create a branch out of my branch#FundThm_SymPoly, add some new files, and start working on what you want; the fact the PR isn't in mathlib yet shouldn't block you from building on top of it. You could also make your repo/project depend on a specific branch/commit of mathlib, but I don't see the necessity of a separate repo at this stage.

[Alessandro Iraci]

I implemented the complete homogeneous symmetric functions, proved that they are symmetric, and a few lemmas about them. Should I submit a pull request (and wait for it to be rejected, since the code is horrible)?

[Kevin Buzzard]

Maybe it's better to post it here first and get feedback? You could try...

[Riccardo Brasca]

I think you can go with the PR. Maybe mark it "RFC" (request for comment), to make clear you want an initial feedback.

[Alessandro Iraci]

Done, it's #10983. Looking forward to hear feedback!

[Riccardo Brasca]

I've left a couple of comments but I didn't look at the proofs, I will do it tomorrow.

[Alessandro Iraci]

Second attempt! #11026

Can I close the old PR and delete the fork? I think having a fork is messing up with my Git somehow.

[Ruben Van de Velde]

Yes, you can

[Riccardo Brasca]

I'll have a look at #11026 later toaday, can you fix the build error?

[Riccardo Brasca]

I never remember if the error is public or not, anyway it is

Warning: ./././Mathlib/RingTheory/MvPolynomial/Symmetric.lean:8:1: warning: unused import (use `lake exe shake --fix` to fix this, or `lake exe shake --update` to ignore)
./././Mathlib/RingTheory/MvPolynomial/Symmetric.lean:
  remove #[Mathlib.Data.Set.Card]

[Alessandro Iraci]

I think I already fixed that, maybe it's not pushed yet?

[Riccardo Brasca]

I don't see any commit touching the import lines.

[Timothy Harevy]

Can someone point me in the right direction here not to sure where to start tried using rcases on h but didn't work.

example (h: ∀(n : ℕ), ∃x,  a - 1 / (n + 1) < x): ∃(y_n : ℕ → ℝ), ∀ (n : ℕ), a - 1 / (n + 1) < y_n n :=by{

}

[Ruben Van de Velde]

choose f hf using h, but you're in the wrong stream and your use of subtraction and division on natural numbers is making your life hard

[Timothy Harevy]

ahh thank you much appeciated

[Alessandro Iraci]

I just found out about this and now I'm jealous. https://github.com/math-comp/Coq-Combi