toLinearMap_map — Mathlib

English

Let f: M →ₗ⁅R,L⁆ P and g: N →ₗ⁅R,L⁆ Q be Lie-module morphisms. The linear map underlying the Lie-tensor map map f g is precisely the standard tensor product map TensorProduct.map (f : M →ₗ[R] P) (g : N →ₗ[R] Q).

Русский

Пусть f: M →ₗ⁅R,L⁆ P и g: N →ₗ⁅R,L⁆ Q — морфизмы Ли-модулей. Тогда линейное отображение, лежащее в основе отображения map f g, равно обычному тензорному отображению TensorProduct.map (f) (g).

LaTeX

$$$$(map\, f\, g) = TensorProduct.map\,(f : M \to P)\,(g : N \to Q).$$$$

Lean4

@[simp]
theorem toLinearMap_map (f : M →ₗ⁅R,L⁆ P) (g : N →ₗ⁅R,L⁆ Q) :
    (map f g : M ⊗[R] N →ₗ[R] P ⊗[R] Q) = TensorProduct.map (f : M →ₗ[R] P) (g : N →ₗ[R] Q) :=
  rfl

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