The chain property of the Bruhat order on a parabolic quotient

Let cs : CoxeterSystem M W be a Coxeter system and J a set of simple indices. The Bruhat order of the parabolic quotient W / W_J is modelled on the minimal coset representatives, with covering relation CoxeterSystem.MinimalCosetRepCovBy and saturated chains CoxeterSystem.MinimalCosetRepChain. This file proves that this order is graded by the Coxeter length:

• if y < x are minimal coset representatives, there is a minimal coset representative z with y ≤ z, a Bruhat edge from z to x, and ℓ z + 1 = ℓ x (the chain property);
• consequently y is covered by x in W / W_J exactly when y ≤ x and ℓ y + 1 = ℓ x;
• every saturated chain from x down to y has length ℓ x - ℓ y, and such a chain exists whenever y ≤ x.

For J = ∅ every element is a minimal coset representative, and the first statement is the chain property of the Bruhat order of W itself.

Saturated chains of W / W_λ, for the stabilizer W_λ of a dominant weight, carry the bonds and bond gcds of TauCeti/LinearAlgebra/RootSystem/Weyl/ChainBond.lean. The existence statement says that two comparable cosets are always joined by such a chain, and gradedness is the starting point for comparing different saturated chains between the same two cosets.

The proof is by induction on the length of x, removing a left descent s i of x. Left multiplication by s i preserves minimal coset representatives when it shortens them (CoxeterSystem.IsMinimalCosetRep.simple_mul_of_isLeftDescent), and when it lengthens one it either preserves minimality or stays in the same coset (Deodhar's lemma, CoxeterSystem.IsMinimalCosetRep.simple_mul_or_exists_eq_mul_simple). The comparisons are moved along by the left-multiplication forms of the lifting property.

Main results

• CoxeterSystem.IsMinimalCosetRep.exists_bruhatStep_of_bruhatLE: the chain property of W / W_J.
• CoxeterSystem.BruhatLE.exists_bruhatStep_of_ne: the chain property of the Bruhat order of W.
• CoxeterSystem.MinimalCosetRepCovBy.length_add_one_eq and CoxeterSystem.minimalCosetRepCovBy_iff: a cover of W / W_J raises the length by exactly one, and this characterizes the covers.
• CoxeterSystem.MinimalCosetRepChain.length_last_add_length: every saturated chain from x down to y has length ℓ x - ℓ y.
• CoxeterSystem.exists_minimalCosetRepChain: two comparable minimal coset representatives are joined by a saturated chain.
• CoxeterSystem.minimalCosetRepCovBy_simple_mul_of_isLeftDescent, CoxeterSystem.MinimalCosetRepCovBy.isLeftDescent_of_ne and CoxeterSystem.MinimalCosetRepCovBy.simple_mul_of_isLeftDescent: for a left descent s i of x, s i * x ⋖ x, and every other cover z ⋖ x has the left descent s i too, with s i * z ⋖ s i * x.

References

• A. Björner and F. Brenti, Combinatorics of Coxeter Groups, Springer GTM 231 (2005), Sections 2.2 (the chain property) and 2.5 (gradedness of the parabolic quotients).
• V. V. Deodhar, On some geometric aspects of Bruhat orderings II. The parabolic analogue of Kazhdan–Lusztig polynomials, J. Algebra 111 (1987), 483–506.

theorem CoxeterSystem.IsMinimalCosetRep.exists_bruhatStep_of_bruhatLE {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} {cs : CoxeterSystem M W} {J : Set B} {y x : W} (hy : cs.IsMinimalCosetRep J y) (hx : cs.IsMinimalCosetRep J x) (h : cs.BruhatLE y x) (hne : y ≠ x) : ∃ (z : W), cs.IsMinimalCosetRep J z ∧ cs.BruhatLE y z ∧ cs.BruhatStep z x ∧ cs.length z + 1 = cs.length x

The chain property of the parabolic quotient W / W_J. If y < x are minimal coset representatives for cs.parabolic J, then some minimal coset representative z with y ≤ z is joined to x by a Bruhat edge and is exactly one shorter than x.

theorem CoxeterSystem.BruhatLE.exists_bruhatStep_of_ne {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} {cs : CoxeterSystem M W} {u w : W} (h : cs.BruhatLE u w) (hne : u ≠ w) : ∃ (z : W), cs.BruhatLE u z ∧ cs.BruhatStep z w ∧ cs.length z + 1 = cs.length w

The chain property of the Bruhat order. If u < w, then some z with u ≤ z is joined to w by a Bruhat edge and is exactly one shorter than w.

theorem CoxeterSystem.MinimalCosetRepCovBy.length_add_one_eq {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} {cs : CoxeterSystem M W} {J : Set B} {y x : W} (h : cs.MinimalCosetRepCovBy J y x) : cs.length y + 1 = cs.length x

A cover of the parabolic quotient W / W_J raises the length by exactly one.

theorem CoxeterSystem.minimalCosetRepCovBy_iff {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} {cs : CoxeterSystem M W} {J : Set B} {y x : W} : cs.MinimalCosetRepCovBy J y x ↔ cs.IsMinimalCosetRep J y ∧ cs.IsMinimalCosetRep J x ∧ cs.BruhatLE y x ∧ cs.length y + 1 = cs.length x

The covers of the parabolic quotient W / W_J are the comparable pairs of minimal coset representatives whose lengths differ by one.

theorem CoxeterSystem.MinimalCosetRepChain.length_last_add_length {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} {cs : CoxeterSystem M W} {J : Set B} (C : cs.MinimalCosetRepChain J) : cs.length ↑(RelSeries.last C) + C.length = cs.length ↑(RelSeries.head C)

The parabolic quotient W / W_J is graded by the length. A saturated chain x₀ ⋗ x₁ ⋗ ⋯ ⋗ x_l of W / W_J has ℓ x_l + l = ℓ x₀; so all saturated chains between the same two elements have the same length.

theorem CoxeterSystem.exists_minimalCosetRepChain {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} {cs : CoxeterSystem M W} {J : Set B} {y x : W} (hy : cs.IsMinimalCosetRep J y) (hx : cs.IsMinimalCosetRep J x) (h : cs.BruhatLE y x) : ∃ (C : cs.MinimalCosetRepChain J), RelSeries.head C = ⟨x, hx⟩ ∧ RelSeries.last C = ⟨y, hy⟩

Comparable elements of the parabolic quotient W / W_J are joined by a saturated chain. If y ≤ x are minimal coset representatives for cs.parabolic J, there is a saturated chain of W / W_J from x down to y; its length is ℓ x - ℓ y, by CoxeterSystem.MinimalCosetRepChain.length_last_add_length.

Covers and left descents

theorem CoxeterSystem.minimalCosetRepCovBy_simple_mul_of_isLeftDescent {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} {cs : CoxeterSystem M W} {J : Set B} {x : W} (hx : cs.IsMinimalCosetRep J x) {i : B} (hi : cs.IsLeftDescent x i) : cs.MinimalCosetRepCovBy J (cs.simple i * x) x

Removing a left descent gives a cover. If s i is a left descent of a minimal coset representative x, then s i * x is covered by x in W / W_J.

theorem CoxeterSystem.MinimalCosetRepCovBy.isLeftDescent_of_ne {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} {cs : CoxeterSystem M W} {J : Set B} {z x : W} (h : cs.MinimalCosetRepCovBy J z x) {i : B} (hi : cs.IsLeftDescent x i) (hne : z ≠ cs.simple i * x) : cs.IsLeftDescent z i

A left descent of the top of a cover is a left descent of the bottom, unless the cover is s i * x ⋖ x. If z ⋖ x in W / W_J and s i is a left descent of x, then either z = s i * x or s i is a left descent of z: otherwise the lifting property gives z ≤ s i * x, and the two have the same length.

theorem CoxeterSystem.MinimalCosetRepCovBy.simple_mul_of_isLeftDescent {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} {cs : CoxeterSystem M W} {J : Set B} {z x : W} (h : cs.MinimalCosetRepCovBy J z x) {i : B} (hz : cs.IsLeftDescent z i) (hx : cs.IsLeftDescent x i) : cs.MinimalCosetRepCovBy J (cs.simple i * z) (cs.simple i * x)

A common left descent moves a cover down. If z ⋖ x in W / W_J and s i is a left descent of both, then s i * z ⋖ s i * x.