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

The set of reflections of a Coxeter system: all conjugates of simple generators, $T = \{w s_i w^{-1} \mid w \in W,\ i \in B\}$.

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

A single Bruhat step $v \to w$: there exists a reflection $t$ such that $v t = w$ and $\ell(v) < \ell(w)$.

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

The Bruhat order $v \le w$, defined as the reflexive-transitive closure of $\mathtt{BruhatStep}$.

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

The standard parabolic subgroup $W_J$ generated by the simple reflections indexed by $J \subseteq B$.

theorem CoxeterBruhat.simple_sq {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i : B) : cs.simple i * cs.simple i = 1

Simple reflections are involutions: $s_i \cdot s_i = 1$.

theorem CoxeterBruhat.simple_inv {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i : B) : (cs.simple i)⁻¹ = cs.simple i

Simple reflections are self-inverse: $s_i^{-1} = s_i$.

theorem CoxeterBruhat.reflection_sq {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {t : W} (ht : t ∈ reflections M cs) : t * t = 1

Every reflection $t$ is an involution: $t \cdot t = 1$.

theorem CoxeterBruhat.reflection_inv {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {t : W} (ht : t ∈ reflections M cs) : t⁻¹ = t

Every reflection is self-inverse: $t^{-1} = t$.

theorem CoxeterBruhat.simple_mem_reflections {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i : B) : cs.simple i ∈ reflections M cs

Each simple reflection $s_i$ is itself a reflection in the set $T$.

theorem CoxeterBruhat.simple_conj_reflection {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {t : W} (ht : t ∈ reflections M cs) (i : B) : cs.simple i * t * cs.simple i ∈ reflections M cs

Reflections are closed under conjugation by simple reflections: if $t \in T$ then $s_i\, t\, s_i \in T$.

theorem CoxeterBruhat.mul_simple_conj_eq {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {v w t : W} (hvw : v * t = w) (i : B) : v * cs.simple i * (cs.simple i * t * cs.simple i) = w * cs.simple i

Algebraic identity used in the lifting lemma: if $v t = w$ then $(v s_i)(s_i t s_i) = w s_i$.

theorem CoxeterBruhat.mul_reflection_reverse {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {a b t : W} (ht : t ∈ reflections M cs) (h : a * t = b) : b * t = a

Multiplication by a reflection is reversible: if $a t = b$ for a reflection $t$, then $b t = a$.

theorem CoxeterBruhat.reflection_length_odd {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {t : W} (ht : t ∈ reflections M cs) : cs.length t % 2 = 1

Every reflection has odd length.

theorem CoxeterBruhat.length_parity_ne_of_mul_reflection {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {v w t : W} (ht : t ∈ reflections M cs) (hvw : v * t = w) : cs.length v % 2 ≠ cs.length w % 2

Multiplying by a reflection flips the parity of the length: if $v t = w$ and $t \in T$, then $\ell(v)$ and $\ell(w)$ have opposite parities.

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

A Bruhat step strictly increases length: if $v \to w$ then $\ell(v) < \ell(w)$.

theorem CoxeterBruhat.bruhatLE_length_le {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {v w : W} (h : BruhatLE cs v w) : cs.length v ≤ cs.length w

The Bruhat order is compatible with length: $v \le w$ implies $\ell(v) \le \ell(w)$.

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

Reflexivity of the Bruhat order.

theorem CoxeterBruhat.bruhatLE_trans {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {u v w : W} (h1 : BruhatLE cs u v) (h2 : BruhatLE cs v w) : BruhatLE cs u w

Transitivity of the Bruhat order.

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

A single Bruhat step witnesses the Bruhat-order inequality.

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

A right descent gives a Bruhat step: if $\ell(v s_i) < \ell(v)$ then $v s_i \to v$ is a Bruhat step.

theorem CoxeterBruhat.bruhatLE_eq_of_length_eq {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {v w : W} (h : BruhatLE cs v w) (hlen : cs.length v = cs.length w) : v = w

Antisymmetry via length: if $v \le w$ and $\ell(v) = \ell(w)$, then $v = w$.

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

The Strong Exchange Condition specialised to Bruhat covers: when $v < w$ is a Bruhat cover via a reflection $t$ (i.e. $vt = w$ and $\ell(v)+1 = \ell(w)$) and $i$ is a right descent of $w$ but not of $v$, then $v s_i = w$.

theorem CoxeterBruhat.bruhat_lifting_lemma {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (hSEC : StrongExchangeForBruhat cs) {v w : W} (t : W) (ht : t ∈ reflections M cs) (hvt : v * t = w) (hcover : cs.length v + 1 = cs.length w) (i : B) (hv_up : ¬cs.IsRightDescent v i) (hne : v * cs.simple i ≠ w) : ¬cs.IsRightDescent w i ∧ BruhatStep cs (v * cs.simple i) (w * cs.simple i)

Bruhat lifting lemma: given a Bruhat cover $v \to w$ via a reflection $t$, if $i$ is not a right descent of $v$ and $v s_i \ne w$, then $i$ is not a right descent of $w$ either, and $v s_i \to w s_i$ is a Bruhat step.

theorem CoxeterBruhat.bruhatStep_right_mul {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (hSEC : StrongExchangeForBruhat cs) {v w : W} (hvw : BruhatStep cs v w) (i : B) : BruhatLE cs (v * cs.simple i) w ∨ BruhatLE cs (v * cs.simple i) (w * cs.simple i)

Right multiplication by a simple reflection on a Bruhat step: from $v \to w$ one obtains either $v s_i \le w$ or $v s_i \le w s_i$ in the Bruhat order.

theorem CoxeterBruhat.bruhat_right_mul {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (hSEC : StrongExchangeForBruhat cs) {v w : W} (hvw : BruhatLE cs v w) (i : B) : BruhatLE cs (v * cs.simple i) w ∨ BruhatLE cs (v * cs.simple i) (w * cs.simple i)

Right multiplication compatibility with the Bruhat order: if $v \le w$ then either $v s_i \le w$ or $v s_i \le w s_i$.