def Garrett.ExchangeDeletion.SatisfiesExchangeCondition {B : Type u_1} {W : Type u_2} [Group W] (M : CoxeterMatrix B) (cs : CoxeterSystem M W) : Prop

The exchange condition for a Coxeter system: if right multiplying a reduced word $\omega$ by $s_i$ decreases length, there is some index $i$ such that erasing the $i$-th letter from $\omega$ produces a word with product $\omega \cdot s$.

def Garrett.ExchangeDeletion.SatisfiesDeletionCondition {B : Type u_1} {W : Type u_2} [Group W] (M : CoxeterMatrix B) (cs : CoxeterSystem M W) : Prop

The deletion condition: if a word is non-reduced, two letters can be erased without changing its product. Formally, if $\mathtt{word.length} > \ell(\mathtt{wordProd}\,\mathtt{word})$ then there exist $i < j$ such that erasing positions $i$ and $j$ leaves the product unchanged.

def Garrett.ExchangeDeletion.ExchangeCorollary {B : Type u_1} {W : Type u_2} [Group W] (M : CoxeterMatrix B) (cs : CoxeterSystem M W) : Prop

Corollary of the exchange condition used in subexpression arguments: if both $\ell(sw) = \ell(w) + 1$ and $\ell(wt) = \ell(w) + 1$ hold, then either $\ell(swt) = \ell(w) + 2$ or $swt = w$.

theorem Garrett.ExchangeDeletion.exists_first_decreasing (f : ℕ → ℕ) (n : ℕ) (h0 : f 0 = 0) (hstep : ∀ j < n, f (j + 1) = f j + 1 ∨ f (j + 1) + 1 = f j) (hlt : n > f n) : ∃ j < n, f (j + 1) + 1 = f j ∧ ∀ k < j, f (k + 1) = f k + 1

Given a sequence $f : \mathbb{N} \to \mathbb{N}$ that starts at $0$ and at each step either increases or decreases by $1$, if $f(n) < n$ then there is a first index $j < n$ where $f$ decreases (i.e. $f(j+1) + 1 = f(j)$ and $f$ is strictly increasing on $[0, j]$).

theorem Garrett.ExchangeDeletion.deletion_of_exchange {B : Type u_2} {W : Type u_3} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (hex : SatisfiesExchangeCondition M cs) : SatisfiesDeletionCondition M cs

The exchange condition implies the deletion condition: any non-reduced word admits a pair of letters whose removal preserves its product.

theorem Garrett.ExchangeDeletion.corollary_of_exchange {B : Type u_2} {W : Type u_3} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (hex : SatisfiesExchangeCondition M cs) : ExchangeCorollary M cs

The exchange condition implies the exchange corollary: given an element $w$ with $\ell(sw) = \ell(wt) = \ell(w) + 1$, either $\ell(swt) = \ell(w) + 2$ or $swt = w$.