The Bruhat order on a Coxeter group

Let cs : CoxeterSystem M W be a Coxeter system. The Bruhat graph of cs has an edge from u to w whenever w = t * u for a reflection t and w is the longer of the two; the Bruhat order cs.BruhatLE is the reachability relation of that graph, the reflexive transitive closure of the edge relation.

Two things make this a well-behaved order rather than a bare relation. It is a partial order: an edge strictly increases the length, so a cycle would have to be constant, and cs.bruhatPartialOrder packages the three order axioms as data. And it satisfies the necessary direction of the subword property: if u ≤ w then u is spelled by a sublist of every word spelling w, reduced or not (CoxeterSystem.BruhatLE.exists_sublist_wordProd_eq). Since a reduced word for w is in particular a word for w, this says that every reduced word for w, not merely some one of them, has a subword spelling u.

The subword property identifies this graph-theoretic order with the classical reduced-word description: u ≤ w exactly when a reduced word for w has a subword spelling u. The converse direction follows from the right-multiplication lifting property, which controls how Bruhat comparisons change when both endpoints are multiplied by the same simple reflection.

Main definitions

• CoxeterSystem.BruhatStep: the edge relation of the Bruhat graph, w = t * u for a reflection t with ℓ u < ℓ w.
• CoxeterSystem.BruhatLE: the Bruhat order, the reflexive transitive closure of BruhatStep.
• CoxeterSystem.bruhatPartialOrder: the Bruhat order as a PartialOrder on W.
• CoxeterSystem.MinimalCosetRepCovBy: the covering relation of the Bruhat order of a parabolic quotient W / W_J, on minimal coset representatives.
• CoxeterSystem.MinimalCosetRepChain: the saturated chains of W / W_J, descending through covers, as Mathlib RelSeries.

Main results

• CoxeterSystem.BruhatLE.length_le and CoxeterSystem.BruhatLE.length_lt_of_ne: the length is monotone along the order, and strictly monotone below the top.
• CoxeterSystem.BruhatLE.antisymm: the Bruhat order is antisymmetric, so together with reflexivity and transitivity it is a partial order.
• CoxeterSystem.one_bruhatLE and CoxeterSystem.bruhatLE_one_iff: the identity is the least element.
• CoxeterSystem.bruhatLE_inv_iff: the order is invariant under inversion.
• CoxeterSystem.BruhatLE.exists_sublist_wordProd_eq and CoxeterSystem.BruhatLE.exists_sublist_wordProd_eq_length_eq: an element below w is spelled by a sublist of every word spelling w, and by a reduced such sublist. This is the necessary direction of the subword property.
• CoxeterSystem.bruhatLE_wordProd_eraseIdx: deleting one letter of a reduced word moves down the order.
• CoxeterSystem.bruhatLE_wordProd_of_sublist: every subword of a reduced word spells an element below the product of the whole word.
• CoxeterSystem.bruhatLE_iff_exists_sublist_wordProd_eq: the full subword characterization of Bruhat order.
• CoxeterSystem.BruhatLE.bruhatLE_mul_simple: the lifting property in the form u ≤ w * s when u ≤ w and s lengthens u.
• CoxeterSystem.BruhatLE.simple_mul_of_isLeftDescent, CoxeterSystem.BruhatLE.simple_mul_of_not_isLeftDescent, CoxeterSystem.BruhatLE.simple_mul_simple_mul_of_isLeftDescent and CoxeterSystem.BruhatLE.bruhatLE_simple_mul: the left-multiplication forms of the lifting property.
• CoxeterSystem.IsMinimalCosetRep.bruhatLE_mul and CoxeterSystem.isMinimalCosetRep_iff_forall_bruhatLE_mul: a minimal representative of a left coset of a standard parabolic subgroup is the Bruhat-least element of that coset.
• CoxeterSystem.IsMinimalCosetRep.bruhatLE_of_bruhatLE_mul and CoxeterSystem.BruhatLE.minimalCosetRep: the projection to minimal coset representatives is monotone; CoxeterSystem.minimalCosetRep_bruhatLE says that it moves down.
• CoxeterSystem.MinimalCosetRepChain.bruhatLE_of_le: a saturated chain of W / W_J descends in the Bruhat order.
• CoxeterSystem.MinimalCosetRepCovBy.exists_isReflection: a cover of a parabolic quotient is the projection of a Bruhat edge t * x < x; CoxeterSystem.minimalCosetRepCovBy_one_simple is the cover of the identity by a simple reflection.

References

The Coxeter-system input is CoxeterSystem.strongExchange of TauCeti/GroupTheory/Coxeter/StrongExchange.lean, together with Mathlib's length, reflection and inversion-sequence API for CoxeterSystem.

• A. Björner and F. Brenti, Combinatorics of Coxeter Groups, Springer GTM 231 (2005), Sections 2.1, 2.2 and 2.5.
• N. Bourbaki, Groupes et algèbres de Lie, Chapitres IV-VI, Ch. IV, §1, Exercise 3.
• J. E. Humphreys, Reflection Groups and Coxeter Groups, CUP (1990), Section 5.9.

The Bruhat graph

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

One step up in the Bruhat order: w is obtained from u by multiplying by a reflection, and is the longer of the two. This is the edge relation of the Bruhat graph of cs.

theorem CoxeterSystem.bruhatStep_iff {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {u w : W} : cs.BruhatStep u w ↔ ∃ (t : W), cs.IsReflection t ∧ w = t * u ∧ cs.length u < cs.length w

theorem CoxeterSystem.bruhatStep_mul_left {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {u t : W} (ht : cs.IsReflection t) (h : cs.length u < cs.length (t * u)) : cs.BruhatStep u (t * u)

theorem CoxeterSystem.BruhatStep.length_lt {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} {cs : CoxeterSystem M W} {u w : W} (h : cs.BruhatStep u w) : cs.length u < cs.length w

theorem CoxeterSystem.BruhatStep.inv {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} {cs : CoxeterSystem M W} {u w : W} (h : cs.BruhatStep u w) : cs.BruhatStep u⁻¹ w⁻¹

The Bruhat graph is invariant under inversion: conjugating the reflection of an edge by u turns an edge u → w into an edge u⁻¹ → w⁻¹.

theorem CoxeterSystem.one_bruhatStep {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {t : W} (ht : cs.IsReflection t) : cs.BruhatStep 1 t

A reflection lies above the identity in the Bruhat graph: its length is odd, hence positive.

theorem CoxeterSystem.bruhatStep_or_bruhatStep_mul_left {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {t : W} (ht : cs.IsReflection t) (u : W) : cs.BruhatStep u (t * u) ∨ cs.BruhatStep (t * u) u

Multiplying by a reflection always produces an edge of the Bruhat graph, in one direction or the other: a reflection never preserves the length.

theorem CoxeterSystem.bruhatStep_mul_simple {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {w : W} (i : B) (h : cs.length w < cs.length (w * cs.simple i)) : cs.BruhatStep w (w * cs.simple i)

Appending a simple reflection on the right is an edge of the Bruhat graph whenever it lengthens: the conjugate w * s i * w⁻¹ is the reflection realizing it.

theorem CoxeterSystem.bruhatStep_simple_mul {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {w : W} (i : B) (h : cs.length w < cs.length (cs.simple i * w)) : cs.BruhatStep w (cs.simple i * w)

Prepending a simple reflection is an edge of the Bruhat graph whenever it lengthens.

theorem CoxeterSystem.bruhatStep_wordProd_eraseIdx {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {ω : List B} {j : ℕ} (h : cs.length (cs.wordProd (ω.eraseIdx j)) < cs.length (cs.wordProd ω)) : cs.BruhatStep (cs.wordProd (ω.eraseIdx j)) (cs.wordProd ω)

Deleting a letter of a word is an edge of the Bruhat graph as soon as it shortens: the entry of the left inversion sequence at that position is the reflection realizing it.

The Bruhat order

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

The Bruhat order on a Coxeter group: u ≤ w when w is reachable from u in the Bruhat graph, that is, when a chain of reflections leads from u up to w with the length increasing at each step.

theorem CoxeterSystem.bruhatLE_iff_reflTransGen {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {u w : W} : cs.BruhatLE u w ↔ Relation.ReflTransGen cs.BruhatStep u w

theorem CoxeterSystem.bruhatLE_refl {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (w : W) : cs.BruhatLE w w

theorem CoxeterSystem.BruhatStep.bruhatLE {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} {cs : CoxeterSystem M W} {u w : W} (h : cs.BruhatStep u w) : cs.BruhatLE u w

theorem CoxeterSystem.BruhatLE.trans {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} {cs : CoxeterSystem M W} {u v w : W} (h₁ : cs.BruhatLE u v) (h₂ : cs.BruhatLE v w) : cs.BruhatLE u w

theorem CoxeterSystem.BruhatLE.tail {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} {cs : CoxeterSystem M W} {u v w : W} (h : cs.BruhatLE u v) (hs : cs.BruhatStep v w) : cs.BruhatLE u w

theorem CoxeterSystem.BruhatLE.length_le {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) : cs.length u ≤ cs.length w

The length is monotone along the Bruhat order, each edge increasing it.

theorem CoxeterSystem.BruhatLE.length_lt_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) : cs.length u < cs.length w

Below the top, the length increases strictly: a nontrivial chain has at least one edge.

theorem CoxeterSystem.BruhatLE.antisymm {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) (h₂ : cs.BruhatLE w u) : u = w

The Bruhat order is antisymmetric: a two-way chain cannot increase the length.

theorem CoxeterSystem.BruhatLE.inv {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) : cs.BruhatLE u⁻¹ w⁻¹

The Bruhat order is invariant under inversion.

@[simp]

theorem CoxeterSystem.bruhatLE_inv_iff {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {u w : W} : cs.BruhatLE u⁻¹ w⁻¹ ↔ cs.BruhatLE u w

The Bruhat order is invariant under inversion: u⁻¹ ≤ w⁻¹ exactly when u ≤ w, since inverting a chain of edges term by term is an involution on chains.

@[simp]

theorem CoxeterSystem.one_bruhatLE {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (w : W) : cs.BruhatLE 1 w

The identity is the least element of the Bruhat order: every element of a Coxeter group lies above 1.

@[simp]

theorem CoxeterSystem.bruhatLE_one_iff {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {w : W} : cs.BruhatLE w 1 ↔ w = 1

The only element below the identity is the identity itself, since 1 is the least element of the Bruhat order and the order is antisymmetric.

@[instance_reducible]

def CoxeterSystem.bruhatPartialOrder {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) : PartialOrder W

The Bruhat order as a partial order on the Coxeter group. It is stated as data rather than as an instance: a Coxeter group carries no order of its own, and a second Coxeter system on the same group need not give the same one.

@[simp]

theorem CoxeterSystem.bruhatPartialOrder_le {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) : LE.le = cs.BruhatLE

The ≤ of CoxeterSystem.bruhatPartialOrder is CoxeterSystem.BruhatLE.

@[simp]

theorem CoxeterSystem.bruhatPartialOrder_lt {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {u w : W} : u < w ↔ cs.BruhatLE u w ∧ u ≠ w

The < of CoxeterSystem.bruhatPartialOrder is CoxeterSystem.BruhatLE away from the diagonal.

The subword description

theorem CoxeterSystem.BruhatLE.exists_sublist_wordProd_eq {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) (ω : List B) : cs.wordProd ω = w → ∃ (σ : List B), σ.Sublist ω ∧ cs.wordProd σ = u

An element below w is spelled by a sublist of every word spelling w. The word need not be reduced, so in particular every reduced word for w, not merely some one of them, has a subword spelling u. This is the necessary direction of the subword property; the converse is not proved here.

theorem CoxeterSystem.BruhatLE.exists_sublist_wordProd_eq_length_eq {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) (ω : List B) (hω : cs.wordProd ω = w) : ∃ (σ : List B), σ.Sublist ω ∧ cs.wordProd σ = u ∧ σ.length = cs.length u

An element below w is spelled by a reduced sublist of every word spelling w, whose length is therefore its own Coxeter length. This refines CoxeterSystem.BruhatLE.exists_sublist_wordProd_eq by shrinking the sublist to a reduced one.

theorem CoxeterSystem.bruhatLE_wordProd_eraseIdx {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {ω : List B} (hω : cs.IsReduced ω) {j : ℕ} (hj : j < ω.length) : cs.BruhatLE (cs.wordProd (ω.eraseIdx j)) (cs.wordProd ω)

Deleting one letter of a reduced word moves down the Bruhat order. This is the one-letter case of the converse of CoxeterSystem.BruhatLE.exists_sublist_wordProd_eq; the general case, which would identify cs.BruhatLE with the classical reduced-word definition, is not proved here.

The lifting property and the subword characterization

theorem CoxeterSystem.BruhatStep.mul_simple_of_not_isRightDescent {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} {cs : CoxeterSystem M W} {u w : W} (h : cs.BruhatStep u w) (i : B) (hw : ¬cs.IsRightDescent w i) : cs.BruhatStep (u * cs.simple i) (w * cs.simple i)

Right multiplication by a simple reflection preserves a Bruhat edge when it lengthens the upper endpoint.

theorem CoxeterSystem.bruhatStep_mul_simple_of_isRightDescent {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} {cs : CoxeterSystem M W} {w : W} (i : B) (hw : cs.IsRightDescent w i) : cs.BruhatStep (w * cs.simple i) w

A right descent gives the downward Bruhat edge obtained by multiplying by that simple reflection.

theorem CoxeterSystem.BruhatLE.mul_simple_of_isRightDescent {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) (i : B) (hw : cs.IsRightDescent w i) : cs.BruhatLE (u * cs.simple i) w

At a right descent of the upper endpoint, right multiplication of the lower endpoint by the same simple reflection remains below the original upper endpoint.

theorem CoxeterSystem.BruhatLE.mul_simple_of_not_isRightDescent {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) (i : B) (hw : ¬cs.IsRightDescent w i) : cs.BruhatLE (u * cs.simple i) (w * cs.simple i)

At a right ascent of the upper endpoint, right multiplication of both endpoints by the same simple reflection preserves Bruhat order.

theorem CoxeterSystem.bruhatLE_wordProd_of_sublist {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {σ ω : List B} (hω : cs.IsReduced ω) (hσω : σ.Sublist ω) : cs.BruhatLE (cs.wordProd σ) (cs.wordProd ω)

Every subword of a reduced word spells an element below the product of that word. The subword itself need not be reduced. This is the converse of CoxeterSystem.BruhatLE.exists_sublist_wordProd_eq.

theorem CoxeterSystem.bruhatLE_iff_exists_sublist_wordProd_eq {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {u : W} {ω : List B} (hω : cs.IsReduced ω) : cs.BruhatLE u (cs.wordProd ω) ↔ ∃ (σ : List B), σ.Sublist ω ∧ cs.wordProd σ = u

The subword characterization of Bruhat order for a fixed reduced word. An element is below the product of ω exactly when some subword of ω spells it.

theorem CoxeterSystem.BruhatLE.bruhatLE_mul_simple {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) {i : B} (hu : ¬cs.IsRightDescent u i) : cs.BruhatLE u (w * cs.simple i)

Lifting property, lower form. If u ≤ w and the simple reflection s i lengthens u, then u ≤ w * s i. This is the substantial case of the lifting property when s i shortens w; when it lengthens w, already w ≤ w * s i.

The left-multiplication forms of the lifting property follow by inversion.

theorem CoxeterSystem.BruhatLE.simple_mul_of_isLeftDescent {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) (i : B) (hw : cs.IsLeftDescent w i) : cs.BruhatLE (cs.simple i * u) w

At a left descent of the upper endpoint, left multiplication of the lower endpoint by the same simple reflection remains below the original upper endpoint.

theorem CoxeterSystem.BruhatLE.simple_mul_of_not_isLeftDescent {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) (i : B) (hw : ¬cs.IsLeftDescent w i) : cs.BruhatLE (cs.simple i * u) (cs.simple i * w)

At a left ascent of the upper endpoint, left multiplication of both endpoints by the same simple reflection preserves Bruhat order.

theorem CoxeterSystem.BruhatLE.bruhatLE_simple_mul {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) {i : B} (hu : ¬cs.IsLeftDescent u i) : cs.BruhatLE u (cs.simple i * w)

Lifting property, lower left form. If u ≤ w and the simple reflection s i lengthens u on the left, then u ≤ s i * w.

theorem CoxeterSystem.BruhatLE.simple_mul_simple_mul_of_isLeftDescent {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) {i : B} (hu : cs.IsLeftDescent u i) : cs.BruhatLE (cs.simple i * u) (cs.simple i * w)

At a left descent of the lower endpoint, left multiplication of both endpoints by that simple reflection preserves Bruhat order.

Minimal coset representatives

theorem CoxeterSystem.IsMinimalCosetRep.bruhatLE_mul {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.BruhatLE u (u * v)

A minimal coset representative lies below every element of its coset. If u has minimal length in u · cs.parabolic J and v ∈ cs.parabolic J, then u ≤ u * v: lengths add, so a reduced word for u followed by one for v is a reduced word for u * v containing the first as a subword.

theorem CoxeterSystem.isMinimalCosetRep_iff_forall_bruhatLE_mul {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 ↔ ∀ v ∈ cs.parabolic J, cs.BruhatLE u (u * v)

Minimal coset representatives are the Bruhat-least elements of their cosets.

theorem CoxeterSystem.IsMinimalCosetRep.bruhatLE_of_bruhatLE_mul {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {J : Set B} {y v p : W} (hy : cs.IsMinimalCosetRep J y) (hp : p ∈ cs.parabolic J) (h : cs.BruhatLE y (v * p)) : cs.BruhatLE y v

Projection to minimal coset representatives is monotone. If a minimal coset representative y lies below an element v * p of the coset of v, then y ≤ v.

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

The minimal coset representative of w lies below w in the Bruhat order.

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

Projection to minimal coset representatives is monotone for the Bruhat order.

structure CoxeterSystem.MinimalCosetRepCovBy {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (J : Set B) (y x : W) : Prop

y is covered by x in the Bruhat order of the parabolic quotient W / W_J, modelled on the minimal coset representatives: both are minimal coset representatives, y < x, and no minimal coset representative lies strictly between them.

• isMinimalCosetRep_left : cs.IsMinimalCosetRep J y

  The lower element is a minimal coset representative.

• isMinimalCosetRep_right : cs.IsMinimalCosetRep J x

  The upper element is a minimal coset representative.

• bruhatLE : cs.BruhatLE y x

  The lower element lies below the upper one.

• ne : y ≠ x

  The two elements are distinct.

• eq_or_eq (z : W) : cs.IsMinimalCosetRep J z → cs.BruhatLE y z → cs.BruhatLE z x → z = y ∨ z = x

  No minimal coset representative lies strictly between them.

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

A simple reflection outside a standard parabolic subgroup covers the identity in the Bruhat order of the parabolic quotient.

theorem CoxeterSystem.MinimalCosetRepCovBy.exists_isReflection {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) : ∃ (t : W), cs.IsReflection t ∧ cs.BruhatStep (t * x) x ∧ y⁻¹ * (t * x) ∈ cs.parabolic J

A cover in the parabolic quotient comes from a reflection. If y is covered by x among the minimal coset representatives for J, then there is a reflection t with t * x < x in the Bruhat graph such that y is the minimal representative of the coset of t * x.

@[reducible, inline]

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

A saturated chain of the parabolic quotient W / W_J, descending through covers: a RelSeries x₀, x₁, …, x_l of minimal coset representatives, as elements of the subtype {w // cs.IsMinimalCosetRep J w}, in which each x_{i+1} is covered by x_i (CoxeterSystem.MinimalCosetRepChain.minimalCosetRepCovBy). Its length l is the number of covers, and the chain of length 0 at x is RelSeries.singleton _ x.

theorem CoxeterSystem.MinimalCosetRepChain.minimalCosetRepCovBy {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} {cs : CoxeterSystem M W} {J : Set B} (C : cs.MinimalCosetRepChain J) (i : Fin C.length) : cs.MinimalCosetRepCovBy J ↑(C.toFun i.succ) ↑(C.toFun i.castSucc)

Each step x_{i+1} ⋖ x_i of a saturated chain of W / W_J is a cover.

theorem CoxeterSystem.MinimalCosetRepChain.bruhatLE_of_le {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} {cs : CoxeterSystem M W} {J : Set B} (C : cs.MinimalCosetRepChain J) {i j : Fin (C.length + 1)} (hij : i ≤ j) : cs.BruhatLE ↑(C.toFun j) ↑(C.toFun i)

In a saturated chain x₀ ⋗ x₁ ⋗ ⋯ ⋗ x_l of W / W_J, a later element lies below an earlier one in the Bruhat order.

theorem CoxeterSystem.MinimalCosetRepChain.bruhatLE_last_head {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.BruhatLE ↑(RelSeries.last C) ↑(RelSeries.head C)

The last element of a saturated chain of W / W_J lies below its first element in the Bruhat order.