The strong exchange condition and the identity criterion for inversion sets

If a word in the simple reflections spells a Weyl-group element sending a positive root to a negative root, then appending the reflection in that root to the word is spelled by the word with one of its letters deleted. This is the strong exchange condition, and it is the missing half of the identification of the inversion set as the obstruction to being the identity: an element with an empty inversion set is spelled by the empty word, so it is the identity.

Two features of the statement are what make it usable and are not shared by the weaker "some shorter word exists" form. The reflecting root ranges over all positive roots, not just the simple ones, so the condition applies to an arbitrary reflection of the Weyl group; and the shorter word is l.eraseIdx j for a named position j, a deletion that can be replayed verbatim on the corresponding word over any other family of generators indexed by b.support, in particular over the generators of the presented Coxeter group. The weaker form asserts only that some shorter word exists inside the Weyl group; it names no word over those generators to carry the assertion back through the presentation map, which is why the word property behind Tits' theorem consumes the deletion form.

The proof is an induction on the word. Peeling off the leading simple reflection sⱼ, either the shorter word already sends the root to a negative root, and the inductive hypothesis deletes a letter from it, or the shorter word sends it to a positive root that sⱼ makes negative. In the second case that positive root must be the simple root αⱼ itself, because a simple reflection permutes the remaining positive roots, and then conjugation identifies sⱼ with the appended reflection, so the leading letter is the one deleted.

Main results

• TauCeti.exists_wordProd_eraseIdx_eq_mul_ofIdx is the strong exchange condition.
• TauCeti.eq_one_of_inversions_eq_empty and TauCeti.inversions_eq_empty_iff_eq_one say that the inversion set of a Weyl-group element is empty exactly when the element is the identity.
• TauCeti.eq_one_of_mapsTo_posRoots restates this as: a Weyl-group element keeping every positive root positive is the identity.
• TauCeti.inversions_nonempty_of_ne_one and TauCeti.ncard_inversions_pos_of_ne_one are the contrapositive forms used to detect nontrivial Weyl-group elements.
• TauCeti.exists_mem_support_mem_inversions_of_ne_one sharpens the first of those to a simple inversion, which is what makes induction along right multiplication by simple reflections available.

References

This file supplies the root-level exchange condition of Layer 1 in TauCetiRoadmap/RepresentationTheory/RootSystems/README.md, the step through which the Coxeter presentation of Layer 2 proves that the braid relations are complete. The argument is the one in J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, Ch. III, §10.3.

theorem TauCeti.exists_wordProd_eraseIdx_eq_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) [Finite ι] [CharZero R] [IsDomain R] [P.IsCrystallographic] [P.IsReduced] (b : P.Base) {k : ι} (hk : b.IsPos k) (l : List ↥b.support) (h : ¬b.IsPos ((P.weylGroupToPerm (wordProd P b l)) k)) : ∃ j < l.length, wordProd P b (l.eraseIdx j) = wordProd P b l * RootPairing.weylGroup.ofIdx P k

The strong exchange condition. If the word l spells a Weyl-group element sending the positive root αₖ to a negative root, then the word l with the reflection sₖ appended is spelled by l with one of its letters deleted. The root αₖ is an arbitrary positive root, not necessarily a simple one, and the shorter word is a subword of l.

theorem TauCeti.eq_one_of_inversions_eq_empty {ι : 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} (h : inversions P b w = ∅) : w = 1

A Weyl-group element with an empty inversion set is the identity. A shortest word spelling it must be empty: otherwise its final simple reflection is an inversion of the word it follows, and the strong exchange condition produces a shorter word.

@[simp]

theorem TauCeti.inversions_eq_empty_iff_eq_one {ι : 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} : inversions P b w = ∅ ↔ w = 1

The inversion set of a Weyl-group element is empty exactly when the element is the identity.

theorem TauCeti.eq_one_of_mapsTo_posRoots {ι : 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} (h : Set.MapsTo (⇑(P.weylGroupToPerm w)) (posRoots P b) (posRoots P b)) : w = 1

A Weyl-group element keeping every positive root positive is the identity.

theorem TauCeti.inversions_nonempty_of_ne_one {ι : 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} (hw : w ≠ 1) : (inversions P b w).Nonempty

A Weyl-group element other than the identity sends some positive root to a negative root.

theorem TauCeti.ncard_inversions_pos_of_ne_one {ι : 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} (hw : w ≠ 1) : 0 < (inversions P b w).ncard

A Weyl-group element other than the identity has at least one inversion.

theorem TauCeti.mapsTo_posRoots_of_forall_mem_support {ι : 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) {w : ↥P.weylGroup} (h : ∀ i ∈ b.support, (P.weylGroupToPerm w) i ∈ posRoots P b) : Set.MapsTo (⇑(P.weylGroupToPerm w)) (posRoots P b) (posRoots P b)

A Weyl-group element sending every simple root to a positive root sends every positive root to a positive root. A positive root is built up from simple roots by addition, and the height of a sum of two roots is the sum of their heights, so the image again has nonnegative height. This is the mirror image of TauCeti.mapsTo_posRoots_negRoots_of_forall_mem_support.

theorem TauCeti.eq_one_of_forall_mem_support_mem_posRoots {ι : 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} (h : ∀ i ∈ b.support, (P.weylGroupToPerm w) i ∈ posRoots P b) : w = 1

A Weyl-group element keeping every simple root positive is the identity.

theorem TauCeti.exists_mem_support_mem_inversions_of_ne_one {ι : 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} (hw : w ≠ 1) : ∃ i ∈ b.support, i ∈ inversions P b w

A Weyl-group element other than the identity inverts some simple root. Sharpening TauCeti.inversions_nonempty_of_ne_one to a simple inversion is what makes induction along right multiplication by simple reflections available, since only a simple inversion is removed by TauCeti.ncard_inversions_mul_ofIdx_of_mem.