English
On a chosen basis, the matrix of the dualTensorHom on a simple tensor is a unit matrix placed at a single location.
Русский
Для выбранной базы матрица dualTensorHom на простом тензоре имеет единицу в одной позиции и нули повсюду.
LaTeX
$$$\text{toMatrix}\big(bM,bN,(\mathrm{dualTensorHom R M N}(bM.coord j \otimes bN i))\big) = \mathrm{single} i j 1$$$
Lean4
/-- When `M` is a finite free module, the map `lTensorHomToHomLTensor` is an equivalence. Note
that `lTensorHomEquivHomLTensor` is not defined directly in terms of
`lTensorHomToHomLTensor`, but the equivalence between the two is given by
`lTensorHomEquivHomLTensor_toLinearMap` and `lTensorHomEquivHomLTensor_apply`. -/
noncomputable def lTensorHomEquivHomLTensor : P ⊗[R] (M →ₗ[R] Q) ≃ₗ[R] M →ₗ[R] P ⊗[R] Q :=
congr (LinearEquiv.refl R P) (dualTensorHomEquiv R M Q).symm ≪≫ₗ TensorProduct.leftComm R P _ Q ≪≫ₗ
dualTensorHomEquiv R M _
