def CoxeterBruhat.StrongExchangeCondition {B : Type u_1} {W : Type u_3} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) : Prop

The Strong Exchange Condition: if $\omega$ is a reduced word for $w$ and $t$ is a reflection such that $\ell(wt) < \ell(w)$, then $wt$ is obtained from $\omega$ by deleting one letter.

def CoxeterBruhat.ReducedSublistProperty {B : Type u_1} {W : Type u_3} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) : Prop

The reduced sublist property: every word $\omega$ admits a reduced sublist $\tau$ with the same product. This is equivalent to the deletion condition.

theorem CoxeterBruhat.sublist_concat_cases {α : Type u_2} (σ l : List α) (s : α) : σ.Sublist (l ++ [s]) → σ.Sublist l ∨ ∃ (σ' : List α), σ = σ' ++ [s] ∧ σ'.Sublist l

Case analysis for a sublist of $l ++ [s]$: it is either a sublist of $l$ or has the form $\sigma' ++ [s]$ for some sublist $\sigma'$ of $l$.

theorem CoxeterBruhat.bruhatLE_subexpression_forward {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (hSEC : StrongExchangeCondition cs) (hRSP : ReducedSublistProperty cs) {v w : W} (hvw : BruhatLE cs v w) {ω : List B} (hred : cs.IsReduced ω) (hprod : w = cs.wordProd ω) : ∃ (σ : List B), σ.Sublist ω ∧ v = cs.wordProd σ

Tits' subexpression theorem (forward direction): if $v \le w$ in the Bruhat order and $\omega$ is a reduced word for $w$, then $v$ is the product of some sublist of $\omega$.

theorem CoxeterBruhat.subexpression_bruhatLE_backward {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (hSEC : StrongExchangeForBruhat cs) {v w : W} {ω : List B} (hred : cs.IsReduced ω) (hprod : w = cs.wordProd ω) {σ : List B} (hσ_sub : σ.Sublist ω) (hσ_eq : v = cs.wordProd σ) : BruhatLE cs v w

Tits' subexpression theorem (backward direction): if $\omega$ is a reduced word for $w$ and $v$ is the product of some sublist of $\omega$, then $v \le w$ in the Bruhat order.

theorem CoxeterBruhat.subexpression_theorem {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (hSEC_full : StrongExchangeCondition cs) (hRSP : ReducedSublistProperty cs) (hSEC : StrongExchangeForBruhat cs) {v w : W} {ω : List B} (hred : cs.IsReduced ω) (hprod : w = cs.wordProd ω) : BruhatLE cs v w ↔ ∃ (σ : List B), σ.Sublist ω ∧ v = cs.wordProd σ

Tits' subexpression theorem: $v \le w$ in the Bruhat order if and only if $v$ is the product of some sublist of a (any) reduced word $\omega$ for $w$.

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

The strict Bruhat order: $v < w$ iff $v \le w$ and $v \ne w$.

theorem CoxeterBruhat.bruhat_covering_lemma {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (hSEC : StrongExchangeForBruhat cs) {v w : W} (hvw : BruhatLT cs v w) (hcover : cs.length v + 1 = cs.length w) (i : B) (hv_up : ¬cs.IsRightDescent v i) (hne : v * cs.simple i ≠ w) : BruhatLT cs w (w * cs.simple i) ∧ BruhatLT cs (v * cs.simple i) (w * cs.simple i)

Bruhat covering lemma: given a Bruhat cover $v < w$ with $i$ not a right descent of $v$ and $v s_i \ne w$, both $w < w s_i$ and $v s_i < w s_i$ hold in the Bruhat order.

theorem CoxeterBruhat.bruhat_predecessor {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (hSEC_full : StrongExchangeCondition cs) (hRSP : ReducedSublistProperty cs) (hSEC : StrongExchangeForBruhat cs) {v w : W} (hvw : BruhatLT cs v w) : ∃ (u : W), BruhatLE cs v u ∧ BruhatLT cs u w ∧ cs.length u + 1 = cs.length w

Existence of an immediate Bruhat predecessor: for any $v < w$ there exists $u$ with $v \le u < w$ and $\ell(u) + 1 = \ell(w)$.

theorem CoxeterBruhat.bruhat_chain_property {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (hSEC_full : StrongExchangeCondition cs) (hRSP : ReducedSublistProperty cs) (hSEC : StrongExchangeForBruhat cs) {v w : W} (hvw : BruhatLT cs v w) : ∃ (n : ℕ) (f : Fin (n + 2) → W), f ⟨0, ⋯⟩ = v ∧ f ⟨n + 1, ⋯⟩ = w ∧ ∀ (i : Fin (n + 1)), BruhatLT cs (f ⟨↑i, ⋯⟩) (f ⟨↑i + 1, ⋯⟩) ∧ cs.length (f ⟨↑i, ⋯⟩) + 1 = cs.length (f ⟨↑i + 1, ⋯⟩)

The chain property for the Bruhat order: every strict inequality $v < w$ extends to a saturated chain $v = u_0 < u_1 < \cdots < u_{n+1} = w$ in which each $\ell(u_{i+1}) = \ell(u_i) + 1$.