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 = 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 #

References #

source
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⁻¹
Instances For
    source
    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)
    source
    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
    source
    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
    source
    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
    source
    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⁻¹
    source
    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)
    source
    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
    source
    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
    source
    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⁻¹)
    source
    @[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
    source
    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)
    Instances For
      source
      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)
      Instances For
        source
        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
        source
        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
        source
        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
        source
        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
        source
        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
        source
        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
        source
        @[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
        source
        @[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
        source
        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
        Instances For
          source
          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)
          Instances For
            source
            @[simp]
            theorem CoxeterSystem.rightInvSeq_nil {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) :
            cs.rightInvSeq [] = []
            source
            @[simp]
            theorem CoxeterSystem.leftInvSeq_nil {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) :
            cs.leftInvSeq [] = []
            source
            @[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]
            source
            @[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]
            source
            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)
            source
            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 ω)⁻¹)
            source
            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
            source
            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
            source
            @[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
            source
            @[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
            source
            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 (ω.get? j)).getD 1 * cs.wordProd (List.drop (j + 1) ω)
            source
            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 (ω.get? j)).getD 1 * (cs.wordProd (List.take j ω))⁻¹
            source
            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
            source
            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
            source
            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 ω)
            source
            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 ω)
            source
            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
            source
            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
            source
            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)
            source
            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)
            source
            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
            source
            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
            source
            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 ω)⁻¹
            source
            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 ω)⁻¹
            source
            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
            source
            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