English
The construction coweightHom provides a monoid hom from End P to the opposite of linear endomorphisms, capturing dual weight data.
Русский
Построение coweightHom задаёт гомоморфизм моноида от End P в противоположное множество линейных эндоморфизмов, фиксируя двойственные весовые данные.
LaTeX
$$coweightHom : End P →* (Module.End R M)ᵐᵒᵖ$$
Lean4
/-- The coweight space representation of endomorphisms -/
def coweightHom (P : RootPairing ι R M N) : End P →* (N →ₗ[R] N)ᵐᵒᵖ
where
toFun g := MulOpposite.op (Hom.coweightMap (P := P) (Q := P) g)
map_mul' g h := by simp only [← MulOpposite.op_mul, coweightMap_mul, Module.End.mul_eq_comp]
map_one' := by simp only [MulOpposite.op_eq_one_iff, coweightMap_one, Module.End.one_eq_id]
