The Coxeter system of a Tits system

The Weyl group of a Tits system is a Coxeter group, with the prescribed simple reflections. Its Coxeter matrix records the orders of products of pairs of simple reflections, with zero representing infinite order. The Coxeter length agrees with the word length already used to control multiplication of Bruhat cells. Consequently the Coxeter-group API applies to the Weyl quotient of any BN-pair, without finiteness assumptions.

The construction combines TitsSystem.exists_eraseIdx_prod_eq_of_wordLength_lt_right, the exchange condition obtained from Bruhat cells, with CoxeterSystem.ofExchange, the recognition theorem for Coxeter presentations. No additional relations or exchange axioms are assumed.

The Weyl group is irreducible, TauCeti.TitsSystem.IsIrreducible, if every subset J of the simple reflections S that commutes elementwise with its complement is empty or all of S. For nonempty S this says exactly that the Coxeter graph of (W, S) is connected.

Main definitions

• TauCeti.TitsSystem.coxeterMatrix: the Coxeter matrix of the simple reflections.
• TauCeti.TitsSystem.coxeterSystem: the Coxeter system on the Weyl group.
• TauCeti.TitsSystem.IsIrreducible: every set of simple reflections commuting elementwise with its complement is empty or everything.
• TauCeti.TitsSystem.isIrreducible_of_subsingleton_simple: a Tits system with at most one simple reflection is irreducible.

References

• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Chapter IV, §2, no. 4, Theorem 2, and §1, no. 6.
• J. E. Humphreys, Linear Algebraic Groups (1975), Section 29.3.

noncomputable def TauCeti.TitsSystem.coxeterMatrix {G : Type u} [Group G] (T : TitsSystem G) : CoxeterMatrix ↑T.simple

The Coxeter matrix of a Tits system: the entry at s, t is the order of s * t in its Weyl group. An entry zero denotes infinite order.

@[simp]

theorem TauCeti.TitsSystem.coxeterMatrix_apply {G : Type u} [Group G] (T : TitsSystem G) (s t : ↑T.simple) : T.coxeterMatrix.M s t = orderOf (↑s * ↑t)

The entries of the Coxeter matrix are the orders of the products of simple reflections.

def TauCeti.TitsSystem.IsIrreducible {G : Type u} [Group G] (T : TitsSystem G) : Prop

The Weyl group of a Tits system is irreducible if every set J of simple reflections that commutes elementwise with its complement is empty or all of S. For nonempty S this says exactly that the Coxeter graph of (W, S) is connected.

theorem TauCeti.TitsSystem.isIrreducible_iff {G : Type u} [Group G] (T : TitsSystem G) : T.IsIrreducible ↔ ∀ (J : Set ↑T.simple), (∀ s ∈ J, ∀ t ∉ J, ↑s * ↑t = ↑t * ↑s) → J = ∅ ∨ J = Set.univ

Unfolds TauCeti.TitsSystem.IsIrreducible.

theorem TauCeti.TitsSystem.isIrreducible_of_subsingleton_simple {G : Type u} [Group G] (T : TitsSystem G) (h : T.simple.Subsingleton) : T.IsIrreducible

A Tits system with at most one simple reflection is irreducible.

theorem TauCeti.TitsSystem.IsIrreducible.of_mulEquiv {G : Type u} [Group G] {T : TitsSystem G} (hirr : T.IsIrreducible) {H : Type v} [Group H] {T' : TitsSystem H} (e : T'.WeylGroup ≃* T.WeylGroup) (he : ⇑e ⁻¹' T.simple = T'.simple) : T'.IsIrreducible

Irreducibility transfers along an isomorphism of Weyl groups identifying the simple reflections.

noncomputable def TauCeti.TitsSystem.coxeterSystem {G : Type u} [Group G] (T : TitsSystem G) : CoxeterSystem T.coxeterMatrix T.WeylGroup

The Weyl quotient of a Tits system, equipped with its canonical Coxeter system indexed by the prescribed simple reflections.

@[simp]

theorem TauCeti.TitsSystem.coxeterSystem_simple {G : Type u} [Group G] (T : TitsSystem G) (s : ↑T.simple) : T.coxeterSystem.simple s = ↑s

The simple generators of the Coxeter system are the original simple reflections of the BN-pair, as elements of its Weyl quotient.

@[simp]

theorem TauCeti.TitsSystem.coxeterSystem_wordProd {G : Type u} [Group G] (T : TitsSystem G) (l : List ↑T.simple) : T.coxeterSystem.wordProd l = (List.map Subtype.val l).prod

A Coxeter word evaluates to the product of its original simple reflections in the Weyl quotient.

@[simp]

theorem TauCeti.TitsSystem.coxeterSystem_length {G : Type u} [Group G] (T : TitsSystem G) (w : T.WeylGroup) : T.coxeterSystem.length w = T.simpleGenerators.wordLength w

Coxeter length is the word length governing the Bruhat multiplication laws.

instance TauCeti.TitsSystem.instIsCoxeterGroupWeylGroup {G : Type u} [Group G] (T : TitsSystem G) : IsCoxeterGroup T.WeylGroup

The Weyl group of every Tits system is a Coxeter group, with no rank or finiteness assumptions.