The order of a product of two simple reflections #
The product of the reflections in two roots αᵢ, αⱼ changes every weight by an element of the
span of the two roots. Over a characteristic-zero ring, its order is read off the Cartan product
c = ⟨αᵢ, αⱼ^∨⟩⟨αⱼ, αᵢ^∨⟩: the values 1, 2, 3 give the orders 3, 4, 6. This file proves
the corresponding upper bounds over an arbitrary commutative ring and these exact orders under
characteristic zero. It then proves — for two simple roots of a base of a finite crystallographic
pairing over a characteristic-zero domain, where c = 0 is the remaining possibility and gives the
order 2 — that the entries of
TauCeti.coxeterMatrixOfBase really are the orders they are named for, so that the braid relations
of the Coxeter presentation of a Weyl group hold in the Weyl group.
The iterates of the product are supplied by Mathlib's
Module.reflection_mul_reflection_pow_apply and Module.reflection_mul_reflection_pow_apply_self,
which express (r₁r₂)ⁿ over an arbitrary commutative ring through the Chebyshev S-polynomials
(Polynomial.Chebyshev.S) evaluated at t = c - 2;
RootPairing.weylGroup.pow_ofIdx_mul_ofIdx_smul and
RootPairing.weylGroup.pow_ofIdx_mul_ofIdx_smul_root are those formulas for a product of
two reflections of a root pairing, read as elements of the Weyl group. Substituting c = 1, 2, 3,
that is t = -1, 0, 1, makes the two Chebyshev coefficients of the general formula vanish at the
exponents 3, 4, 6, which gives g³ = 1, g⁴ = 1, g⁶ = 1; the remaining value c = 0 is
the orthogonal case, already settled in TauCeti.LinearAlgebra.RootSystem.Coxeter.Matrix, where the
two reflections commute, and where the order is pinned to 2 only for two distinct simple roots of
a base.
That the order is no smaller is checked on the single vector αᵢ: its αᵢ^∨-coordinate along the
orbit of g is again a Chebyshev expression in c, and for the relevant powers that expression
avoids the value ⟨αᵢ, αᵢ^∨⟩ = 2.
The iterate formulas and upper bounds are stated over an arbitrary commutative ring. The exact-order
results add characteristic zero, but still concern an arbitrary pair of roots of an arbitrary root
pairing, the Cartan product entering only as a hypothesis on RootPairing.pairing; no finiteness,
crystallographic or reducedness assumption is used there. The last section specialises to a pair of
simple roots of a base, where TauCeti.cartanMatrix_mul_cartanMatrix_mem_of_ne confines the Cartan
product to {0, 1, 2, 3} and the case analysis closes.
Main results #
RootPairing.weylGroup.pow_ofIdx_mul_ofIdx_smulandRootPairing.weylGroup.pow_ofIdx_mul_ofIdx_smul_root: the iterates of a product of two reflections, acting on a weight and on the first of the two roots.RootPairing.weylGroup.pow_three_ofIdx_mul_ofIdx_eq_one,RootPairing.weylGroup.pow_four_ofIdx_mul_ofIdx_eq_one,RootPairing.weylGroup.pow_six_ofIdx_mul_ofIdx_eq_one: the braid relations at Cartan product1,2,3, andRootPairing.weylGroup.orderOf_ofIdx_mul_ofIdx_eq_three,RootPairing.weylGroup.orderOf_ofIdx_mul_ofIdx_eq_four,RootPairing.weylGroup.orderOf_ofIdx_mul_ofIdx_eq_six: the matching exact orders under characteristic zero.RootPairing.weylGroup.orderOf_ofIdx_mul_ofIdx_eq_coxeterMatrixOfBase: the entries of the Coxeter matrix of a base are the orders of the products of the corresponding simple reflections.RootPairing.weylGroup.pow_coxeterMatrixOfBase_ofIdx_mul_ofIdx_eq_one: the braid relations of that Coxeter matrix hold in the Weyl group.
References #
This file supplies “the order of a product of two simple reflections” in Layer 2 of
TauCetiRoadmap/RepresentationTheory/RootSystems/README.md, the input the roadmap earmarks for the
braid relations of weylCoxeterSystem. The rank-two computation is Bourbaki, Lie Groups and Lie
Algebras, Chapters 4--6, Ch. VI, §1.3, and Humphreys, Introduction to Lie Algebras and
Representation Theory, §9.
The rank-two computation #
The iterates of a product of two reflections. This is Mathlib's
Module.reflection_mul_reflection_pow_apply for the reflections in two roots αᵢ, αⱼ of a root
pairing, read in the Weyl group; its Chebyshev polynomials are evaluated at the Cartan product
shifted by 2, that is at t = ⟨αᵢ, αⱼ^∨⟩⟨αⱼ, αᵢ^∨⟩ - 2.
The iterates of a product of two reflections on the first of the two roots. This is
Mathlib's Module.reflection_mul_reflection_pow_apply_self read in the Weyl group; it is the case
x = αᵢ of RootPairing.weylGroup.pow_ofIdx_mul_ofIdx_smul, in a form where the two
coefficients are single Chebyshev values.
The braid relations #
The braid relation at Cartan product 1: the product of the two reflections has order
dividing 3, the A₂ configuration.
The braid relation at Cartan product 2: the product of the two reflections has order
dividing 4, the B₂ configuration.
The braid relation at Cartan product 3: the product of the two reflections has order
dividing 6, the G₂ configuration.
The order is no smaller #
The lower bounds are read off a single vector: the αᵢ^∨-coordinate of gⁿ • αᵢ is a Chebyshev
expression in the Cartan product c, and comparing it with ⟨αᵢ, αᵢ^∨⟩ = 2 rules out gⁿ = 1.
At Cartan product 1 the product of the two reflections has order exactly 3.
At Cartan product 2 the product of the two reflections has order exactly 4.
At Cartan product 3 the product of the two reflections has order exactly 6.
The entries of the Coxeter matrix of a base #
The entries of the Coxeter matrix of a base are the orders of the products of the
corresponding simple reflections. On the diagonal both sides are 1, a simple reflection being
an involution; off the diagonal the four Cartan products 0, 1, 2, 3 give the four dihedral
orders 2, 3, 4, 6.
The braid relations of the Coxeter matrix of a base hold in the Weyl group. This is the
relation half of the Coxeter presentation of the Weyl group. It is not a simp lemma: its
left-hand side is not in simp normal form, because the exponent coxeterMatrixOfBase P b k l is
itself rewritten by TauCeti.coxeterMatrixOfBase_apply.