Equiv.Perm (Fin (n + 1)) is a Coxeter group

Stream: maths

[Robin Carlier]

For a project, I need to use that the symmetric group admits a presentation by generators and relations of the form : $\mathfrak{S}_{n + 1} \cong \left\langle (s_{i})_{0 \le i < n}\quad | \begin{cases}s_i^2 &=& e \\ s_is_{i+1}s_i &=& s_{i+1}s_is_{i+1} \\ s_is_j &=& s_js_i\ \mathrm{if}\ |i - j| > 1\end{cases} \right\rangle$, the isomorphism is sending $s_i$ to the permutation $(i\ \ i+1)$ (and that fully characterizes it).

Of course, this presentation is the one that comes from the fact that $\mathfrak{S}_{n + 1}$ is a Coxeter group of type $\mathrm{A}_n$. So I set out to construct a term of type CoxeterSystem (CoxeterMatrix.Aₙ n) (Equiv.Perm (Fin (n + 1))).
I formalized the criterion from the book Combinatorics of Coxeter Groups by Björner and Brenti, which provides a concrete combinatorial recognition principle for when a group equipped with a set of order 2 generators defines a Coxeter system: the group needs to satisfy the "exchange property" (thm 1.5.2 in the book). Then, one has to check that the symmetric groups have this property, using properties of the inversion number of permutations.
I have made the formalization available in a branch of my fork.
The relevant files are here (for the criterion) and here (for the fact that this is satisfied by Equiv.Perm (Fin (n + 1))).

Mathlib has the definition of Coxeter matrices, and some work on Coxeter systems but does not have any non-trivial Coxeter system (i.e one that is not M.toCoxeterSystem where M is a Coxeter matrix), so I guess we also finally have an application of this theory.

I wanted to share the small milestone, but the code still needs some cleanup (there are non-terminal simp, bad names, etc.) before it can be split into smaller chunks that are upstreamable. I have good hopes that I’ll get to it soon though.