Standard parabolic subgroups and minimal coset representatives

Let cs : CoxeterSystem M W be a Coxeter system with simple reflections indexed by B. For a set J ⊆ B the standard parabolic subgroup cs.parabolic J is the subgroup of W generated by the simple reflections s i with i ∈ J. Its elements are exactly those spelled by words all of whose letters lie in J (CoxeterSystem.mem_parabolic_iff_exists_wordProd_eq), and the word may be taken reduced. The first substantive statement here is that a reduced word for an element of cs.parabolic J never leaves the subgroup: each of its letters spells a simple reflection already in cs.parabolic J (CoxeterSystem.simple_mem_parabolic_of_isReduced).

The main theorem is the factorization of W along a standard parabolic subgroup. Call u a minimal coset representative when it has minimal length in its own left coset u · cs.parabolic J. Then:

• multiplying a minimal coset representative by a parabolic element adds lengths, ℓ (u * v) = ℓ u + ℓ v (CoxeterSystem.length_mul_of_isMinimalCosetRep);
• u is a minimal coset representative exactly when no i ∈ J is a right descent of u (CoxeterSystem.isMinimalCosetRep_iff);
• every w : W factors uniquely as w = u * v with u a minimal coset representative and v ∈ cs.parabolic J (CoxeterSystem.existsUnique_isMinimalCosetRep_mul), and the two lengths then add by the first item.

The same factorization is also available on the other side: ℓ (x * v) = ℓ x + ℓ v whenever x ∈ cs.parabolic J and v has no left descent in J (CoxeterSystem.length_mul_of_forall_not_isLeftDescent), and every w : W factors uniquely as such a product (CoxeterSystem.existsUnique_mem_parabolic_mul).

The development rests only on the exchange condition of TauCeti/GroupTheory/Coxeter/StrongExchange.lean: there is no geometric representation, no finiteness hypothesis, and no appeal to Matsumoto's theorem, which these results are meant to feed.

Membership of u in the left coset of w is spelled u⁻¹ * w ∈ cs.parabolic J throughout, rather than through a coset type, so that the statements compose directly with the length API.

Relation to Matsumoto's theorem

This file is the dihedral-parabolic input to Matsumoto's theorem, which is not proved here. That theorem factors an element along the standard parabolic subgroup on a pair of indices {i, i'}, and so consumes CoxeterSystem.existsUnique_mem_parabolic_mul for the factorization, CoxeterSystem.length_mul_of_forall_not_isLeftDescent for its length additivity, and CoxeterSystem.exists_isReduced_wordProd_eq_of_mem_parabolic together with CoxeterSystem.simple_mem_parabolic_of_isReduced for the reduced words of the parabolic factor.

Main definitions

• CoxeterSystem.parabolic: the standard parabolic subgroup attached to a set of indices.
• CoxeterSystem.IsMinimalCosetRep: having minimal length in one's own left coset of a standard parabolic subgroup.
• CoxeterSystem.minimalCosetRep: the minimal coset representative of the left coset of an element.

Main results

• CoxeterSystem.mem_parabolic_iff_exists_wordProd_eq and CoxeterSystem.exists_isReduced_wordProd_eq_of_mem_parabolic: membership in a standard parabolic subgroup is being spelled by a word, indeed by a reduced word, with letters in the given set.
• CoxeterSystem.simple_mem_parabolic_of_isReduced: every letter of a reduced word for an element of a standard parabolic subgroup spells a simple reflection lying in that subgroup.
• CoxeterSystem.length_mul_of_isMinimalCosetRep: lengths add across a minimal coset representative.
• CoxeterSystem.isMinimalCosetRep_iff: minimality in the coset is the absence of right descents in J.
• CoxeterSystem.existsUnique_isMinimalCosetRep_mul: the unique factorization of an element of W as a minimal coset representative times a parabolic element.
• CoxeterSystem.minimalCosetRepProdParabolicEquiv: the same factorization, as an equivalence {u // cs.IsMinimalCosetRep J u} × cs.parabolic J ≃ W.
• CoxeterSystem.IsMinimalCosetRep.eq_of_inv_mul_mem: each left coset has only one minimal coset representative; CoxeterSystem.minimalCosetRep picks it out, and CoxeterSystem.eq_minimalCosetRep_iff characterizes it.
• CoxeterSystem.IsMinimalCosetRep.simple_mul_of_isLeftDescent and CoxeterSystem.IsMinimalCosetRep.simple_mul_or_exists_eq_mul_simple (Deodhar's lemma): left multiplication by a simple reflection keeps a minimal coset representative minimal when it shortens it, and in general either keeps it minimal or stays in the same coset.
• CoxeterSystem.parabolic_le_iff: the universal property of a standard parabolic subgroup.
• CoxeterSystem.length_mul_of_forall_not_isLeftDescent and CoxeterSystem.existsUnique_mem_parabolic_mul: the same length additivity and unique factorization, on the other side, with the left-descent form of the minimality condition; CoxeterSystem.parabolicProdEquiv is that factorization as an equivalence.

References

• A. Björner and F. Brenti, Combinatorics of Coxeter Groups, Springer GTM 231 (2005), Section 2.4.
• N. Bourbaki, Groupes et algèbres de Lie, Chapitres IV-VI, Ch. IV, §1.8.
• V. V. Deodhar, On some geometric aspects of Bruhat orderings II. The parabolic analogue of Kazhdan–Lusztig polynomials, J. Algebra 111 (1987), 483–506.
• J. E. Humphreys, Reflection Groups and Coxeter Groups, CUP (1990), Section 1.10.

Standard parabolic subgroups

def CoxeterSystem.parabolic {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (J : Set B) : Subgroup W

The standard parabolic subgroup attached to a set J of indices: the subgroup of W generated by the simple reflections s i with i ∈ J.

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

@[simp]

theorem CoxeterSystem.parabolic_le_iff {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {J : Set B} {H : Subgroup W} : cs.parabolic J ≤ H ↔ ∀ i ∈ J, cs.simple i ∈ H

The universal property of a standard parabolic subgroup. It is the smallest subgroup of W containing the simple reflections indexed by J: it is contained in a subgroup H exactly when s i ∈ H for every i ∈ J.

theorem CoxeterSystem.parabolic_mono {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {J J' : Set B} (h : J ⊆ J') : cs.parabolic J ≤ cs.parabolic J'

@[simp]

theorem CoxeterSystem.parabolic_empty {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) : cs.parabolic ∅ = ⊥

theorem CoxeterSystem.wordProd_mem_parabolic {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {J : Set B} {ω : List B} (hω : ∀ i ∈ ω, i ∈ J) : cs.wordProd ω ∈ cs.parabolic J

A word with letters in J spells an element of the standard parabolic subgroup of J.

@[simp]

theorem CoxeterSystem.parabolic_univ {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) : cs.parabolic Set.univ = ⊤

theorem CoxeterSystem.sum_parabolic_univ {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) [Fintype W] [Fintype ↥(cs.parabolic Set.univ)] {A : Type u_3} [AddCommMonoid A] (f : W → A) : ∑ w : ↥(cs.parabolic Set.univ), f ↑w = ∑ w : W, f w

Summing over the full standard parabolic subgroup is summing over the Coxeter carrier.

theorem CoxeterSystem.exists_wordProd_eq_of_mem_parabolic {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {J : Set B} {w : W} (hw : w ∈ cs.parabolic J) : ∃ (ω : List B), (∀ i ∈ ω, i ∈ J) ∧ cs.wordProd ω = w

Every element of a standard parabolic subgroup is spelled by a word with letters in the defining set.

theorem CoxeterSystem.mem_parabolic_iff_exists_wordProd_eq {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {J : Set B} {w : W} : w ∈ cs.parabolic J ↔ ∃ (ω : List B), (∀ i ∈ ω, i ∈ J) ∧ cs.wordProd ω = w

Membership in a standard parabolic subgroup is being spelled by a word with letters in the defining set.

theorem CoxeterSystem.exists_isReduced_wordProd_eq_of_mem_parabolic {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {J : Set B} {w : W} (hw : w ∈ cs.parabolic J) : ∃ (ω : List B), cs.IsReduced ω ∧ (∀ i ∈ ω, i ∈ J) ∧ cs.wordProd ω = w

The word of CoxeterSystem.mem_parabolic_iff_exists_wordProd_eq may be taken reduced: every element of a standard parabolic subgroup is spelled by a reduced word with letters in the defining set.

Reduced words of parabolic elements stay inside the parabolic subgroup

theorem CoxeterSystem.simple_mem_parabolic_of_isLeftDescent {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {J : Set B} {w : W} (hw : w ∈ cs.parabolic J) {i : B} (hi : cs.IsLeftDescent w i) : cs.simple i ∈ cs.parabolic J

A left descent of an element of a standard parabolic subgroup lies in that subgroup. This is the single-letter case that CoxeterSystem.simple_mem_parabolic_of_isReduced iterates along a reduced word.

theorem CoxeterSystem.simple_mem_parabolic_of_isReduced {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {J : Set B} (ω : List B) : cs.IsReduced ω → cs.wordProd ω ∈ cs.parabolic J → ∀ i ∈ ω, cs.simple i ∈ cs.parabolic J

The letters of a reduced word for a parabolic element are parabolic. If ω is reduced and spells an element of cs.parabolic J, then s i lies in cs.parabolic J for every letter i of ω.

The conclusion is about the simple reflections rather than about the indices: injectivity of cs.simple is not available for an abstract Coxeter system, so a letter outside J could a priori spell the same reflection as one inside it.

theorem CoxeterSystem.exists_rightDescent_mem_of_mem_parabolic_of_ne_one {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {J : Set B} {v : W} (hv : v ∈ cs.parabolic J) (hv₁ : v ≠ 1) : ∃ i ∈ J, cs.IsRightDescent v i

Every element v ≠ 1 of cs.parabolic J has a right descent i with i ∈ J. This refines CoxeterSystem.exists_rightDescent_of_ne_one, which gives no control over the index.

Minimal coset representatives

def CoxeterSystem.IsMinimalCosetRep {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (J : Set B) (u : W) : Prop

u is a minimal coset representative for the standard parabolic subgroup of J when it has minimal length in its own left coset u · cs.parabolic J.

theorem CoxeterSystem.isMinimalCosetRep_one {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (J : Set B) : cs.IsMinimalCosetRep J 1

The identity is the minimal coset representative of the parabolic subgroup itself.

theorem CoxeterSystem.exists_isMinimalCosetRep {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (J : Set B) (w : W) : ∃ v ∈ cs.parabolic J, cs.IsMinimalCosetRep J (w * v)

Every left coset of a standard parabolic subgroup contains a minimal coset representative.

theorem CoxeterSystem.length_mul_of_isMinimalCosetRep {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {J : Set B} {u : W} (hu : cs.IsMinimalCosetRep J u) {v : W} (hv : v ∈ cs.parabolic J) : cs.length (u * v) = cs.length u + cs.length v

Lengths add across a minimal coset representative. If u has minimal length in u · cs.parabolic J and v lies in that parabolic subgroup, then ℓ (u * v) = ℓ u + ℓ v.

theorem CoxeterSystem.not_isRightDescent_mul_of_isMinimalCosetRep {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {J : Set B} {u : W} (hu : cs.IsMinimalCosetRep J u) {v : W} (hv : v ∈ cs.parabolic J) {i : B} (hi : cs.simple i ∈ cs.parabolic J) (hvi : ¬cs.IsRightDescent v i) : ¬cs.IsRightDescent (u * v) i

Let u be a minimal coset representative for cs.parabolic J and let v ∈ cs.parabolic J. If s i ∈ cs.parabolic J and i is not a right descent of v, then i is not a right descent of u * v. See [Björner–Brenti, Combinatorics of Coxeter Groups, §2.4] and [Humphreys, Reflection Groups and Coxeter Groups, §1.10].

@[simp]

theorem CoxeterSystem.isMinimalCosetRep_iff {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {J : Set B} {u : W} : cs.IsMinimalCosetRep J u ↔ ∀ i ∈ J, ¬cs.IsRightDescent u i

Minimality in the coset is the absence of right descents inside J.

theorem CoxeterSystem.existsUnique_isMinimalCosetRep_mul {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (J : Set B) (w : W) : ∃! p : W × W, cs.IsMinimalCosetRep J p.1 ∧ p.2 ∈ cs.parabolic J ∧ w = p.1 * p.2

Every element of W factors uniquely as a minimal coset representative times an element of the standard parabolic subgroup. The two lengths then add, by CoxeterSystem.length_mul_of_isMinimalCosetRep.

noncomputable def CoxeterSystem.minimalCosetRepProdParabolicEquiv {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (J : Set B) : { u : W // cs.IsMinimalCosetRep J u } × ↥(cs.parabolic J) ≃ W

The factorization along a standard parabolic subgroup, as an equivalence. Multiplication (u, v) ↦ u * v identifies pairs of a minimal coset representative u and an element v of cs.parabolic J with W, by CoxeterSystem.existsUnique_isMinimalCosetRep_mul.

@[simp]

theorem CoxeterSystem.minimalCosetRepProdParabolicEquiv_apply {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (J : Set B) (p : { u : W // cs.IsMinimalCosetRep J u } × ↥(cs.parabolic J)) : (cs.minimalCosetRepProdParabolicEquiv J) p = ↑p.1 * ↑p.2

CoxeterSystem.minimalCosetRepProdParabolicEquiv multiplies the two factors.

theorem CoxeterSystem.IsMinimalCosetRep.eq_of_inv_mul_mem {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {J : Set B} {u v : W} (hu : cs.IsMinimalCosetRep J u) (hv : cs.IsMinimalCosetRep J v) (h : u⁻¹ * v ∈ cs.parabolic J) : u = v

Minimal coset representatives are unique. Two minimal representatives of the same left coset of cs.parabolic J are equal.

noncomputable def CoxeterSystem.minimalCosetRep {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (J : Set B) (w : W) : W

The minimal coset representative of the left coset w · cs.parabolic J: its unique element of minimal length (CoxeterSystem.eq_minimalCosetRep_iff). This is the projection of W onto the parabolic quotient W / W_J, modelled on the minimal coset representatives.

theorem CoxeterSystem.isMinimalCosetRep_minimalCosetRep {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (J : Set B) (w : W) : cs.IsMinimalCosetRep J (cs.minimalCosetRep J w)

The minimal coset representative of w is a minimal coset representative.

@[simp]

theorem CoxeterSystem.inv_mul_minimalCosetRep_mem {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (J : Set B) (w : W) : w⁻¹ * cs.minimalCosetRep J w ∈ cs.parabolic J

The minimal coset representative of w lies in the left coset of w.

theorem CoxeterSystem.eq_minimalCosetRep_iff {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {J : Set B} {u w : W} : u = cs.minimalCosetRep J w ↔ cs.IsMinimalCosetRep J u ∧ w⁻¹ * u ∈ cs.parabolic J

The minimal coset representative of w is the only minimal coset representative in the left coset of w.

theorem CoxeterSystem.IsMinimalCosetRep.minimalCosetRep_eq {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {J : Set B} {u : W} (hu : cs.IsMinimalCosetRep J u) : cs.minimalCosetRep J u = u

A minimal coset representative is its own minimal coset representative.

@[simp]

theorem CoxeterSystem.minimalCosetRep_eq_self_iff {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {J : Set B} {w : W} : cs.minimalCosetRep J w = w ↔ cs.IsMinimalCosetRep J w

An element is its own minimal coset representative exactly when it is a minimal coset representative.

@[simp]

theorem CoxeterSystem.minimalCosetRep_minimalCosetRep {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (J : Set B) (w : W) : cs.minimalCosetRep J (cs.minimalCosetRep J w) = cs.minimalCosetRep J w

Taking the minimal coset representative is idempotent.

theorem CoxeterSystem.minimalCosetRep_eq_minimalCosetRep_iff {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {J : Set B} {v w : W} : cs.minimalCosetRep J v = cs.minimalCosetRep J w ↔ v⁻¹ * w ∈ cs.parabolic J

Two elements have the same minimal coset representative exactly when they lie in the same left coset.

theorem CoxeterSystem.IsMinimalCosetRep.simple_mul_of_isLeftDescent {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {J : Set B} {u : W} (hu : cs.IsMinimalCosetRep J u) {i : B} (hi : cs.IsLeftDescent u i) : cs.IsMinimalCosetRep J (cs.simple i * u)

Removing a left descent keeps a minimal coset representative minimal. If u is a minimal coset representative for cs.parabolic J and s i * u is shorter than u, then s i * u is a minimal coset representative too.

theorem CoxeterSystem.IsMinimalCosetRep.simple_mul_or_exists_eq_mul_simple {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {J : Set B} {u : W} (hu : cs.IsMinimalCosetRep J u) (i : B) : cs.IsMinimalCosetRep J (cs.simple i * u) ∨ ∃ j ∈ J, cs.simple i * u = u * cs.simple j

Deodhar's lemma. Let u be a minimal coset representative for cs.parabolic J and let s i be a simple reflection. Then either s i * u is again a minimal coset representative, or s i * u = u * s j for some j ∈ J, so that s i * u lies in the coset of u. The second case can only occur when s i * u is longer than u.

The factorization on the other side

theorem CoxeterSystem.length_mul_of_forall_not_isLeftDescent {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {J : Set B} {x : W} (hx : x ∈ cs.parabolic J) {v : W} (hv : ∀ i ∈ J, ¬cs.IsLeftDescent v i) : cs.length (x * v) = cs.length x + cs.length v

Lengths add across an element with no left descent in J. If x lies in cs.parabolic J and v has no left descent lying in J, then ℓ (x * v) = ℓ x + ℓ v.

theorem CoxeterSystem.existsUnique_mem_parabolic_mul {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (J : Set B) (w : W) : ∃! p : W × W, p.1 ∈ cs.parabolic J ∧ (∀ i ∈ J, ¬cs.IsLeftDescent p.2 i) ∧ w = p.1 * p.2

Every element of W factors uniquely as an element of the standard parabolic subgroup times an element with no left descent in J. The two lengths then add, by CoxeterSystem.length_mul_of_forall_not_isLeftDescent. This is the shape of the factorization consumed by the induction step of Matsumoto's theorem.

noncomputable def CoxeterSystem.parabolicProdEquiv {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (J : Set B) : ↥(cs.parabolic J) × { v : W // ∀ i ∈ J, ¬cs.IsLeftDescent v i } ≃ W

The factorization on the other side, as an equivalence. Multiplication (x, v) ↦ x * v identifies pairs of an element x of cs.parabolic J and an element v with no left descent in J with W, by CoxeterSystem.existsUnique_mem_parabolic_mul.

@[simp]

theorem CoxeterSystem.parabolicProdEquiv_apply {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (J : Set B) (p : ↥(cs.parabolic J) × { v : W // ∀ i ∈ J, ¬cs.IsLeftDescent v i }) : (cs.parabolicProdEquiv J) p = ↑p.1 * ↑p.2

CoxeterSystem.parabolicProdEquiv multiplies the two factors.