English
Let P and Q be root pairings and e an equivalence between them. The weight map associated to e is invertible, and applying the inverse of the weight equivalence to the image of any m ∈ M under the weight map yields m itself. In particular, for every m ∈ M, (weightEquiv P Q e).symm (e.toHom.weightMap m) = m.
Русский
Пусть P и Q — пару корней, и e — эквивалент между ними. Весовое отображение, соответствующее e, имеет обратное отображение, и для каждого m ∈ M верно (weightEquiv P Q e).symm (e.toHom.weightMap m) = m.
LaTeX
$$$\forall m \in M,\;\bigl(\mathrm{weightEquiv}(P,Q,e)\bigr)^{-1}\Bigl( e.toHom.weightMap(m)\Bigr) = m$$$
Lean4
@[simp]
theorem weightEquiv_symm_weightMap (e : RootPairing.Equiv P Q) (m : M) :
(weightEquiv P Q e).symm (e.toHom.weightMap m) = m :=
(LinearEquiv.symm_apply_eq (weightEquiv P Q e)).mpr rfl
