Coxeter.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

Signed reflection permutations and strong exchange for arbitrary Coxeter systems.

def OAI.KLInvariance.CoxeterSupport.simpleAction line 22
theorem OAI.KLInvariance.CoxeterSupport.simpleAction_apply line 44
def OAI.KLInvariance.CoxeterSupport.wordAction line 50
theorem OAI.KLInvariance.CoxeterSupport.wordAction_nil line 53
theorem OAI.KLInvariance.CoxeterSupport.wordAction_concat line 55
theorem OAI.KLInvariance.CoxeterSupport.wordAction_record line 60
Source documentation
Signed action records the parity of the genuine left inversion sequence.
```
theorem wordAction_record (ω : List B) (t : W) (a : ZMod 2) :
    wordAction cs ω ((cs.wordProd ω)⁻¹ * t * cs.wordProd ω, a) =
      (t, a + ((cs.leftInvSeq ω).count t : ZMod 2)) := by
…
```
Mentions: OAI.KLInvariance.CoxeterSupport.wordAction
theorem OAI.KLInvariance.CoxeterSupport.leftInvSeq_alternating_formula line 92
Source documentation
The presentation relation has a doubled inversion sequence, so its signed action is trivial, including for no-relation entries M i j = 0.
```
theorem leftInvSeq_alternating_formula (i j : B) (p : ℕ) :
    cs.leftInvSeq (alternatingWord i j (2 * p)) =
      (List.range (2 * p)).map (fun k => cs.simple i * (cs.simple j * cs.simple i) ^ k) := by
…
```
theorem OAI.KLInvariance.CoxeterSupport.leftInvSeq_relation_doubled line 106
theorem OAI.KLInvariance.CoxeterSupport.wordAction_alternating line 118
theorem OAI.KLInvariance.CoxeterSupport.simpleAction_liftable line 132
def OAI.KLInvariance.CoxeterSupport.reflectionAction line 144
theorem OAI.KLInvariance.CoxeterSupport.reflectionAction_simple line 147
theorem OAI.KLInvariance.CoxeterSupport.reflectionAction_wordProd line 151
theorem OAI.KLInvariance.CoxeterSupport.reflectionAction_translation line 160
Source documentation
The signed action is conjugation on labels and a translation on signs.
```
theorem reflectionAction_translation (w t : W) :
    ∃ δ : ZMod 2, ∀ a : ZMod 2,
      reflectionAction cs w (t, a) = (w * t * w⁻¹, a + δ) := by
…
```
Mentions: OAI.KLInvariance.CoxeterSupport.reflectionAction
theorem OAI.KLInvariance.CoxeterSupport.reflectionAction_reflection line 173
Source documentation
A reflection changes the sign of its own label. This is the critical conjugation step making the representation yield strong exchange.
```
theorem reflectionAction_reflection {t : W} (ht : cs.IsReflection t) (a : ZMod 2) :
    reflectionAction cs t (t, a) = (t, a + 1) := by
…
```
Mentions: OAI.KLInvariance.CoxeterSupport.reflectionAction
theorem OAI.KLInvariance.CoxeterSupport.mem_leftInvSeq_of_inversion line 199

theorem OAI.KLInvariance.CoxeterSupport.strong_exchange line 228

Source documentation

Full strong exchange, with the deletion index in the supplied reduced word.

theorem strong_exchange {ω : List B} (hω : cs.IsReduced ω) {t : W}
    (ht : cs.IsLeftInversion (cs.wordProd ω) t) :
    ∃ j : ℕ, j < ω.length ∧ t * cs.wordProd ω = cs.wordProd (ω.eraseIdx j) := by
…