The root-level exchange step

Right multiplication by a simple reflection changes the number of positive roots sent to negative roots by exactly one. Reflection bijects the two inversion sets away from its defining simple root, while that root itself changes sides.

This is the exchange step that underlies the Coxeter presentation of a Weyl group and the later identification of Coxeter length with the number of inversions.

Main results

• TauCeti.mem_inversions_mul_ofIdx_iff_not_mem shows that the reflecting root toggles membership in the inversion set. It needs only that the root is positive, so it covers the reflection in an arbitrary positive root and not just a simple one.
• TauCeti.ncard_inversions_mul_ofIdx_of_notMem and TauCeti.ncard_inversions_mul_ofIdx_of_mem say in which direction the count moves: it goes up exactly when the defining simple root is not already an inversion.
• TauCeti.ncard_inversions_mul_ofIdx proves that the inversion count changes by one.

References

This file implements the exchange target in Layer 1 of TauCetiRoadmap/RepresentationTheory/RootSystems/README.md. The mathematical convention follows Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6.

theorem TauCeti.mem_inversions_mul_ofIdx_iff_not_mem {ι : 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) (w : ↥P.weylGroup) [CharZero R] (b : P.Base) {i : ι} (hi : b.IsPos i) : i ∈ inversions P b (w * RootPairing.weylGroup.ofIdx P i) ↔ i ∉ inversions P b w

Right multiplication by the reflection in a positive root toggles whether that root is an inversion.

theorem TauCeti.ncard_inversions_mul_ofIdx_of_notMem {ι : 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) (w : ↥P.weylGroup) [CharZero R] (b : P.Base) [Finite ι] [IsDomain R] [P.IsCrystallographic] [P.IsReduced] {i : ι} (hi : i ∈ b.support) (hiw : i ∉ inversions P b w) : (inversions P b (w * RootPairing.weylGroup.ofIdx P i)).ncard = (inversions P b w).ncard + 1

Right multiplication by a simple reflection whose simple root is not yet an inversion raises the number of inversions by one.

theorem TauCeti.ncard_inversions_mul_ofIdx_of_mem {ι : 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) (w : ↥P.weylGroup) [CharZero R] (b : P.Base) [Finite ι] [IsDomain R] [P.IsCrystallographic] [P.IsReduced] {i : ι} (hi : i ∈ b.support) (hiw : i ∈ inversions P b w) : (inversions P b (w * RootPairing.weylGroup.ofIdx P i)).ncard + 1 = (inversions P b w).ncard

Right multiplication by a simple reflection whose simple root is already an inversion lowers the number of inversions by one.

theorem TauCeti.ncard_inversions_mul_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) (w : ↥P.weylGroup) [CharZero R] (b : P.Base) [Finite ι] [IsDomain R] [P.IsCrystallographic] [P.IsReduced] {i : ι} (hi : i ∈ b.support) : (inversions P b (w * RootPairing.weylGroup.ofIdx P i)).ncard = (inversions P b w).ncard + 1 ∨ (inversions P b (w * RootPairing.weylGroup.ofIdx P i)).ncard + 1 = (inversions P b w).ncard

Right multiplication by a simple reflection changes the number of inversions by exactly one.