English
The map toModuleHom provides a Lie-module morphism L ⊗R M →ₗ⁅R,L⁆ M, i.e., the action of the Lie algebra on its module realized as a morphism of Lie modules.
Русский
Map toModuleHom задаёт морфизм Ли-модуля L ⊗R M →ₗ⁅R,L⁆ M, реализуя действие Ли на модуле как морфизм Ли-модулей.
LaTeX
$$$$ toModuleHom: L \otimes_R M \to M $$ in the Lie-module sense.$$
Lean4
/-- The trace form of a Lie module is compatible with the action of the Lie algebra.
See also `LieModule.traceForm_apply_lie_apply'`. -/
theorem traceForm_apply_lie_apply (x y z : L) : traceForm R L M ⁅x, y⁆ z = traceForm R L M x ⁅y, z⁆ :=
by
calc
traceForm R L M ⁅x, y⁆ z = trace R _ (φ ⁅x, y⁆ ∘ₗ φ z) := by simp only [traceForm_apply_apply]
_ = trace R _ ((φ x * φ y - φ y * φ x) * φ z) := ?_
_ = trace R _ (φ x * (φ y * φ z)) - trace R _ (φ y * (φ x * φ z)) := ?_
_ = trace R _ (φ x * (φ y * φ z)) - trace R _ (φ x * (φ z * φ y)) := ?_
_ = traceForm R L M x ⁅y, z⁆ := ?_
· simp only [LieHom.map_lie, Ring.lie_def, ← Module.End.mul_eq_comp]
· simp only [sub_mul, map_sub, mul_assoc]
· simp only [LinearMap.trace_mul_cycle' R (φ x) (φ z) (φ y)]
· simp only [traceForm_apply_apply, LieHom.map_lie, Ring.lie_def, mul_sub, map_sub, ← Module.End.mul_eq_comp]
