English
Let P be a RootPairing. If the reflection permutation at indices i and j are equal, then the corresponding reflections are equal after doubling, i.e. 2·reflection_i = 2·reflection_j as linear endomorphisms.
Русский
Пусть P — корневое сочетание. Если отражения под индексами i и j совпадают по перестановке отражений, то сами отражения совпадают после умножения на 2: 2·-reflection_i = 2·reflection_j в виде линейных отображений.
LaTeX
$$$$ 2\\cdot \\bigl( \\mathrm{reflection}_i \\bigr) \\\\ = \\\\ 2\\cdot \\bigl( \\mathrm{reflection}_j \\bigr). $$$$
Lean4
theorem two_nsmul_reflection_eq_of_perm_eq (hij : P.reflectionPerm i = P.reflectionPerm j) :
2 • ⇑(P.reflection i) = 2 • P.reflection j := by
ext x
suffices 2 • P.toLinearMap x (P.coroot i) • P.root i = 2 • P.toLinearMap x (P.coroot j) • P.root j by
simpa [reflection_apply, smul_sub]
calc
2 • P.toLinearMap x (P.coroot i) • P.root i = P.toLinearMap x (P.coroot i) • ((2 : R) • P.root i) := ?_
_ = P.toLinearMap x (P.coroot i) • (P.pairing i j • P.root j) := ?_
_ = P.toLinearMap x (P.pairing i j • P.coroot i) • (P.root j) := ?_
_ = P.toLinearMap x ((2 : R) • P.coroot j) • (P.root j) := ?_
_ = 2 • P.toLinearMap x (P.coroot j) • P.root j := ?_
· rw [smul_comm, ← Nat.cast_smul_eq_nsmul R, Nat.cast_ofNat]
· rw [P.pairing_smul_root_eq j i i hij.symm, pairing_same]
· rw [← smul_comm, ← smul_assoc, map_smul]
· rw [← P.pairing_smul_coroot_eq j i j hij.symm, pairing_same]
· rw [map_smul, smul_assoc, ← Nat.cast_smul_eq_nsmul R, Nat.cast_ofNat]
