lTensor_tensor — Mathlib

English

There is a compatibility statement expressing that lTensor distributes over the tensor product in a canonical way, relating lTensor with assoc.

Русский

Существуют совместимости, говорящие, что lTensor распределяется по тензорному произведению канонически через ассоциатор.

LaTeX

$$$\\text{lTensor}_{R}(M\\otimes_R N) \\; f = (\\text{assoc}_R(M,N,Q))^{-1} \\circ_\\ell (f.\\text{lTensor} N).lTensor M \\circ_\\ell (\\text{assoc}_R M N P).toLinearMap$$$

Lean4

theorem lTensor_tensor (f : P →ₗ[R] Q) :
    lTensor (M ⊗[R] N) f = (assoc R M N Q).symm ∘ₗ (f.lTensor N).lTensor M ∘ₗ assoc R M N P :=
  TensorProduct.ext <| TensorProduct.ext rfl

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