English
Let k be a commutative ring, G a group, and V a k-vector space with a G-action ρ. Then the additive isomorphism unitIsoAddEquiv between V and the module obtained from V via the monoid algebra of G intertwines the G-action with the induced monoid-algebra action; i.e., for all g in G and x in V, the action of g on x transported by the isomorphism equals the monoid-algebra action of g on the transported element.
Русский
Пусть k — коммутативное кольцо, G — группа, V — пространтво над k с действием G, задаваемым ρ. Тогда аддитивное изоморождение unitIsoAddEquiv между V и модулем, полученным из V над моноидальной алгеброй, взаимно приводят действия G и алгебраического модуля: для любого g∈G и x∈V выполняется intertwine-условие междуρ(g) и соответствующим действием через моноидальную алгебру.
LaTeX
$$$\\forall g \\in G, \\forall x \\in V:\\ unitIsoAddEquiv( (V.\\rho\\, g).toFun\\, x ) = (\\, (ofModuleMonoidAlgebra.obj (toModuleMonoidAlgebra.obj V)).\\rho\\, g).toFun (unitIsoAddEquiv\\, x).$$$
Lean4
theorem unit_iso_comm (V : Rep k G) (g : G) (x : V) :
unitIsoAddEquiv ((V.ρ g).toFun x) =
((ofModuleMonoidAlgebra.obj (toModuleMonoidAlgebra.obj V)).ρ g).toFun (unitIsoAddEquiv x) :=
by simp [unitIsoAddEquiv, ofModuleMonoidAlgebra, toModuleMonoidAlgebra]
