lTensorHomToHomLTensor — Mathlib

English

The map that takes a pair of linear maps to their tensor-product map is bilinear in each argument.

Русский

Отображение, сопоставляющее пару линейных отображений их тензорному отображению, би-линейно по каждому аргументу.

LaTeX

$$def mapBilinear : (M →ₗ[R] P) → (N →ₗ[R] Q) → M ⊗[R] N →ₗ[R] P ⊗[R] Q := LinearMap.mk₂ R map ...$$

Lean4

/-- The canonical linear map from `P ⊗[R] (M →ₗ[R] Q)` to `(M →ₗ[R] P ⊗[R] Q)` -/
def lTensorHomToHomLTensor : P ⊗[R] (M →ₗ[R] Q) →ₗ[R] M →ₗ[R] P ⊗[R] Q :=
  TensorProduct.lift (llcomp R M Q _ ∘ₗ mk R P Q)

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