inner — Mathlib

English

There is a natural linear map inner: M →ₗ[R] LieDerivation R L M sending an element m ∈ M to the derivation ad_m defined by ad_m(x) = [m, x].

Русский

Существует естественная линейная карта inner: M →ₗ[R] LieDerivation R L M, отправляющая m ∈ M в вывод derivation ad_m, заданный как ad_m(x) = [m, x].

LaTeX

$$inner : M →ₗ[R] LieDerivation R L M$$

Lean4

/-- The natural map from a Lie module to the derivations taking values in it. -/
@[simps!]
def inner : M →ₗ[R] LieDerivation R L M
    where
  toFun
    m :=
    { __ := (LieModule.toEnd R L M : L →ₗ[R] Module.End R M).flip m
      leibniz' := by simp }
  map_add' m n := by ext; simp
  map_smul' t m := by ext; simp

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