toLinearMapLieHom — Mathlib

English

There is a Lie algebra morphism from LieDerivation R L L to the space of linear endomorphisms of L, mapping a LieDerivation to its associated linear endomorphism.

Русский

Существует морфизм Ли-алгебр от LieDerivation R L L к пространству линейных однородных отображений L, переводящий Ли-производную к соответствующему линейному эндоморфизму.

LaTeX

$$$\text{toLinearMapLieHom } : \ LieDerivation R L L \to_\langle R \rangle L \to_\text{Lin}_R L L$$$

Lean4

/-- The Lie algebra morphism from Lie derivations into linear endormophisms. -/
def toLinearMapLieHom : LieDerivation R L L →ₗ⁅R⁆ L →ₗ[R] L
    where
  toFun := toLinearMap
  map_add' := by intro D1 D2; dsimp
  map_smul' := by intro D1 D2; dsimp
  map_lie' := by intro D1 D2; dsimp

Похожие утверждения