Documentation

Mathlib.GroupTheory.Coxeter.Inversion

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=usiu1, where uW and si is a simple reflection. We say that a reflection t is a left inversion (CoxeterSystem.IsLeftInversion) of an element wW if (tw)<(w), and we say it is a right inversion (CoxeterSystem.IsRightInversion) of w if (wt)>(w). Here 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 #

References #

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

t : W is a reflection of the Coxeter system cs if it is of the form wsiw1, where wW and si is a simple reflection.

Equations
theorem CoxeterSystem.isReflection_simple {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i : B) :
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) :
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) :
def CoxeterSystem.IsRightInversion {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (w t : W) :

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

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

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

Equations
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} :
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} :
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} :
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} :
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} :
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} :
@[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) :
@[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) :
def CoxeterSystem.rightInvSeq {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (ω : List B) :

The right inversion sequence of ω. The right inversion sequence of a word si1si is the sequence sisi1si,,sisi1si2si1si,,sisi1si,si.

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

The left inversion sequence of ω. The left inversion sequence of a word si1si is the sequence si1,si1si2si1,si1si2si3si2si1,,si1sisi1.

Equations
@[simp]
theorem CoxeterSystem.rightInvSeq_nil {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) :
@[simp]
theorem CoxeterSystem.leftInvSeq_nil {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) :
@[simp]
theorem CoxeterSystem.rightInvSeq_singleton {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i : B) :
@[simp]
theorem CoxeterSystem.leftInvSeq_singleton {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i : B) :
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) :
theorem CoxeterSystem.leftInvSeq_reverse {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (ω : List B) :
@[simp]
theorem CoxeterSystem.length_rightInvSeq {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (ω : List B) :
@[simp]
theorem CoxeterSystem.length_leftInvSeq {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (ω : List B) :
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 : ) :
theorem CoxeterSystem.leftInvSeq_take {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (ω : List B) (j : ) :
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 ω) :
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 ω) :
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 ω) :
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 ω) :
theorem CoxeterSystem.prod_rightInvSeq {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (ω : List B) :
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 ω) :
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 ω) :
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 (alternatingWord i j (2 * p)))[k + 1] = (MulAut.conj (cs.simple i)) (cs.leftInvSeq (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 (alternatingWord i j (2 * p)))[k] = cs.wordProd (alternatingWord j i (2 * k + 1))