English
Let f: M →ₗ⁅R,L⁆ P and g: N →ₗ⁅R,L⁆ Q be Lie-module morphisms. Then there is an induced Lie-module morphism map f g: M ⊗R N →ₗ⁅R,L⁆ P ⊗R Q given by applying f and g to the respective factors, i.e., map f g(m ⊗ n) = f m ⊗ g n, and this construction preserves the Lie-module structure.
Русский
Пусть f: M →ₗ⁅R,L⁆ P и g: N →ₗ⁅R,L⁆ Q — морфизмы Ли-модулей. Тогда существует индуцированный морфизм Ли-модулей map f g: M ⊗R N →ₗ⁅R,L⁆ P ⊗R Q, который действует на тензор простым образом: map f g(m ⊗ n) = f m ⊗ g n, и сохраняет структуру Ли-модуля.
LaTeX
$$$$\text{map } f g : M \otimes_R N \to P \otimes_R Q\quad \text{is a Lie-module morphism with} \quad (m,n) \mapsto f(m) \otimes g(n).$$$$
Lean4
/-- A pair of Lie module morphisms `f : M → P` and `g : N → Q`, induce a Lie module morphism:
`M ⊗ N → P ⊗ Q`. -/
nonrec def map (f : M →ₗ⁅R,L⁆ P) (g : N →ₗ⁅R,L⁆ Q) : M ⊗[R] N →ₗ⁅R,L⁆ P ⊗[R] Q :=
{ map (f : M →ₗ[R] P) (g : N →ₗ[R] Q) with
map_lie' := fun {x t} => by
simp only [LinearMap.toFun_eq_coe]
refine t.induction_on ?_ ?_ ?_
· simp only [LinearMap.map_zero, lie_zero]
· intro m n
simp only [LieModuleHom.coe_toLinearMap, lie_tmul_right, LieModuleHom.map_lie, map_tmul, LinearMap.map_add]
· intro t₁ t₂ ht₁ ht₂; simp only [ht₁, ht₂, lie_add, LinearMap.map_add] }
