mapIncl — Mathlib

English

Given Lie submodules M' ⊆ M and N' ⊆ N, there is a natural Lie-module map mapIncl M' N' : M' ⊗R N' →ₗ⁅R,L⁆ M ⊗R N defined by composing the canonical inclusions with the standard tensor product map.

Русский

Пусть M' ⊆ M и N' ⊆ N — подпсубмодули Ли. Существует естественное отображение Ли-модулей mapIncl M' N' : M' ⊗R N' →ₗ⁅R,L⁆ M ⊗R N, задающееся через включения и стандартное тензорное отображение.

LaTeX

$$$${\mathrm{mapIncl}}(M',N') : M' \otimes_R N' \to M \otimes_R N.$$$$

Lean4

/-- Given Lie submodules `M' ⊆ M` and `N' ⊆ N`, this is the natural map: `M' ⊗ N' → M ⊗ N`. -/
def mapIncl (M' : LieSubmodule R L M) (N' : LieSubmodule R L N) : M' ⊗[R] N' →ₗ⁅R,L⁆ M ⊗[R] N :=
  map M'.incl N'.incl

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