English
Let e be an equivalence between root pairings P and Q. Then the weight map on M₂, after applying the inverse weight equivalence, returns the original element m ∈ M₂. In symbols, e.toHom.weightMap ((weightEquiv P Q e).symm m) = m for all m ∈ M₂.
Русский
Пусть e — эквивалент между парами корней P и Q. Тогда весовое отображение на M₂ после применения обратного весового эквививалента возвращает исходный элемент m ∈ M₂: e.toHom.weightMap ((weightEquiv P Q e).symm m) = m для всех m ∈ M₂.
LaTeX
$$$\forall m \in M_2,\; e.toHom.weightMap\bigl((\mathrm{weightEquiv}(P,Q,e).symm)\,m\bigr) = m$$$
Lean4
@[simp]
theorem weightMap_weightEquiv_symm (e : RootPairing.Equiv P Q) (m : M₂) :
e.toHom.weightMap ((weightEquiv P Q e).symm m) = m :=
by
rw [← weightEquiv_apply]
exact LinearEquiv.apply_symm_apply (weightEquiv P Q e) m
