Progress on Coxeter groups

Stream: mathlib4

[Mitchell Lee]

In case anyone is interested, here is my progress on the properties of Coxeter groups.

https://github.com/trivial1711/mathlib4/blob/trivial1711-reduced-words-in-coxeter-groups/Mathlib/GroupTheory/SpecificGroups/Coxeter.lean

I have proved the basic properties of the length function (defined on any CoxeterSystem). I also have an outline for the basic properties of the standard geometric representation and the associated roots and an outline for the (strong) left and right exchange properties and the deletion property.

There are a few important goals that will be in reach once these proofs are completed: Matsumoto's theorem, the classification of finite irreducible Coxeter groups (which may be a little easier once the representation theory of finite groups is more developed), and the combinatorial descriptions of Coxeter groups of type A, B, and D.

The code is reasonably well-documented, though some of the docstrings are currently broken. I plan to move a lot of this material into separate files soon.

• Does anyone have any feedback on my code? I am still relatively new to Lean, so it is possible that I have done some things wrong.
• Does this seem like something that could potentially make it into Mathlib?
• Is anyone interested in helping to fill in some of the proofs?

[Johan Commelin]

Does this seem like something that could potentially make it into Mathlib?

Yes, certainly! Start with PRs of small chunks!

[Mitchell Lee]

Hello, I've just started a pull request. https://github.com/leanprover-community/mathlib4/pull/11387

For now, it doesn't contain anything about the standard geometric representation. It just contains the basic properties of length, inversions, reflections, and inversion sequences.

Thanks for the help.

[Joël Riou]

At first glance, this looks great! I would suggest splitting this in a few dependent PRs:
1) the mostly straightforward refactor part (addition of the isCoxeter field to CoxeterSystem) -- actually I favored more the design with IsCoxeter as a typeclass, I think it was originally a mistake to change it to a structure only.
2) the very basic API about words in Coxeter systems (1 + 2 could be a single PR).
3) the more advanced results on words and the length (this could be further split in at least 2 PRs).

[Mitchell Lee]

Thank you for the feedback. Should I change IsCoxeter to a typeclass (maybe renaming it to CoxeterMatrix) then?

[Joël Riou]

The name IsCoxeter is fine.

[Mitchell Lee]

I've split it into two pull requests:
https://github.com/leanprover-community/mathlib4/pull/11406
https://github.com/leanprover-community/mathlib4/pull/11408

[Mitchell Lee]

I'll work on rewriting the proofs to satisfy the linter (and make them more readable) now

[Huanchen Bao]

We actually have a group working on Coxeter groups here.

https://gitee.com/hoxide/coxeter4/tree/master/Coxeter

We are almost done with the strong exchange properties and basic definitions of Hecke algebras. We are currently setting up the Blueprint as well. The short term goals aim for the El-shellability of Bruhat intervals, defining R polynomials and Kazhdan-Lusztig polynomials.

We do not work on the classification though.

[Mitchell Lee]

Thank you for telling me about this. I think I am going to continue trying to build on the Coxeter groups in Mathlib, working toward the goals I outlined at the beginning of this topic. I am currently working on proving that the standard geometric representation is well-defined. However, please tell me if this would make things more difficult for you or unnecessarily duplicate work.

[Mitchell Lee]

Hello, I would like to give an update on my current progress on this. I currently have six pull requests in the queue.

1. #11493: Prove that the generators of any presented group generate the presented group. (That is, the Subgroup.closure of the set of generators is equal to ⊤.) This is a small pull request and not specific to Coxeter groups.
2. #11436: Prove some general theorems about Antiperiodic functions; you can shift by an integer multiple n of the period by multiplying by n.negOnePow. Also specialize them to Real.sin and Real.cos. This isn't specific to Coxeter groups either, but it is a little more involved.
3. #11406: The basic theory of Coxeter groups, built on Newell Jensen's earlier work. Define simple reflections and words. Add some API for lifting homomorphisms. Also, improve the documentation. Depends on #11493.
4. #11465: Define the length function $\ell \colon W \to \mathbb{N}$. Use the length function to define reduced words and descents. Prove their basic properties. Depends on #11406.
5. #11466: Define reflections, inversions, and the inversion sequence of a word. Depends on #11465.
6. #11526: Define the standard geometric representation $\rho$ and the simple roots $\alpha_i$. Prove that $\rho$ is faithful and that it preserves the standard bilinear form. Depends on #11465, #11436 (but not #11466).

I know this is a very large amount to review, so I understand if it takes a while. I'm happy to discuss any of it whenever.

Also, I want to apologize for revising some of these pull requests so much after already having requested reviews for them. I'm going to step back for now so that the reviewers can take a look and not worry about anything changing.

[Mitchell Lee]

Thanks @Oliver Nash for reviewing #11493!

[Mitchell Lee]

Hi, thanks so much to Yaël Dillies for helping me with #11406. I've decided to split it into two PRs. The first is #11836, which refactors the existing Coxeter groups file. The second is #11406, which adds some basic theorems about simple reflections, lifting homomorphisms, and words.

I think @Newell Jensen, the author of the existing Coxeter groups file, may be interested in looking at #11836 in particular.

[Newell Jensen]

Hey Mitchell. I have been too tied up with other work lately to be of much help (no Lean for me for the past 1.5 months unfortunately :cry: ). I just left a quick review for #11836 (in which the below is repeated some).

I took a quick glance and I like the idea of breaking out the matrix parts to its own separate file. One thing I did notice though is that even though M.coxeterMatrix might adhere to naming conventions, I would think (I haven't checked with other parts of mathlib and I don't remember off the top of my head) that since Coxeter is a name of someone we sould keep it capitalized. If this is not done in mathlib I would argue that it should be that way! Coxeter and the other greats deserve this respect IMHO! :)

Thanks for giving Coxeter Groups some love and maybe sometime in the future I will have more time to work on it some more myself. Thanks!

[Mitchell Lee]

Thank you for the review!

[Yaël Dillies]

Newell Jensen said:

even though M.coxeterMatrix might adhere to naming conventions, I would think (I haven't checked with other parts of mathlib and I don't remember off the top of my head) that since Coxeter is a name of someone we sould keep it capitalized.

docs#gaussSum would like to disagree

[Yaël Dillies]

I think that so many mathematical objects are named after people that it would render the new naming convention mostly useless if we tried to capitalise them

[Mitchell Lee]

Hello, I just realized that all the naming can be a whole lot cleaner if we get rid of IsCoxeter and just create a subtype CoxeterMatrix B of Matrix B B \N with its own API

[Mitchell Lee]

This avoids cluttering the Matrix namespace with Coxeter stuff and it reduces the number of variables that need to be carried around everywhere

[Mitchell Lee]

This also gets around the current issue that Matrix.coxeterGroup can fail to be a Coxeter group; I will replace it with CoxeterMatrix.coxeterGroup

[Mitchell Lee]

Actually, can I just call it CoxeterMatrix.group?

[Mitchell Lee]

Okay, I've done it: #11836. I am reasonably happy with how everything is named now.

[Junyan Xu]

Apparently there is a separate project (and a presentation here as well). (found through this thread on Dr. Ma Jiajun's homepage.

[Mitchell Lee]

I have talked to the organizers of that project and I am about to fly to Singapore, where we will discuss how to best combine our two approaches.

[Kevin Buzzard]

Will you be around on Monday? I'm giving a talk in Singapore!

[Mitchell Lee]

Yeah, I'm going to the workshop

[Mitchell Lee]

I'm looking forward to meeting you!

[Mitchell Lee]

Hello everyone! I am currently at the Workshop on Formal Proofs and Lean at the National University of Singapore.

In case anyone is curious, here is a summary of the current situation regarding the formalization of the theory of Coxeter groups.

Currently, there are two separate projects.

• Project A: The project initiated by @Newell Jensen and continued by me. This is aimed at building the basic theory of Coxeter groups. It contains some foundational results about the length function, reduced words, descents, inversions, and the standard geometric representation. Some of this project is already on the master branch of mathlib (see here). The rest is contained within the mathlib pull requests #11406, #11465, #11466, and #11526. Branch mathlib4/trivial1711-coxeter-groups-all contains the contents of all of these pull requests. This project was set up with a view toward Matsumoto's theorem and the classification of finite irreducible Coxeter groups, but it is not actively being worked on.
• Project B: The Xiamen University/National University of Singapore/Renmin University project. This is currently separate from mathlib and can be found here. The team consists primarily of undergraduates and the project is overseen by Professor @Huanchen Bao at NUS. The primary current goal is to define the Bruhat order on a Coxeter group and to establish the basic properties of Bruhat intervals. There are some other stretch goals, such as the theory of Hecke algebras.

We are currently working on making these two projects compatible, and we have decided to do so by refactoring project B to build upon the definitions and theorems from project A. This is a sizable amount of work, but we agreed that project B was in need of a refactor anyway, in part to align it more closely to the conventions of mathlib. The team has been handling this new work very well and making an impressive amount of progress. (Fortunately, much of project B is completely independent from project A, and that part doesn't need to be changed at all.)

Pull requests #11406, #11465, #11466, and #11526 are still open. Now, the contents of these pull requests are actively being used, so any feedback on how to make the API friendlier is highly appreciated.

P.S. Thanks so much, Professor Bao, for inviting me to this workshop. I've been having a great time.

[Johan Commelin]

Did someone already prove that $S_n$ (aka docs#Equiv.Perm) is a Coxeter group?

[Junyan Xu]

I just showed it has the proper generators here :)

[Johan Commelin]

Nice!

[Mitchell Lee]

I haven't formalized the proof that $S_n$ is a Coxeter group, and I think the NUS group has not either. I believe the easiest way to do so is by proving the following lemma (or something similar), which can be used to combinatorially describe every finite irreducible Coxeter group.

Lemma.

Let $W$ be a group, let $V$ be a real inner product space, and let $\rho \colon W \to GL(V)$ be a representation. Suppose that there exists a set $B$, a function $s_{\bullet} \colon B \to W$, and a function $\alpha_{\bullet} \colon B \to V$ such that:

• For all $i \in B$, we have that $\rho(s_i)$ is the orthogonal reflection in the vector $\alpha_i$.
• The $\alpha_i$ are linearly independent.
• The $s_i$ generate $W$.
• For all $i, i' \in B$, there exists $m = m_{i, i'} \in \mathbb{N} \cup \{\infty\}$ such that the inner product $\langle \alpha_i, \alpha_{i'} \rangle$ evaluates to $-2\cos(\pi / m)$.

Then $W$ is a Coxeter group with simple reflections $s_i$ and Coxeter matrix $(m_{i, i'})_{i, i' \in B}$.

This lemma is an easy consequence of the fact that the standard geometric representation of a Coxeter group is faithful. One can show that $S_n$ is a Coxeter group by taking $W = S_n$, $V = \mathbb{R}^n$, $B = \{1, \ldots, n-1\}$, $s_i = (i, i+1)$, and $\alpha_i = e_{i + 1} - e_i$.

[Junyan Xu]

That sounds like the correct mathlib way of doing things, but what's a reference for the faithfulness? For this particular example ($S_n$) though, it's possible to use this argument by induction and counting cosets.

[Mitchell Lee]

It's proved faithful in #12880, but you might need to wait a bit for that.

[Mitchell Lee]

Hi, I decided that it was important to redo all the code about geometric representations in a way that works over any commutative ring, and which allows defining "a" geometric representation rather than merely "the" geometric representation. So that's what I'm working on right now. It's quite involved, but I just finished what I think is probably the hardest part: #13270.

My approach is certainly unorthodox, so I would be very happy with feedback; not only on the code, but also on whether what I'm trying to do is even worthwhile.

See also this older comment: https://github.com/leanprover-community/mathlib4/pull/11526#issuecomment-2123707628

[Mitchell Lee]

What's proved in #13270 is a formula for $(r_1 r_2)^m z$, where $r_1$ and $r_2$ are any reflections on a module $M$ and $z$ is an element of $M$.

This formula works over any ring, so it can be used (for example) to construct reflection representations of crystallographic Coxeter groups over $\mathbb{Z}$, which I am sure will eventually be of interest.

Unfortunately, it is rather messy. It involves the Cheybshev $S$-polynomials $S_n(x)$, which are related to the usual Cheybshev polynomials of the second kind by $S_n(2x) = U_n(x)$.

[Johan Commelin]

That's a massive effort! But it looks like you've already split it up into three PRs. I'll try to review them

[Mitchell Lee]

@Huanchen Bao Do you have any thoughts on this? I don't want to go forward with this if it would make it more difficult for the NUS group. I think this material is disjoint from what the NUS group is doing, but this does mean that the exchange properties are going to be proved by sorry in https://github.com/NUS-Math-Formalization/coxeter for a little while longer.

[Scott Carnahan]

I think your work is quite helpful for classifying finite type root systems over characteristic zero fields. I had been trying, without success, to find a non-messy but general description of powers of pairs of reflections.

[Huanchen Bao]

Thanks for the checking. I think the issue is minor. I currently have a student working the shelling of posets. But this is independent of your work here. We are going to resume the Coxeter group part most likely in the fall semester later. I can check with you on the status then.

[Yaël Dillies]

Probably stupid remark, but is this related to @Sophie Morel's shellability of ASC?

[Huanchen Bao]

Can you be more specific?

[Sophie Morel]

I only defined the Bruhat order on the symmetric group, in order to show shellability of its Coxeter complex.

[Huanchen Bao]

I see. We are trying to formalized the EL-shellability on Bruhat intervals. This has been the joint effort of many groups as mentioned in Mitchell's earlier message. On one side, one needs to show the EL-labelling implies the shelling. This part is purely about posets. Then one needs to show the Bruhat intervals admit EL-labellings. This is much harder. Which method you used to show shelling? Can you share the link to the lean code, or it is in mathlib?

[Sophie Morel]

It's not in mathlib, as I am quite slow about PRing. The whole project including applications to the Coxeter complex and stuff about the category of simplicial complexes (and also some useless files) is there:
https://github.com/smorel394/ASC
There is also a mathlib branch with the basics of abstract simplicial complexes there:
https://github.com/leanprover-community/mathlib4/tree/AbstractSimplicialComplex

[Mitchell Lee]

Hello, I am currently working on defining reflection representations of Coxeter groups. (https://github.com/leanprover-community/mathlib4/tree/trivial1711-generalized-cartan) I know I said I would do it half a year ago, but I hope that it is better late than never.

[Mitchell Lee]

It has gotten quite complicated, however. Let $M$ be a Coxeter matrix and let $W$ be the corresponding Coxeter group. Let $k$ be a matrix of real numbers (though this can be generalized to any ordered ring) with the same dimensions as $M$. Consider the following conditions that the matrix $k$ could satisfy.

1. For all $i$, we have $k_{i, i} = 2$.
2. For all $i, i'$ with $2 < M_{i, i'} < \infty$, the number $k_{i,i'}k_{i', i}$ is of the form $4 \cos^2(\pi \ell / M_{i, i'})$, where $\ell$ is an integer with $0 < \ell < M_{i, i'} / 2$.
3. For all $i, i'$ with $M_{i, i'} = 2$, we have $k_{i, i'} k_{i', i} = 0$.
4. (strengthening of 2 and 3) For all $i, i'$ with $M_{i, i'} < \infty$, we have $k_{i,i'}k_{i', i} = 4 \cos^2(\pi / M_{i, i'})$.
5. For all $i, i'$ with $M_{i, i'} = \infty$, we have $k_{i,i'}k_{i', i} \geq 4$.
6. (strengthening of 3) For all $i, i'$ with $M_{i, i'} = 2$, we have $k_{i, i'} = k_{i', i} = 0$.
7. For all $i \neq i'$, we have $k_{i, i'} \leq 0$.
8. The entries of $k$ are all integers.
9. The matrix $k$ is symmetrizable; that is, it can be written as $DS$, where $D$ is diagonal and $S$ is symmetric.
10. (strengthening of 9) The matrix $k$ can be written as $DS$ where $D$ is diagonal and $S$ is symmetric and positive definite.

[Mitchell Lee]

Then $k$ is a Cartan matrix if and only if it satisfies all 10 of these properties. (What I mean by this is that a matrix $k$ is a Cartan matrix if and only if there exists a Coxeter matrix $M$ for which all 10 properties hold, and if so, the Coxeter matrix $M$ is unique.) Any Cartan matrix can be used to construct a reflection representation of the Coxeter group $W$. It can be described as follows.

• The representation is on a real vector space $V$, called the root space.
• There are elements $\alpha_i \in V$, called the simple roots. The simple roots form a basis of $V$.
• There are elements $\alpha^\vee_i \in V^*$, called the simple coroots. They are given by $k_{i, i'} = \alpha^\vee_i(\alpha_{i'})$ for all $i, i'$.
• The simple reflection $s_i$ acts by a reflection: $s_i v = v - \alpha^\vee_i (v)\alpha_i$.

[Mitchell Lee]

This is all very well-known and standardized. However, here is something that, as far as I can tell, is not. We do not actually need the matrix $k$ to satisfy all 10 of the above properties in order to get a reflection representation of $W$ as above. Namely:

• Only properties 1, 2, and 3 are necessary in order for the matrix $k$ to actually yield a reflection representation of $W$.
• If $k$ satisfies properties 1, 2, 3, 4, 5, 6, and 7, then this reflection representation is a geometric representation. That is, every element $w \alpha_i \in V$ is either a nonpositive linear combination of the simple roots or a nonnegative linear combination of the simple roots, according to whether $s_i$ is a right descent of $w$ or not. (This implies that the representation is faithful.)
• If $k$ satisfies properties 1, 2, 3, and 8, then this reflection representation is crystallographic. That is, it fixes the root lattice $\bigoplus_i\mathbb{Z} \alpha_i$.
• If $k$ satisfies properties 1, 2, 3, and 9, then this reflection representation comes with its own bilinear form. This bilinear form, considered as a linear map $V \to V^*$, sends each root $\alpha_i$ to a positive multiple of the corresponding coroot $\alpha^\vee_i$.
• If $k$ satisfies properties 1, 2, 3, 9, and 10, then the aforementioned bilinear form is an inner product on $V$. (If $k$ satisfies properties 1, 2, 3, 4, 5, 6, 7, 9, and 10, then this implies that the group $W$ is finite.)

[Mitchell Lee]

The task I am currently working on is to introduce a Prop-valued structure for matrices satisfying properties 1, 2, 3, 4, 5, 6, and 7. I have found these conditions or equivalent ones in a few different references on Coxeter groups. (See Combinatorics of Coxeter Groups by Björner and Brenti, or page 9 here.) Actually, I want to make these conditions work for matrices $k$ with entries in any ordered ring, which means the conditions involving the cosine function instead become conditions about evaluating certain Chebyshev polynomials at $k_{i, i'} k_{i', i} - 2$. The benefit of this is that it will be possible to define representations of $W$ over $\mathbb{Z}$ and other rings, such as real cyclotomic fields, without defining them over $\mathbb{R}$ first. See here for current progress.

[Johan Commelin]

@Mitchell Lee This is great! Thanks for writing up this summary!
Would you mind reposting it on a github issue, so that it is more easily preserved? Zulip seems to ephemeral for content like this.

[Mitchell Lee]

I will, for sure.

[Johan Commelin]

You list 5 subsets of the properties 1-10 that seem of particular importance. Do you already have names for them?

[Mitchell Lee]

Originally, I wanted to call a matrix a "generalized Cartan matrix" if it satisfies 1, 2, 3, 4, 5, 6, and 7. In fact my current code still calls it that. But this terminology usually refers to something else (https://nreadin.math.ncsu.edu/papers/MSRI3b.pdf), so I am inclined to use a different name. I am still not sure what to use, though.

[Johan Commelin]

Maybe steal names from the representations? Just thinking out loud:

• Matrix.IsCartanReflective
• Matrix.IsCartanGeometric
• Matrix.IsCartanCrystallographic
• Matrix.IsCartanBilinear (??)
• Matrix.IsCartanPosDef (??)

[Johan Commelin]

I'm not very happy with the latter two suggestions

[Mitchell Lee]

That sounds reasonable. It does have the slight downside of making it sound like it's a stronger condition than being a Cartan matrix, when it's actually weaker. This is probably fine though.

For matrices that satisfy 1, 2, 3, and 9, one option is to use whatever we use for matrices that satisfy 1, 2, 3, but also have ∧ IsSymmetrizable at the end.

I don't think we need to have any name for the crystallographic condition, because I am trying to make all the conditions make sense over any ordered ring, so you could just take the ring to be $\mathbb{Z}$.

[Mitchell Lee]

So I think we can do Matrix.IsCartanReflective, Matrix.IsCartanGeometric, Matrix.IsSymmetrizable, and Matrix.IsPosDefSymmetrizable and combine these using ∧

[Mitchell Lee]

Here is the github issue: #19934

[Johan Commelin]

Yeah that set of names seems reasonable. And so a small subproject would be to define those properties and proving the implications between the various properties that you mentioned above.

[Mitchell Lee]

If someone knowledgeable about the topic could carefully check what I have written in #19934, I would very much appreciate it.

[Mitchell Lee]

Ok, it seems that you have given it a thumbs up, which I will interpret as you having checked it; thank you!

[Johan Commelin]

Hmm, it was more intended as "thank you, I'm cheering you on" :smiley:

[Johan Commelin]

But I think it all looks very reasonable.

[Mitchell Lee]

Well, I appreciate that too

[Johan Commelin]

But I admit that I've never thought in detail about how to split up these properties.

[Johan Commelin]

It's one of the things that I really like about mathlib: that we figure out those details.

[Scott Carnahan]

I haven't examined your conditions in detail, but it looks quite good at a glance. I would recommend against names like generalized_foo because, as you have amply demonstrated, there can be many possible generalizations. Also, such names are relatively uninformative and unmemorable.

I should mention that there is a type of Cartan matrix that does not immediately correspond to Coxeter matrices - they are used to generate Borcherds-Kac-Moody algebras, whose distinguishing property is that there may be "imaginary" simple roots that do not produce reflections. However, it's not too bad, since you get the type of Cartan matrix that produces a reflection group by deleting the rows and columns with nonpositive diagonal.

[Mitchell Lee]

I have made a correction to the github issue: #19934