English
Let P and Q be root pairings with P.IsCrystallographic, P.IsReduced, P.IsIrreducible and IsAlgClosed K. Then the weight-space representation of endomorphisms induces an irreducible action on weight spaces; more precisely, the weight map provides an irreducible representation of the endomorphism monoid on the weight spaces.
Русский
Пусть P и Q — корневые пара pairings; P кристаллическая, редуцированная и неприводимая; K алгебраически замкнутое. Тогда весовой представления конецоморфизмов порождает неразложимое действие на весовых пространствах.
LaTeX
$$$\\text{IsIrreducible}(\\mathrm{lieAlgebra}(b), (b.\\mathrm{support}\\oplus ι)\\to K)$$$
Lean4
theorem weight_coweight_transpose_apply {ι₂ M₂ N₂ : Type*} [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂]
[Module R N₂] (P : RootPairing ι R M N) (Q : RootPairing ι₂ R M₂ N₂) (x : N₂) (f : Hom P Q) :
f.weightMap.dualMap (Q.flip.toPerfPair x) = P.flip.toPerfPair (f.coweightMap x) :=
Eq.mp (propext LinearMap.ext_iff) f.weight_coweight_transpose x
