Standard parabolic subgroups are Coxeter groups

Let cs : CoxeterSystem M W and cs' : CoxeterSystem M' W' be Coxeter systems with simple reflections indexed by B and B', and let f : B → B' be a map along which the Coxeter matrices agree, M i j = M' (f i) (f j). Sending s i to s' (f i) respects the Coxeter relations of M, so it defines a homomorphism CoxeterSystem.parabolicHom cs cs' hf : W →* W' onto the standard parabolic subgroup cs'.parabolic (Set.range f).

The main theorem is that this homomorphism is injective and preserves lengths. In other words, the standard parabolic subgroup of W' attached to a set J of indices is the Coxeter group of the restriction of M' to J, and its length function is the restriction of the length function of W' (Bourbaki, Chapter IV, §1, no. 8, Theorem 2). For instance, the symmetric group on the first n letters sits inside the group of finitary permutations of ℕ with the same lengths.

The proof applies the characterization of Coxeter systems by the exchange condition (CoxeterSystem.injective_of_exchange): a reduced word in W' for an element of the parabolic subgroup has all of its letters in Set.range f (CoxeterSystem.simple_mem_parabolic_of_isReduced with CoxeterSystem.simple_mem_parabolic_iff), so the length in W' is computed by words in B, and the exchange condition of W' then gives the exchange condition for these words. The orders of the products of two generators are the entries of the Coxeter matrix (CoxeterSystem.orderOf_simple_mul_simple).

Main definitions

• CoxeterSystem.parabolicHom: the homomorphism W →* W' induced by a map of index types along which the Coxeter matrices agree.

Main results

• CoxeterSystem.simple_mem_parabolic_iff: a simple reflection lies in the standard parabolic subgroup of J exactly when its index lies in J.
• CoxeterSystem.parabolicHom_wordProd: the homomorphism sends the product of a word to the product of its image.
• CoxeterSystem.range_parabolicHom: its image is the standard parabolic subgroup of Set.range f.
• CoxeterSystem.length_parabolicHom: it preserves lengths.
• CoxeterSystem.parabolicHom_injective: it is injective.
• CoxeterSystem.isReduced_map_iff: a word is reduced exactly when its image is.

References

• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Chapter IV, §1, no. 8, Theorem 2.
• J. E. Humphreys, Reflection Groups and Coxeter Groups, Cambridge Studies in Advanced Mathematics 29 (1990), Section 5.5.

@[simp]

theorem CoxeterSystem.simple_mem_parabolic_iff {B : Type u_1} {W : Type u_3} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {J : Set B} {i : B} : cs.simple i ∈ cs.parabolic J ↔ i ∈ J

A simple reflection lies in a standard parabolic subgroup exactly when its index lies in the defining set.

def CoxeterSystem.parabolicHom {B : Type u_1} {B' : Type u_2} {W : Type u_3} {W' : Type u_4} [Group W] [Group W'] {M : CoxeterMatrix B} {M' : CoxeterMatrix B'} (cs : CoxeterSystem M W) (cs' : CoxeterSystem M' W') {f : B → B'} (hf : ∀ (i j : B), M.M i j = M'.M (f i) (f j)) : W →* W'

The homomorphism of Coxeter groups induced by a map f : B → B' of index types along which the Coxeter matrices agree, M i j = M' (f i) (f j): it sends s i to s' (f i). It is injective (CoxeterSystem.parabolicHom_injective) and length-preserving (CoxeterSystem.length_parabolicHom), with image the standard parabolic subgroup of Set.range f (CoxeterSystem.range_parabolicHom).

@[simp]

theorem CoxeterSystem.parabolicHom_simple {B : Type u_1} {B' : Type u_2} {W : Type u_3} {W' : Type u_4} [Group W] [Group W'] {M : CoxeterMatrix B} {M' : CoxeterMatrix B'} (cs : CoxeterSystem M W) {cs' : CoxeterSystem M' W'} {f : B → B'} (hf : ∀ (i j : B), M.M i j = M'.M (f i) (f j)) (i : B) : (cs.parabolicHom cs' hf) (cs.simple i) = cs'.simple (f i)

@[simp]

theorem CoxeterSystem.parabolicHom_wordProd {B : Type u_1} {B' : Type u_2} {W : Type u_3} {W' : Type u_4} [Group W] [Group W'] {M : CoxeterMatrix B} {M' : CoxeterMatrix B'} (cs : CoxeterSystem M W) {cs' : CoxeterSystem M' W'} {f : B → B'} (hf : ∀ (i j : B), M.M i j = M'.M (f i) (f j)) (ω : List B) : (cs.parabolicHom cs' hf) (cs.wordProd ω) = cs'.wordProd (List.map f ω)

The homomorphism CoxeterSystem.parabolicHom sends the product of a word to the product of its image under f.

theorem CoxeterSystem.range_parabolicHom {B : Type u_1} {B' : Type u_2} {W : Type u_3} {W' : Type u_4} [Group W] [Group W'] {M : CoxeterMatrix B} {M' : CoxeterMatrix B'} (cs : CoxeterSystem M W) {cs' : CoxeterSystem M' W'} {f : B → B'} (hf : ∀ (i j : B), M.M i j = M'.M (f i) (f j)) : (cs.parabolicHom cs' hf).range = cs'.parabolic (Set.range f)

The image of CoxeterSystem.parabolicHom is the standard parabolic subgroup of Set.range f.

@[simp]

theorem CoxeterSystem.length_parabolicHom {B : Type u_1} {B' : Type u_2} {W : Type u_3} {W' : Type u_4} [Group W] [Group W'] {M : CoxeterMatrix B} {M' : CoxeterMatrix B'} (cs : CoxeterSystem M W) {cs' : CoxeterSystem M' W'} {f : B → B'} (hf : ∀ (i j : B), M.M i j = M'.M (f i) (f j)) (w : W) : cs'.length ((cs.parabolicHom cs' hf) w) = cs.length w

The homomorphism CoxeterSystem.parabolicHom preserves lengths.

theorem CoxeterSystem.parabolicHom_injective {B : Type u_1} {B' : Type u_2} {W : Type u_3} {W' : Type u_4} [Group W] [Group W'] {M : CoxeterMatrix B} {M' : CoxeterMatrix B'} (cs : CoxeterSystem M W) {cs' : CoxeterSystem M' W'} {f : B → B'} (hf : ∀ (i j : B), M.M i j = M'.M (f i) (f j)) : Function.Injective ⇑(cs.parabolicHom cs' hf)

The homomorphism CoxeterSystem.parabolicHom is injective: the Coxeter relations of M are the only relations among the simple reflections s' (f i) of W'.

theorem CoxeterSystem.isReduced_map_iff {B : Type u_1} {B' : Type u_2} {W : Type u_3} {W' : Type u_4} [Group W] [Group W'] {M : CoxeterMatrix B} {M' : CoxeterMatrix B'} (cs : CoxeterSystem M W) {cs' : CoxeterSystem M' W'} {f : B → B'} (hf : ∀ (i j : B), M.M i j = M'.M (f i) (f j)) {ω : List B} : cs'.IsReduced (List.map f ω) ↔ cs.IsReduced ω

A word in B is reduced exactly when its image under f is reduced in W'.