theorem CoxeterBruhat.exchange_length_analysis {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (v w : W) (i : B) (hcover : cs.length v + 1 = cs.length w) (hv_not_desc : ¬cs.IsRightDescent v i) (hw_desc : cs.IsRightDescent w i) : cs.length (w * cs.simple i) = cs.length v ∧ cs.length (v * cs.simple i) = cs.length w

In a Bruhat cover $v \lessdot w$ with $i$ a descent of $w$ but not of $v$: $\ell(ws_i) = \ell(v)$ and $\ell(vs_i) = \ell(w)$.

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

Abstract hypothesis that the reflection $t$ realizing a Bruhat cover $v \lessdot w = vt$ must equal a simple reflection $s_i$ when $i$ is a descent of $w$ but not of $v$.

• identify (v w t : W) : t ∈ reflections M cs → v * t = w → cs.length v + 1 = cs.length w → ∀ (i : B), ¬cs.IsRightDescent v i → cs.IsRightDescent w i → t = cs.simple i

theorem CoxeterBruhat.strong_exchange_of_reflection_id {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (hid : ReflectionIdentificationHyp cs) : StrongExchangeForBruhat cs

The reflection identification hypothesis implies the strong exchange condition for the Bruhat order.