Coxeter Groups in Lean

We formalize in Lean some results on Coxeter groups, following the textbooks [1] and [2]. The results are organized as follows:

• Basic.lean
  • Basic definitions and lemmas
  • The opposite of a Coxeter group
• PermutationRepresentation.lean
  • Construction of the permutation repersentation
• StrongExchange.lean
  • Strong exchange
  • Deletion property
• Bruhat.lean
  • Definition of the Bruhat order
  • Subword property
  • Lifting property
  • The longest element of a finite Coxeter group
• GeometricRepresentation.lean
  • Construction of the geometric repersentation
  • Order of $s_i s_{i'}$
  • Injectivity of cs.simple

References

[1]: A. Björner and F. Brenti, Combinatorics of Coxeter Groups. Springer, 2005. DOI: 10.1007/3-540-27596-7

[2]: N. Bourbaki, Groupes et algèbres de Lie. Springer, 2007. DOI: 10.1007/978-3-540-34491-9