Documentation

TauCeti.GroupTheory.Coxeter.ExchangeCondition

The exchange condition characterizes Coxeter systems #

Let cs : CoxeterSystem M W be a Coxeter system and φ : W →* G a homomorphism of groups, so that the images φ (s i) of the simple reflections are involutions satisfying the braid relations of M. For g in the image of φ, let ℓ g be the least number of letters of a word whose image is g. Suppose that

Then φ is injective (CoxeterSystem.injective_of_exchange) and preserves lengths (CoxeterSystem.length_eq_of_exchange). These conclusions require no assumption on ℓ outside the image of φ. If every element of G is spelled by a word, then G is the Coxeter group of M, with the images of the simple reflections as generators; CoxeterSystem.ofExchange is that Coxeter system on G. This is the characterization of Coxeter systems by the exchange condition (Bourbaki, Chapter IV, §1, no. 6, Theorem 1).

The exchange condition is stated with ≤ as in Bourbaki: no parity of lengths in G is assumed, so the hypothesis covers multiplications that do not change the length, and the conclusion rules them out. Where lengths change by exactly one under multiplication by a generator, as for the Weyl group of a root system, the two forms agree.

The argument #

Call a word minimal if it has least length among the words with the same image in G. The core statement is that two minimal words of the same length with the same image have the same product in W. It is proved by induction on the length, following Humphreys.

Write the final letters of the two words as p and q. The exchange condition applied to the first word x and the letter q deletes one letter of x. Unless the deleted letter is the first one, the result followed by q shares its first letter with x and its last letter with the second word, and induction concludes. If the first letter is deleted, x may be replaced by x.tail ++ [q], which ends with the alternating pair p q; repeating with the roles of p and q exchanged, the suffix alternating between them lengthens until the two words are the two alternating words of their common length m. Their images agree, so (φ (s q) * φ (s p)) ^ m = 1 by CoxeterSystem.wordProd_alternatingWord_eq_mul_pow, and M q p divides m, while reducedness of the alternating word bounds m by M q p. Hence m = M q p, and the two words have the same product in W by the braid relation.

The core statement then shows that a word reduced in W is minimal: at the first letter where a prefix stops being minimal, the exchange condition would produce a shorter word with the same product. In particular a word reduced in W whose image is 1 is empty, so φ is injective.

Main definitions #

Main results #

References #

source
theorem CoxeterSystem.length_eq_of_exchange {B : Type u_1} {W : Type u_2} {G : Type u_3} [Group W] [Group G] {M : CoxeterMatrix B} {cs : CoxeterSystem M W} (φ : W →* G) (ℓ : G → ℕ) (horder : ∀ (i i' : B), orderOf (φ (cs.simple i) * φ (cs.simple i')) = M.M i i') (hℓ : ∀ (w : W), IsLeast {n : ℕ | ∃ (ω : List B), φ (cs.wordProd ω) = φ w ∧ ω.length = n} (ℓ (φ w))) (hexch : ∀ (ω : List B) (i : B), ℓ (φ (cs.wordProd ω)) = ω.length → ℓ (φ (cs.wordProd ω * cs.simple i)) ≤ ω.length → ∃ j < ω.length, φ (cs.wordProd (ω.eraseIdx j)) = φ (cs.wordProd ω * cs.simple i)) (w : W) :
ℓ (φ w) = cs.length w

A homomorphism satisfying the exchange condition preserves lengths. Let φ : W →* G be a homomorphism out of a Coxeter group such that each φ (s i) * φ (s i') has order M i i', let ℓ g be the least length of a word whose image is g for each g in the image of φ, and suppose that the images of the simple reflections satisfy the exchange condition: whenever a word ω of least length spells g and ℓ (g * φ (s i)) ≤ ℓ g, deleting some letter of ω spells g * φ (s i). Then ℓ (φ w) = cs.length w. No assumption is made on ℓ outside the image of φ.

source
theorem CoxeterSystem.injective_of_exchange {B : Type u_1} {W : Type u_2} {G : Type u_3} [Group W] [Group G] {M : CoxeterMatrix B} {cs : CoxeterSystem M W} (φ : W →* G) (ℓ : G → ℕ) (horder : ∀ (i i' : B), orderOf (φ (cs.simple i) * φ (cs.simple i')) = M.M i i') (hℓ : ∀ (w : W), IsLeast {n : ℕ | ∃ (ω : List B), φ (cs.wordProd ω) = φ w ∧ ω.length = n} (ℓ (φ w))) (hexch : ∀ (ω : List B) (i : B), ℓ (φ (cs.wordProd ω)) = ω.length → ℓ (φ (cs.wordProd ω * cs.simple i)) ≤ ω.length → ∃ j < ω.length, φ (cs.wordProd (ω.eraseIdx j)) = φ (cs.wordProd ω * cs.simple i)) :
Function.Injective ⇑φ

A homomorphism satisfying the exchange condition is injective. This is the statement that the braid relations are the only relations among the generators φ (s i): under the hypotheses of CoxeterSystem.length_eq_of_exchange, an element of W with trivial image has length 0.

source
noncomputable def CoxeterSystem.ofExchange {B : Type u_1} {W : Type u_2} {G : Type u_3} [Group W] [Group G] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (φ : W →* G) (ℓ : G → ℕ) (horder : ∀ (i i' : B), orderOf (φ (cs.simple i) * φ (cs.simple i')) = M.M i i') (hℓ : ∀ (g : G), IsLeast {n : ℕ | ∃ (ω : List B), φ (cs.wordProd ω) = g ∧ ω.length = n} (ℓ g)) (hexch : ∀ (ω : List B) (i : B), ℓ (φ (cs.wordProd ω)) = ω.length → ℓ (φ (cs.wordProd ω * cs.simple i)) ≤ ω.length → ∃ j < ω.length, φ (cs.wordProd (ω.eraseIdx j)) = φ (cs.wordProd ω * cs.simple i)) :
CoxeterSystem M G

The Coxeter system defined by the exchange condition. Under the hypotheses of CoxeterSystem.length_eq_of_exchange, with least word lengths given for every element of G, the homomorphism φ : W →* G is an isomorphism. Transporting cs along it makes G a Coxeter group whose simple reflections are the images φ (s i) (CoxeterSystem.ofExchange_simple) and whose length function is ℓ (CoxeterSystem.length_ofExchange).

Instances For
    source
    @[simp]
    theorem CoxeterSystem.ofExchange_simple {B : Type u_1} {W : Type u_2} {G : Type u_3} [Group W] [Group G] {M : CoxeterMatrix B} {cs : CoxeterSystem M W} (φ : W →* G) (ℓ : G → ℕ) (horder : ∀ (i i' : B), orderOf (φ (cs.simple i) * φ (cs.simple i')) = M.M i i') (hℓ : ∀ (g : G), IsLeast {n : ℕ | ∃ (ω : List B), φ (cs.wordProd ω) = g ∧ ω.length = n} (ℓ g)) (hexch : ∀ (ω : List B) (i : B), ℓ (φ (cs.wordProd ω)) = ω.length → ℓ (φ (cs.wordProd ω * cs.simple i)) ≤ ω.length → ∃ j < ω.length, φ (cs.wordProd (ω.eraseIdx j)) = φ (cs.wordProd ω * cs.simple i)) (i : B) :
    (cs.ofExchange φ ℓ horder hℓ hexch).simple i = φ (cs.simple i)

    The simple reflections of CoxeterSystem.ofExchange are the images of those of cs.

    source
    @[simp]
    theorem CoxeterSystem.ofExchange_wordProd {B : Type u_1} {W : Type u_2} {G : Type u_3} [Group W] [Group G] {M : CoxeterMatrix B} {cs : CoxeterSystem M W} (φ : W →* G) (ℓ : G → ℕ) (horder : ∀ (i i' : B), orderOf (φ (cs.simple i) * φ (cs.simple i')) = M.M i i') (hℓ : ∀ (g : G), IsLeast {n : ℕ | ∃ (ω : List B), φ (cs.wordProd ω) = g ∧ ω.length = n} (ℓ g)) (hexch : ∀ (ω : List B) (i : B), ℓ (φ (cs.wordProd ω)) = ω.length → ℓ (φ (cs.wordProd ω * cs.simple i)) ≤ ω.length → ∃ j < ω.length, φ (cs.wordProd (ω.eraseIdx j)) = φ (cs.wordProd ω * cs.simple i)) (ω : List B) :
    (cs.ofExchange φ ℓ horder hℓ hexch).wordProd ω = φ (cs.wordProd ω)

    A word for CoxeterSystem.ofExchange spells the image of the word for cs.

    source
    @[simp]
    theorem CoxeterSystem.length_ofExchange {B : Type u_1} {W : Type u_2} {G : Type u_3} [Group W] [Group G] {M : CoxeterMatrix B} {cs : CoxeterSystem M W} (φ : W →* G) (ℓ : G → ℕ) (horder : ∀ (i i' : B), orderOf (φ (cs.simple i) * φ (cs.simple i')) = M.M i i') (hℓ : ∀ (g : G), IsLeast {n : ℕ | ∃ (ω : List B), φ (cs.wordProd ω) = g ∧ ω.length = n} (ℓ g)) (hexch : ∀ (ω : List B) (i : B), ℓ (φ (cs.wordProd ω)) = ω.length → ℓ (φ (cs.wordProd ω * cs.simple i)) ≤ ω.length → ∃ j < ω.length, φ (cs.wordProd (ω.eraseIdx j)) = φ (cs.wordProd ω * cs.simple i)) (g : G) :
    (cs.ofExchange φ ℓ horder hℓ hexch).length g = ℓ g

    The length function of CoxeterSystem.ofExchange is ℓ.