The Coxeter presentation of the Weyl group

The Coxeter matrix of a base gives an abstract presented group. Its generators map to the simple reflections of the Weyl group because those reflections satisfy the Coxeter relations, and the resulting homomorphism is surjective because the simple reflections generate the Weyl group.

Tits' theorem says that this homomorphism is also injective: the braid relations are the only relations among the simple reflections, so the Weyl group with its simple reflections is a Coxeter system for the Coxeter matrix of the base. Its Coxeter length is the number of inversions, the positive roots sent to negative roots.

The proof is the characterization of Coxeter systems by the exchange condition (CoxeterSystem.ofExchange), applied with the inversion count as length function. The inversion count is the least length of a word in the simple reflections (TauCeti.isLeast_ncard_inversions), the product of two simple reflections has the order prescribed by the Coxeter matrix (RootPairing.weylGroup.orderOf_ofIdx_mul_ofIdx_eq_coxeterMatrixOfBase), and the exchange condition is the root-level strong exchange condition (TauCeti.exists_wordProd_eraseIdx_eq_mul_ofIdx): when the last letter does not lengthen a word, its simple root is an inversion of the word, and the reflection in it deletes a letter.

Main definitions

• TauCeti.weylCoxeterHom: the canonical homomorphism from the Coxeter group of a base to its Weyl group.
• TauCeti.weylCoxeterSystem: the Weyl group as a Coxeter system for the Coxeter matrix of a base.

Main results

• TauCeti.weylCoxeterHom_apply_simple: the abstract generator maps to the corresponding simple root reflection.
• TauCeti.weylCoxeterHom_wordProd: the homomorphism sends an abstract word to the same word in the Weyl group.
• TauCeti.weylCoxeterHom_surjective: the canonical homomorphism is surjective.
• TauCeti.weylCoxeterHom_injective: Tits' theorem, the canonical homomorphism is injective.
• TauCeti.weylCoxeterSystem_simple and TauCeti.weylCoxeterSystem_wordProd: the simple reflections of the Coxeter system are the simple root reflections.
• TauCeti.length_weylCoxeterSystem_eq: the Coxeter length of a Weyl-group element is its number of inversions.
• TauCeti.isReduced_weylCoxeterSystem_iff: a word is reduced exactly when the element it spells has as many inversions as the word has letters.
• RootPairing.exists_isReduced_forall_isLeftDescent: some reduced word spells an element of which every simple reflection is a left descent (a reduced word of the longest element of the Weyl group).
• RootPairing.weylCoxeterSystem_isReflection_ofIdx: the reflection in every root, simple or not, is a reflection of the Coxeter system.
• RootPairing.bruhatStep_ofIdx_mul_iff_mem_inversions: for a positive root β, s_β w → w is an edge of the Bruhat graph exactly when β is an inversion of w⁻¹.

References

• J. Tits, Le problème des mots dans les groupes de Coxeter, Symposia Mathematica 1 (1969), 175--185.
• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Chapter VI, §1, no. 5, Theorem 2.
• J. E. Humphreys, Reflection Groups and Coxeter Groups, Cambridge Studies in Advanced Mathematics 29 (1990), Sections 1.5--1.9.

noncomputable def TauCeti.weylCoxeterHom {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Finite ι] [CharZero R] [IsDomain R] [P.IsCrystallographic] (b : P.Base) : (coxeterMatrixOfBase P b).Group →* ↥P.weylGroup

The canonical homomorphism from the abstract Coxeter group attached to a base to its Weyl group, sending each abstract generator to the corresponding simple root reflection.

@[simp]

theorem TauCeti.weylCoxeterHom_apply_simple {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Finite ι] [CharZero R] [IsDomain R] [P.IsCrystallographic] (b : P.Base) (i : ↥b.support) : (weylCoxeterHom P b) ((coxeterMatrixOfBase P b).simple i) = RootPairing.weylGroup.ofIdx P ↑i

The canonical homomorphism sends an abstract Coxeter generator to the corresponding simple root reflection.

@[simp]

theorem TauCeti.weylCoxeterHom_wordProd {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Finite ι] [CharZero R] [IsDomain R] [P.IsCrystallographic] (b : P.Base) (l : List ↥b.support) : (weylCoxeterHom P b) ((coxeterMatrixOfBase P b).toCoxeterSystem.wordProd l) = wordProd P b l

The canonical homomorphism sends a word in the abstract Coxeter generators to the same word in the simple reflections of the Weyl group.

theorem TauCeti.weylCoxeterHom_surjective {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Finite ι] [CharZero R] [IsDomain R] [P.IsCrystallographic] (b : P.Base) [P.IsReduced] : Function.Surjective ⇑(weylCoxeterHom P b)

The canonical homomorphism from the Coxeter presentation to the Weyl group is surjective.

theorem TauCeti.weylCoxeterHom_injective {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Finite ι] [CharZero R] [IsDomain R] [P.IsCrystallographic] (b : P.Base) [P.IsReduced] : Function.Injective ⇑(weylCoxeterHom P b)

Tits' theorem: the braid relations are the only relations among the simple reflections. The canonical homomorphism from the Coxeter group of a base to the Weyl group is injective.

noncomputable def TauCeti.weylCoxeterSystem {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Finite ι] [CharZero R] [IsDomain R] [P.IsCrystallographic] (b : P.Base) [P.IsReduced] : CoxeterSystem (coxeterMatrixOfBase P b) ↥P.weylGroup

The Weyl group is a Coxeter system. For a base b of a finite reduced crystallographic root system, the Weyl group with the simple reflections of b is a Coxeter system for the Coxeter matrix of b: by Tits' theorem, it is the abstract Coxeter group of that matrix.

@[simp]

theorem TauCeti.weylCoxeterSystem_simple {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Finite ι] [CharZero R] [IsDomain R] [P.IsCrystallographic] (b : P.Base) [P.IsReduced] (i : ↥b.support) : (weylCoxeterSystem P b).simple i = RootPairing.weylGroup.ofIdx P ↑i

The simple reflections of the Coxeter system of the Weyl group are the simple root reflections.

@[simp]

theorem TauCeti.weylCoxeterSystem_wordProd {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Finite ι] [CharZero R] [IsDomain R] [P.IsCrystallographic] (b : P.Base) [P.IsReduced] (l : List ↥b.support) : (weylCoxeterSystem P b).wordProd l = wordProd P b l

A word in the simple reflections of the Coxeter system of the Weyl group spells the same element as the word in the simple root reflections.

@[simp]

theorem TauCeti.length_weylCoxeterSystem_eq {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Finite ι] [CharZero R] [IsDomain R] [P.IsCrystallographic] (b : P.Base) [P.IsReduced] (w : ↥P.weylGroup) : (weylCoxeterSystem P b).length w = (inversions P b w).ncard

Length equals inversions. The Coxeter length of a Weyl-group element is the number of positive roots it sends to negative roots.

theorem TauCeti.isReduced_weylCoxeterSystem_iff {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Finite ι] [CharZero R] [IsDomain R] [P.IsCrystallographic] (b : P.Base) [P.IsReduced] (l : List ↥b.support) : (weylCoxeterSystem P b).IsReduced l ↔ (inversions P b (wordProd P b l)).ncard = l.length

A word in the simple reflections is reduced exactly when the element it spells has as many inversions as the word has letters.

theorem RootPairing.exists_isReduced_forall_isLeftDescent {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Finite ι] [CharZero R] [IsDomain R] [P.IsCrystallographic] (b : P.Base) [P.IsReduced] : ∃ (ω : List ↥b.support), (TauCeti.weylCoxeterSystem P b).IsReduced ω ∧ ∀ (i : ↥b.support), (TauCeti.weylCoxeterSystem P b).IsLeftDescent ((TauCeti.weylCoxeterSystem P b).wordProd ω) i

A reduced word for the longest element: some reduced word in the simple reflections spells an element of which every simple reflection is a left descent.

theorem RootPairing.weylCoxeterSystem_isReflection_ofIdx {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Finite ι] [CharZero R] [IsDomain R] [P.IsCrystallographic] (b : P.Base) [P.IsReduced] (i : ι) : (TauCeti.weylCoxeterSystem P b).IsReflection (weylGroup.ofIdx P i)

Root reflections are Coxeter reflections. The reflection in any root, simple or not, is a conjugate of a simple reflection of the Coxeter system of the Weyl group, because every root is Weyl-conjugate to a simple root.

theorem RootPairing.bruhatStep_ofIdx_mul_iff_mem_inversions {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Finite ι] [CharZero R] [IsDomain R] [P.IsCrystallographic] (b : P.Base) [P.IsReduced] (w : ↥P.weylGroup) {β : ι} (hβ : b.IsPos β) : (TauCeti.weylCoxeterSystem P b).BruhatStep (weylGroup.ofIdx P β * w) w ↔ β ∈ TauCeti.inversions P b w⁻¹

Bruhat steps by root reflections. For a positive root β, reflecting in β moves w one step down the Bruhat graph, s_β w → w, exactly when β is an inversion of w⁻¹.