The Weyl group acts simply transitively on the bases

A root pairing has many bases, and the Weyl group moves them around: an automorphism carries a base to a base (RootPairing.Base.map). This file proves that for a finite reduced crystallographic root pairing the Weyl group acts simply transitively on its bases: for any two bases b and b' there is exactly one Weyl-group element w with b.map w = b' (RootPairing.Base.existsUnique_map_eq).

The argument is the classical one. Fix b and b', and count the positive roots of b that a Weyl-group element w sends to negative roots of b'. If that count is not zero then some simple root αₖ of b is among them, because a positive root is built from simple roots by adding one simple root at a time while staying a root. Replacing w by w sₖ lowers the count by one: the simple reflection sₖ permutes the positive roots of b other than αₖ and negates αₖ. So some w sends every positive root of b to a positive root of b'. Such a w carries the simple roots of b onto those of b', since the simple roots are the positive roots that are not sums of two positive roots (TauCeti.mem_support_iff_isPos_and_forall_ne_add) and w is additive. Uniqueness reduces to TauCeti.eq_one_of_mapsTo_posRoots: an element of the Weyl group keeping every positive root of one base positive is the identity. The propagation from simple roots to all positive roots is TauCeti.mapsTo_posRoots_of_forall_mem_support.

Main results

• TauCeti.isPos_weylGroupToPerm_iff_of_mapsTo_posRoots and TauCeti.weylGroupToPerm_mem_support_iff_of_mapsTo_posRoots: a Weyl-group element sending the positive roots of b to positive roots of b' identifies the positive roots, and the simple roots, of the two bases.
• RootPairing.Base.exists_mapsTo_posRoots: some Weyl-group element sends the positive roots of b to positive roots of b', and TauCeti.eq_of_mapsTo_posRoots says it is unique.
• TauCeti.map_eq_iff_mapsTo_posRoots: b.map w = b' exactly when w sends the positive roots of b to positive roots of b'.
• RootPairing.Base.existsUnique_map_eq: the Weyl group acts simply transitively on the bases.

References

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, Ch. III, §10.3, Theorem (b) and (e).
• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Ch. VI, §1.5, Theorem 2.

theorem TauCeti.isPos_weylGroupToPerm_iff_of_mapsTo_posRoots {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [CharZero R] {b b' : P.Base} {w : ↥P.weylGroup} (h : Set.MapsTo (⇑(P.weylGroupToPerm w)) (posRoots P b) (posRoots P b')) (i : ι) : b'.IsPos ((P.weylGroupToPerm w) i) ↔ b.IsPos i

An element sending the positive roots of b to positive roots of b' also sends the negative roots of b to negative roots of b', so it identifies the two notions of positivity.

theorem TauCeti.weylGroupToPerm_mem_support_iff_of_mapsTo_posRoots {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [CharZero R] {b b' : P.Base} {w : ↥P.weylGroup} [Finite ι] [IsDomain R] [P.IsCrystallographic] (h : Set.MapsTo (⇑(P.weylGroupToPerm w)) (posRoots P b) (posRoots P b')) (i : ι) : (P.weylGroupToPerm w) i ∈ b'.support ↔ i ∈ b.support

An element matching the positive roots of two bases matches their simple roots. The simple roots are the positive roots that are not the sum of two positive roots, and a Weyl-group element preserves sums of roots.

theorem TauCeti.map_eq_iff_mapsTo_posRoots {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [CharZero R] {b b' : P.Base} {w : ↥P.weylGroup} [Finite ι] [IsDomain R] [P.IsCrystallographic] : b.map ↑w = b' ↔ Set.MapsTo (⇑(P.weylGroupToPerm w)) (posRoots P b) (posRoots P b')

A Weyl-group element carries b to b' exactly when it matches their positive roots.

theorem RootPairing.Base.exists_mapsTo_posRoots {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [CharZero R] [Finite ι] [IsDomain R] [P.IsCrystallographic] [P.IsReduced] (b b' : P.Base) : ∃ (w : ↥P.weylGroup), Set.MapsTo (⇑(P.weylGroupToPerm w)) (TauCeti.posRoots P b) (TauCeti.posRoots P b')

Some Weyl-group element matches the positive roots of two bases.

theorem TauCeti.eq_of_mapsTo_posRoots {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [CharZero R] {b b' : P.Base} {w : ↥P.weylGroup} [Finite ι] [IsDomain R] [P.IsCrystallographic] [P.IsReduced] {v : ↥P.weylGroup} (hv : Set.MapsTo (⇑(P.weylGroupToPerm v)) (posRoots P b) (posRoots P b')) (hw : Set.MapsTo (⇑(P.weylGroupToPerm w)) (posRoots P b) (posRoots P b')) : v = w

At most one Weyl-group element matches the positive roots of two bases.

theorem RootPairing.Base.existsUnique_map_eq {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [CharZero R] [Finite ι] [IsDomain R] [P.IsCrystallographic] [P.IsReduced] (b b' : P.Base) : ∃! w : ↥P.weylGroup, b.map ↑w = b'

The Weyl group acts simply transitively on the bases. Any base b is carried onto any other base b' by exactly one element of the Weyl group.