English
There is a left action of the opposite automorphism group on the module N, defined by w · x := (unop (coweightHom P (unop w))) x for w in Autᵐᵒᵖ and x in N; this action satisfies the usual axioms of a distributive linear action.
Русский
Существует левое действие группы противоположных автоморфизмов на модуле N, заданное формулой w · x := (unop (coweightHom P (unop w))) x для w ∈ Autᵐᵒᵖ и x ∈ N; это действие удовлетворяет обычным аксиомам распределимого линейного действия.
LaTeX
$$$$ w \cdot x = (\mathrm{unop}\circ \mathrm{coweightHom}_P(\mathrm{unop}(w)))(x) \,. $$$$
Lean4
instance : DistribMulAction P.Autᵐᵒᵖ N
where
smul w x := unop (coweightHom P (unop w)) x
one_smul _ := rfl
mul_smul _ _ _ := rfl
smul_zero w := show unop (coweightHom P (unop w)) 0 = 0 by simp
smul_add w x
y := by
change unop (coweightHom P _) (x + y) = unop (coweightHom P _) x + unop (coweightHom P _) y
simp
