Generation of the Weyl group by simple reflections

For a base of a finite reduced crystallographic root system, every root reflection belongs to the subgroup generated by the reflections in the simple roots. Since the Weyl group is generated by all root reflections, the simple reflections generate the Weyl group.

The proof uses Mathlib's RootPairing.Base.induction_reflect, RootPairing.reflection_reflectionPerm, and RootPairing.weylGroup.induction: reflecting a positive root in a simple root conjugates its reflection by the corresponding simple reflection, while root negation does not change the reflection.

Main results

• TauCeti.weylGroup_eq_closure_simple identifies the Weyl group with the subgroup generated by its simple reflections.
• TauCeti.wordProd multiplies out a word in the simple reflections of a base.
• TauCeti.wordProd_reverse says that reversing a word inverts the element it spells.
• TauCeti.exists_wordProd_eq writes every Weyl-group element as a product of simple reflections.
• RootPairing.weylGroup.ofIdx_ne_ofIdx_of_ne says distinct simple roots give distinct simple reflections.

References

This file implements “Simple reflections generate” in Layer 2 of TauCetiRoadmap/RepresentationTheory/RootSystems/README.md. The argument follows the standard positive-root induction described there.

noncomputable def TauCeti.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) (b : P.Base) (l : List ↥b.support) : ↥P.weylGroup

The Weyl-group element spelled by a word in the simple reflections of a base.

Equations

• TauCeti.wordProd P b l = (List.map (fun (i : ↥b.support) => RootPairing.weylGroup.ofIdx P ↑i) l).prod

@[simp]

theorem TauCeti.wordProd_nil {ι : 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} (b : P.Base) : wordProd P b [] = 1

@[simp]

theorem TauCeti.wordProd_cons {ι : 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} (b : P.Base) (i : ↥b.support) (l : List ↥b.support) : wordProd P b (i :: l) = RootPairing.weylGroup.ofIdx P ↑i * wordProd P b l

@[simp]

theorem TauCeti.wordProd_append {ι : 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} (b : P.Base) (l l' : List ↥b.support) : wordProd P b (l ++ l') = wordProd P b l * wordProd P b l'

@[simp]

theorem TauCeti.wordProd_reverse {ι : 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} (b : P.Base) (l : List ↥b.support) : wordProd P b l.reverse = (wordProd P b l)⁻¹

Reversing a word inverts the Weyl-group element it spells, because a simple reflection is its own inverse.

theorem TauCeti.weylGroup_eq_closure_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] [P.IsReduced] (b : P.Base) : ⊤ = Subgroup.closure (Set.range fun (i : ↥b.support) => RootPairing.weylGroup.ofIdx P ↑i)

The simple reflections associated to a base generate the Weyl group.

theorem TauCeti.exists_wordProd_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] [P.IsReduced] (b : P.Base) (w : ↥P.weylGroup) : ∃ (l : List ↥b.support), wordProd P b l = w

Every Weyl-group element is spelled by a word in the simple reflections.

theorem RootPairing.weylGroup.ofIdx_ne_ofIdx_of_ne {ι : 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) (b : P.Base) [NeZero 2] {i j : ι} (hi : i ∈ b.support) (hj : j ∈ b.support) (hij : i ≠ j) : ofIdx P i ≠ ofIdx P j

Distinct simple roots give distinct simple reflections: the two reflections already disagree on the second simple root, since the two simple roots are linearly independent.