Reflections, inversions, and inversion sequences

Throughout this file, B is a type and M : CoxeterMatrix B is a Coxeter matrix. cs : CoxeterSystem M W is a Coxeter system; that is, W is a group, and cs holds the data of a group isomorphism W ≃* M.group, where M.group refers to the quotient of the free group on B by the Coxeter relations given by the matrix M. See Mathlib/GroupTheory/Coxeter/Basic.lean for more details.

We define a reflection (CoxeterSystem.IsReflection) to be an element of the form $t = u s_i u^{-1}$, where $u \in W$ and $s_i$ is a simple reflection. We say that a reflection $t$ is a left inversion (CoxeterSystem.IsLeftInversion) of an element $w \in W$ if $\ell(t w) < \ell(w)$, and we say it is a right inversion (CoxeterSystem.IsRightInversion) of $w$ if $\ell(w t) > \ell(w)$. Here $\ell$ is the length function (see Mathlib/GroupTheory/Coxeter/Length.lean).

Given a word, we define its left inversion sequence (CoxeterSystem.leftInvSeq) and its right inversion sequence (CoxeterSystem.rightInvSeq). We prove that if a word is reduced, then both of its inversion sequences contain no duplicates. In fact, the right (respectively, left) inversion sequence of a reduced word for $w$ consists of all of the right (respectively, left) inversions of $w$ in some order, but we do not prove that in this file.

Main definitions

• CoxeterSystem.IsReflection
• CoxeterSystem.IsLeftInversion
• CoxeterSystem.IsRightInversion
• CoxeterSystem.leftInvSeq
• CoxeterSystem.rightInvSeq

References

• A. Björner and F. Brenti, Combinatorics of Coxeter Groups

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

t : W is a reflection of the Coxeter system cs if it is of the form $w s_i w^{-1}$, where $w \in W$ and $s_i$ is a simple reflection.

Equations

• cs.IsReflection t = ∃ (w : W) (i : B), t = w * cs.simple i * w⁻¹

theorem CoxeterSystem.isReflection_simple {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i : B) : cs.IsReflection (cs.simple i)

theorem CoxeterSystem.IsReflection.pow_two {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} {cs : CoxeterSystem M W} {t : W} (ht : cs.IsReflection t) : t ^ 2 = 1

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

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

theorem CoxeterSystem.IsReflection.isReflection_inv {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} {cs : CoxeterSystem M W} {t : W} (ht : cs.IsReflection t) : cs.IsReflection t⁻¹

theorem CoxeterSystem.IsReflection.odd_length {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} {cs : CoxeterSystem M W} {t : W} (ht : cs.IsReflection t) : Odd (cs.length t)

theorem CoxeterSystem.IsReflection.length_mul_left_ne {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} {cs : CoxeterSystem M W} {t : W} (ht : cs.IsReflection t) (w : W) : cs.length (w * t) ≠ cs.length w

theorem CoxeterSystem.IsReflection.length_mul_right_ne {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} {cs : CoxeterSystem M W} {t : W} (ht : cs.IsReflection t) (w : W) : cs.length (t * w) ≠ cs.length w

theorem CoxeterSystem.IsReflection.conj {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} {cs : CoxeterSystem M W} {t : W} (ht : cs.IsReflection t) (w : W) : cs.IsReflection (w * t * w⁻¹)

@[simp]

theorem CoxeterSystem.isReflection_conj_iff {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (w t : W) : cs.IsReflection (w * t * w⁻¹) ↔ cs.IsReflection t

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

The proposition that t is a right inversion of w; i.e., t is a reflection and $\ell (w t) < \ell(w)$.

Equations

• cs.IsRightInversion w t = (cs.IsReflection t ∧ cs.length (w * t) < cs.length w)

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

The proposition that t is a left inversion of w; i.e., t is a reflection and $\ell (t w) < \ell(w)$.

Equations

• cs.IsLeftInversion w t = (cs.IsReflection t ∧ cs.length (t * w) < cs.length w)

theorem CoxeterSystem.isRightInversion_inv_iff {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {w t : W} : cs.IsRightInversion w⁻¹ t ↔ cs.IsLeftInversion w t

theorem CoxeterSystem.isLeftInversion_inv_iff {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {w t : W} : cs.IsLeftInversion w⁻¹ t ↔ cs.IsRightInversion w t

theorem CoxeterSystem.IsReflection.isRightInversion_mul_left_iff {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} {cs : CoxeterSystem M W} {t : W} (ht : cs.IsReflection t) {w : W} : cs.IsRightInversion (w * t) t ↔ ¬cs.IsRightInversion w t

theorem CoxeterSystem.IsReflection.not_isRightInversion_mul_left_iff {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} {cs : CoxeterSystem M W} {t : W} (ht : cs.IsReflection t) {w : W} : ¬cs.IsRightInversion (w * t) t ↔ cs.IsRightInversion w t

theorem CoxeterSystem.IsReflection.isLeftInversion_mul_right_iff {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} {cs : CoxeterSystem M W} {t : W} (ht : cs.IsReflection t) {w : W} : cs.IsLeftInversion (t * w) t ↔ ¬cs.IsLeftInversion w t

theorem CoxeterSystem.IsReflection.not_isLeftInversion_mul_right_iff {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} {cs : CoxeterSystem M W} {t : W} (ht : cs.IsReflection t) {w : W} : ¬cs.IsLeftInversion (t * w) t ↔ cs.IsLeftInversion w t

@[simp]

theorem CoxeterSystem.isRightInversion_simple_iff_isRightDescent {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (w : W) (i : B) : cs.IsRightInversion w (cs.simple i) ↔ cs.IsRightDescent w i

@[simp]

theorem CoxeterSystem.isLeftInversion_simple_iff_isLeftDescent {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (w : W) (i : B) : cs.IsLeftInversion w (cs.simple i) ↔ cs.IsLeftDescent w i

def CoxeterSystem.rightInvSeq {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (ω : List B) : List W

The right inversion sequence of ω. The right inversion sequence of a word $s_{i_1} \cdots s_{i_\ell}$ is the sequence $$s_{i_\ell}\cdots s_{i_1}\cdots s_{i_\ell}, \ldots, s_{i_{\ell}}s_{i_{\ell - 1}}s_{i_{\ell - 2}}s_{i_{\ell - 1}}s_{i_\ell}, \ldots, s_{i_{\ell}}s_{i_{\ell - 1}}s_{i_\ell}, s_{i_\ell}.$$

Equations

• cs.rightInvSeq [] = []
• cs.rightInvSeq (i :: ω_2) = (cs.wordProd ω_2)⁻¹ * cs.simple i * cs.wordProd ω_2 :: cs.rightInvSeq ω_2

def CoxeterSystem.leftInvSeq {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (ω : List B) : List W

The left inversion sequence of ω. The left inversion sequence of a word $s_{i_1} \cdots s_{i_\ell}$ is the sequence $$s_{i_1}, s_{i_1}s_{i_2}s_{i_1}, s_{i_1}s_{i_2}s_{i_3}s_{i_2}s_{i_1}, \ldots, s_{i_1}\cdots s_{i_\ell}\cdots s_{i_1}.$$

Equations

• cs.leftInvSeq [] = []
• cs.leftInvSeq (i :: ω_2) = cs.simple i :: List.map (⇑(MulAut.conj (cs.simple i))) (cs.leftInvSeq ω_2)

@[simp]

theorem CoxeterSystem.rightInvSeq_nil {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) : cs.rightInvSeq [] = []

@[simp]

theorem CoxeterSystem.leftInvSeq_nil {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) : cs.leftInvSeq [] = []

@[simp]

theorem CoxeterSystem.rightInvSeq_singleton {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i : B) : cs.rightInvSeq [i] = [cs.simple i]

@[simp]

theorem CoxeterSystem.leftInvSeq_singleton {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i : B) : cs.leftInvSeq [i] = [cs.simple i]

theorem CoxeterSystem.rightInvSeq_concat {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (ω : List B) (i : B) : cs.rightInvSeq (ω.concat i) = (List.map (⇑(MulAut.conj (cs.simple i))) (cs.rightInvSeq ω)).concat (cs.simple i)

theorem CoxeterSystem.leftInvSeq_concat {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (ω : List B) (i : B) : cs.leftInvSeq (ω.concat i) = (cs.leftInvSeq ω).concat (cs.wordProd ω * cs.simple i * (cs.wordProd ω)⁻¹)

theorem CoxeterSystem.rightInvSeq_reverse {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (ω : List B) : cs.rightInvSeq ω.reverse = (cs.leftInvSeq ω).reverse

theorem CoxeterSystem.leftInvSeq_reverse {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (ω : List B) : cs.leftInvSeq ω.reverse = (cs.rightInvSeq ω).reverse

@[simp]

theorem CoxeterSystem.length_rightInvSeq {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (ω : List B) : (cs.rightInvSeq ω).length = ω.length

@[simp]

theorem CoxeterSystem.length_leftInvSeq {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (ω : List B) : (cs.leftInvSeq ω).length = ω.length

theorem CoxeterSystem.getD_rightInvSeq {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (ω : List B) (j : ℕ) : (cs.rightInvSeq ω).getD j 1 = (cs.wordProd (List.drop (j + 1) ω))⁻¹ * (Option.map cs.simple ω[j]?).getD 1 * cs.wordProd (List.drop (j + 1) ω)

theorem CoxeterSystem.getElem_rightInvSeq {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (ω : List B) (j : ℕ) (h : j < ω.length) : (cs.rightInvSeq ω)[j] = (cs.wordProd (List.drop (j + 1) ω))⁻¹ * (Option.map cs.simple ω[j]?).getD 1 * cs.wordProd (List.drop (j + 1) ω)

theorem CoxeterSystem.getD_leftInvSeq {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (ω : List B) (j : ℕ) : (cs.leftInvSeq ω).getD j 1 = cs.wordProd (List.take j ω) * (Option.map cs.simple ω[j]?).getD 1 * (cs.wordProd (List.take j ω))⁻¹

theorem CoxeterSystem.getElem_leftInvSeq {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (ω : List B) (j : ℕ) (h : j < ω.length) : (cs.leftInvSeq ω)[j] = cs.wordProd (List.take j ω) * cs.simple ω[j] * (cs.wordProd (List.take j ω))⁻¹

theorem CoxeterSystem.getD_rightInvSeq_mul_self {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (ω : List B) (j : ℕ) : (cs.rightInvSeq ω).getD j 1 * (cs.rightInvSeq ω).getD j 1 = 1

theorem CoxeterSystem.getD_leftInvSeq_mul_self {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (ω : List B) (j : ℕ) : (cs.leftInvSeq ω).getD j 1 * (cs.leftInvSeq ω).getD j 1 = 1

theorem CoxeterSystem.rightInvSeq_drop {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (ω : List B) (j : ℕ) : cs.rightInvSeq (List.drop j ω) = List.drop j (cs.rightInvSeq ω)

theorem CoxeterSystem.leftInvSeq_take {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (ω : List B) (j : ℕ) : cs.leftInvSeq (List.take j ω) = List.take j (cs.leftInvSeq ω)

theorem CoxeterSystem.isReflection_of_mem_rightInvSeq {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (ω : List B) {t : W} (ht : t ∈ cs.rightInvSeq ω) : cs.IsReflection t

theorem CoxeterSystem.isReflection_of_mem_leftInvSeq {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (ω : List B) {t : W} (ht : t ∈ cs.leftInvSeq ω) : cs.IsReflection t

theorem CoxeterSystem.wordProd_mul_getD_rightInvSeq {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (ω : List B) (j : ℕ) : cs.wordProd ω * (cs.rightInvSeq ω).getD j 1 = cs.wordProd (ω.eraseIdx j)

theorem CoxeterSystem.getD_leftInvSeq_mul_wordProd {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (ω : List B) (j : ℕ) : (cs.leftInvSeq ω).getD j 1 * cs.wordProd ω = cs.wordProd (ω.eraseIdx j)

theorem CoxeterSystem.isRightInversion_of_mem_rightInvSeq {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {ω : List B} (hω : cs.IsReduced ω) {t : W} (ht : t ∈ cs.rightInvSeq ω) : cs.IsRightInversion (cs.wordProd ω) t

theorem CoxeterSystem.isLeftInversion_of_mem_leftInvSeq {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {ω : List B} (hω : cs.IsReduced ω) {t : W} (ht : t ∈ cs.leftInvSeq ω) : cs.IsLeftInversion (cs.wordProd ω) t

theorem CoxeterSystem.prod_rightInvSeq {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (ω : List B) : (cs.rightInvSeq ω).prod = (cs.wordProd ω)⁻¹

theorem CoxeterSystem.prod_leftInvSeq {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (ω : List B) : (cs.leftInvSeq ω).prod = (cs.wordProd ω)⁻¹

theorem CoxeterSystem.IsReduced.nodup_rightInvSeq {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {ω : List B} (rω : cs.IsReduced ω) : (cs.rightInvSeq ω).Nodup

theorem CoxeterSystem.IsReduced.nodup_leftInvSeq {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {ω : List B} (rω : cs.IsReduced ω) : (cs.leftInvSeq ω).Nodup

theorem CoxeterSystem.getElem_succ_leftInvSeq_alternatingWord {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i j : B) (p k : ℕ) (h : k + 1 < 2 * p) : (cs.leftInvSeq (CoxeterSystem.alternatingWord i j (2 * p)))[k + 1] = (MulAut.conj (cs.simple i)) (cs.leftInvSeq (CoxeterSystem.alternatingWord j i (2 * p)))[k]

theorem CoxeterSystem.getElem_leftInvSeq_alternatingWord {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i j : B) (p k : ℕ) (h : k < 2 * p) : (cs.leftInvSeq (CoxeterSystem.alternatingWord i j (2 * p)))[k] = cs.wordProd (CoxeterSystem.alternatingWord j i (2 * k + 1))