The standard geometric representation of a Coxeter system

Let cs : CoxeterSystem M W be a Coxeter system with Coxeter matrix M : CoxeterMatrix B. This file builds the representation of W that Jacques Tits used to analyse Coxeter groups: the free real vector space B →₀ ℝ on the index set, with the i-th basis vector read as the i-th simple root αᵢ, carries the symmetric bilinear form

B(αᵢ, αᵢ') = -cos (π / M i i'),

and W acts with the i-th simple reflection acting as the orthogonal reflection v ↦ v - 2 B(αᵢ, v) αᵢ in the hyperplane B(αᵢ, ·) = 0. Mathlib's convention that an entry M i i' = 0 stands for ∞ is exactly right here: π / 0 is 0 in Lean, so such a pair contributes -cos 0 = -1, the degenerate Gram matrix of a pair of parallel walls. The diagonal entries are -cos π = 1, so every simple root is a unit vector.

What this file is for

The Coxeter relations hold in this representation, which is what makes the action exist; but the point of building it is the converse divisibility that comes out of it. The defining relations of a Coxeter group give only orderOf (s i * s i') ∣ M i i' (CoxeterSystem.simple_mul_simple_pow), and a presentation can a priori collapse. Restricting the action to the plane spanned by two simple roots computes the order on the nose: that plane is Euclidean as soon as M i i' is finite and at least two, the two reflections compose to the rotation through 2 π / M i i', and a rotation through 2 π / m has order exactly m. When M i i' = 0 the plane is degenerate and the composite is a shear, of infinite order. So

orderOf (cs.simple i * cs.simple i') = M i i'

uniformly in i and i', with 0 read as ∞ (CoxeterSystem.orderOf_simple_mul_simple). A further collapse is ruled out at the same time: distinct indices give distinct simple reflections.

Exactness, not just divisibility, is what a braid move needs. The braid move at (i, i') rewrites the alternating word s i s i' s i ⋯ of length M i i' into the alternating word of the same length that starts with s i', and the induction step of Matsumoto's theorem needs those words to be reduced. Were orderOf (s i * s i') a proper divisor d of M i i', the alternating word of length 2 * d would already be trivial and the length-M i i' one would not be reduced.

The route

Everything rests on one two-dimensional computation. In the coordinates αᵢ, αᵢ' the composite σᵢ σᵢ' of the two simple reflections has matrix !![4 c ^ 2 - 1, -(2 c); 2 c, -1] with c = cos (π / M i i'), of determinant one and trace 2 cos (2 π / M i i'); an induction on the exponent, whose step is the pair of addition formulas for cos and sin, turns its k-th power into the rotation matrix through 2 k π / M i i' written in those coordinates. Two consequences are read off. At k = M i i' the angle is 2 π and both simple roots are fixed; since the Gram matrix of the two simple roots is invertible, the plane splits off its orthogonal complement -- on which the composite is the identity, both reflections fixing it -- so the braid relation holds on the whole space. And σᵢ σᵢ' can fix the first simple root only if the angle 2 k π / M i i' is a multiple of 2 π, which pins the order down.

The second simple root is handled without a second induction: σᵢ' σᵢ is the inverse of σᵢ σᵢ', and the two commute, so the first computation with the indices exchanged transfers.

Main results

• CoxeterMatrix.geometricForm: the canonical bilinear form of a Coxeter matrix, with CoxeterMatrix.geometricForm_single_single its Gram matrix and CoxeterMatrix.geometricForm_comm its symmetry.
• CoxeterMatrix.geometricReflection: the simple reflections, with CoxeterMatrix.geometricReflection_mul_self saying that they are involutions, CoxeterMatrix.geometricReflection_apply_single_self that the i-th one negates the i-th simple root, and CoxeterMatrix.geometricForm_geometricReflection that they are orthogonal for the canonical form.
• CoxeterMatrix.isLiftable_geometricReflection: the simple reflections satisfy the Coxeter relations, so they lift along CoxeterSystem.lift.
• CoxeterSystem.geometricRepresentation: the standard geometric representation, with CoxeterSystem.geometricRepresentation_simple its values on the simple reflections and CoxeterSystem.geometricForm_geometricRepresentation its orthogonality.
• CoxeterSystem.simple_mul_simple_pow_eq_one_iff and CoxeterSystem.orderOf_simple_mul_simple: the entry M i i' is the exact order of s i * s i', not merely a multiple of it.
• CoxeterSystem.simple_injective: distinct indices give distinct simple reflections.

What is not proved here

Tits' theorem proper -- that the geometric representation is faithful, so that a Coxeter group is a reflection group -- is a strictly stronger statement, proved by the "root bookkeeping" argument that tracks which simple roots a reduced word makes negative. It is proved in TauCeti/GroupTheory/Coxeter/Geometric/Sign.lean, and none of the results above needs it: the exact order of a product of two simple reflections only needs the representation to be nontrivial on a single rank-two plane.

References

• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Springer (2002), Ch. V, Section 4.3.
• J. E. Humphreys, Reflection Groups and Coxeter Groups, CUP (1990), Section 5.3.

The canonical bilinear form

noncomputable def CoxeterMatrix.geometricForm {B : Type u_1} (M : CoxeterMatrix B) : LinearMap.BilinForm ℝ (B →₀ ℝ)

The canonical bilinear form of a Coxeter matrix on the free real vector space on the index set: the symmetric form whose Gram matrix in the basis of simple roots has entries -cos (π / M i i'). The diagonal entries are -cos π = 1, and a pair of indices with no relation between them (M i i' = 0, read as ∞) contributes -cos 0 = -1.

@[simp]

theorem CoxeterMatrix.geometricForm_single_single {B : Type u_1} (M : CoxeterMatrix B) (i i' : B) (a b : ℝ) : (M.geometricForm (Finsupp.single i a)) (Finsupp.single i' b) = a * b * -Real.cos (Real.pi / ↑(M.M i i'))

The Gram matrix of the canonical form in the basis of simple roots.

theorem CoxeterMatrix.geometricForm_single_self {B : Type u_1} (M : CoxeterMatrix B) (i : B) : (M.geometricForm (Finsupp.single i 1)) (Finsupp.single i 1) = 1

The diagonal entries of the canonical form are 1, the Coxeter matrix having 1 on its diagonal and -cos π being 1.

theorem CoxeterMatrix.geometricForm_comm {B : Type u_1} (M : CoxeterMatrix B) (u v : B →₀ ℝ) : (M.geometricForm u) v = (M.geometricForm v) u

The canonical form is symmetric, the Coxeter matrix being symmetric.

The simple reflections

noncomputable def CoxeterMatrix.geometricReflection {B : Type u_1} (M : CoxeterMatrix B) (i : B) : Module.End ℝ (B →₀ ℝ)

The simple reflection of the geometric representation attached to an index i: the reflection v ↦ v - 2 B(αᵢ, v) αᵢ of the free real vector space on the index set in the hyperplane orthogonal to the i-th simple root αᵢ, for the canonical form B.

@[simp]

theorem CoxeterMatrix.geometricReflection_apply {B : Type u_1} (M : CoxeterMatrix B) (i : B) (v : B →₀ ℝ) : (M.geometricReflection i) v = v - (2 * (M.geometricForm (Finsupp.single i 1)) v) • Finsupp.single i 1

The reflection formula v ↦ v - 2 B(αᵢ, v) αᵢ.

theorem CoxeterMatrix.geometricReflection_apply_single_self {B : Type u_1} (M : CoxeterMatrix B) (i : B) : (M.geometricReflection i) (Finsupp.single i 1) = -Finsupp.single i 1

The i-th simple reflection negates the i-th simple root.

theorem CoxeterMatrix.geometricReflection_apply_pair {B : Type u_1} (M : CoxeterMatrix B) (i j : B) (a b : ℝ) : (M.geometricReflection i) (a • Finsupp.single i 1 + b • Finsupp.single j 1) = (2 * Real.cos (Real.pi / ↑(M.M i j)) * b - a) • Finsupp.single i 1 + b • Finsupp.single j 1

A simple reflection on the plane of two simple roots, in their specified order.

theorem CoxeterMatrix.geometricReflection_apply_apply_of_ne {B : Type u_1} (M : CoxeterMatrix B) {i j : B} (h : j ≠ i) (v : B →₀ ℝ) : ((M.geometricReflection i) v) j = v j

A simple reflection changes only the coefficient of its own simple root.

theorem CoxeterMatrix.geometricReflection_apply_of_eq_zero {B : Type u_1} (M : CoxeterMatrix B) {i : B} {v : B →₀ ℝ} (h : (M.geometricForm (Finsupp.single i 1)) v = 0) : (M.geometricReflection i) v = v

A vector orthogonal to the i-th simple root is fixed by the i-th simple reflection.

theorem CoxeterMatrix.geometricReflection_mul_self {B : Type u_1} (M : CoxeterMatrix B) (i : B) : M.geometricReflection i * M.geometricReflection i = 1

The simple reflections are involutions.

theorem CoxeterMatrix.geometricForm_geometricReflection {B : Type u_1} (M : CoxeterMatrix B) (i : B) (u v : B →₀ ℝ) : (M.geometricForm ((M.geometricReflection i) u)) ((M.geometricReflection i) v) = (M.geometricForm u) v

The simple reflections preserve the canonical form, so the geometric representation is orthogonal for it.

The rank-two computation

theorem CoxeterMatrix.isLiftable_geometricReflection {B : Type u_1} (M : CoxeterMatrix B) : M.IsLiftable M.geometricReflection

The simple reflections of the geometric representation satisfy the Coxeter relations.

noncomputable def CoxeterSystem.geometricRepresentation {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) : Representation ℝ W (B →₀ ℝ)

The standard geometric representation of a Coxeter system: the representation of W on the free real vector space on the index set in which the i-th simple reflection acts as the reflection v ↦ v - 2 B(αᵢ, v) αᵢ in the hyperplane orthogonal to the i-th simple root, for the canonical bilinear form B = CoxeterMatrix.geometricForm M.

The Coxeter relations hold, but for three different reasons. At i = i' the entry is 1 and the relation says that a reflection is an involution. For i ≠ i' with M i i' nonzero, hence at least two (an off-diagonal entry is never 1), the plane spanned by the two simple roots is Euclidean and the two reflections compose to the rotation through 2 π / M i i', whose M i i'-th power is the identity. For i ≠ i' with M i i' = 0, read as ∞, that plane is instead degenerate and the composite is a shear, of infinite order; there the relation to be checked is the vacuous (σᵢ σᵢ')^0 = 1.

@[simp]

theorem CoxeterSystem.geometricRepresentation_simple {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i : B) : cs.geometricRepresentation (cs.simple i) = M.geometricReflection i

Each simple reflection of a Coxeter system acts by its geometric reflection, the reflection in the hyperplane orthogonal to the corresponding simple root.

theorem CoxeterSystem.geometricRepresentation_mul_simple_single {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (w : W) (i : B) : (cs.geometricRepresentation (w * cs.simple i)) (Finsupp.single i 1) = -(cs.geometricRepresentation w) (Finsupp.single i 1)

The image of αᵢ under w * s i is the negative of its image under w.

theorem CoxeterSystem.geometricForm_geometricRepresentation {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (w : W) (u v : B →₀ ℝ) : (M.geometricForm ((cs.geometricRepresentation w) u)) ((cs.geometricRepresentation w) v) = (M.geometricForm u) v

The geometric representation is orthogonal for the canonical bilinear form.

theorem CoxeterSystem.simple_mul_simple_pow_eq_one_iff {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i i' : B) (n : ℕ) : (cs.simple i * cs.simple i') ^ n = 1 ↔ M.M i i' ∣ n

The exact relation satisfied by two simple reflections: the product of two simple reflections is killed by an exponent exactly when that exponent is a multiple of the corresponding entry of the Coxeter matrix. One half of this is the defining relation CoxeterSystem.simple_mul_simple_pow; the other half comes from the geometric representation, in which the product acts on the plane of the two simple roots with exactly this order.

theorem CoxeterSystem.orderOf_simple_mul_simple {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i i' : B) : orderOf (cs.simple i * cs.simple i') = M.M i i'

The entries of the Coxeter matrix are the exact orders of the products of pairs of simple reflections. The defining relations give only the divisibility orderOf (s i * s i') ∣ M i i'; the reverse divisibility comes from the geometric representation. An entry M i i' = 0, read as ∞, says that the product has infinite order.

theorem CoxeterSystem.simple_injective {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) : Function.Injective cs.simple

The simple reflections are pairwise distinct.