map_lie₂ — Mathlib

English

Let f: M → N → P be a Lie module morphism with f m ∈ N → P for each m ∈ M. Then for all x ∈ L, m ∈ M, n ∈ N, we have [x, f m n] = f [x,m] n + f m [x,n].

Русский

Пусть f: M → (N → P) — морфизм Ли-модуля. Тогда для всех x ∈ L, m ∈ M, n ∈ N выполняется [x, f(m)(n)] = f([x,m])(n) + f(m)([x,n]).

LaTeX

$$$\forall x \in L, \forall m \in M, \forall n \in N,\ [x, f(m)(n)] = f([x,m])(n) + f(m)([x,n]).$$$

Lean4

theorem map_lie₂ (f : M →ₗ⁅R,L⁆ N →ₗ[R] P) (x : L) (m : M) (n : N) : ⁅x, f m n⁆ = f ⁅x, m⁆ n + f m ⁅x, n⁆ := by
  simp only [sub_add_cancel, map_lie, LieHom.lie_apply]

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