English
There is a contravariant linear equivalence between the coweight spaces given an equivalence between root pairings. Specifically, coweightEquiv (P : RootPairing ι R M N) (Q : RootPairing ι₂ R M₂ N₂) (e : P.Equiv Q) provides an R-linear isomorphism N₂ ≃ₗ[N] N.
Русский
Существует противоположное (контравариантное) линейное эквивалентное отображение между пространствами ковалентов весов, задаваемое эквивалентностью между парными корнями: coweightEquiv (P) (Q) (e) задаёт линейное изоморфизм между N₂ и N.
LaTeX
$$$\mathrm{coweightEquiv}(P,Q,e) : N_2 \cong_R N = \mathrm{LinearEquiv.ofBijective} \bigl( e.bijective\_coweightMap \bigr)$$$
Lean4
/-- The contravariant equivalence of coweight spaces given by an equivalence of root pairings. -/
def coweightEquiv (e : RootPairing.Equiv P Q) : N₂ ≃ₗ[R] N :=
LinearEquiv.ofBijective _ e.bijective_coweightMap
