English
In the alternatingWord setting, expressions for elements of leftInvSeq are obtained by conjugating corresponding elements by simple reflections.
Русский
В конфигурации alternatingWord выражения элементов leftInvSeq получают путём сопряжения соответствующих элементов простыми отражениями.
LaTeX
$$$\text{(see above)}$$$
Lean4
theorem getElem_leftInvSeq_alternatingWord (i j : B) (p k : ℕ) (h : k < 2 * p) :
(lis(alternatingWord i j (2 * p)))[k]'(by simp; cutsat) = π alternatingWord j i (2 * k + 1) := by
induction k generalizing i j with
|
zero =>
simp only [CoxeterSystem.getElem_leftInvSeq cs (alternatingWord i j (2 * p)) 0 (by simp [h]), take_zero,
wordProd_nil, one_mul, inv_one, mul_one, alternatingWord, concat_eq_append, nil_append, wordProd_singleton]
apply congr_arg
simp only [getElem_alternatingWord i j (2 * p) 0 (by simp [h]), add_zero, even_two, Even.mul_right, ↓reduceIte]
| succ k
hk =>
simp only [getElem_succ_leftInvSeq_alternatingWord cs i j p k h, hk _ _ (by cutsat), MulAut.conj_apply, inv_simple,
alternatingWord_succ' j i, even_two, Even.mul_right, ↓reduceIte, wordProd_cons]
rw [(by ring : 2 * (k + 1) = 2 * k + 1 + 1), alternatingWord_succ j i, wordProd_concat]
simp [mul_assoc]
