English
On a basis element bM.coord j ⊗ bN i, the matrix of dualTensorHom is a matrix with a single 1 at position (i,j).
Русский
На базисном элементе bM.coord j ⊗ bN i матрица dualTensorHom имеет единицу в позиции (i,j) и нули в остальных местах.
LaTeX
$$$\text{toMatrix}(bM,bN)(\mathrm{dualTensorHom}(R,M,N)(bM.coord\,j \otimes bN i)) = \text{single } i j 1$$$
Lean4
/-- If `M` is free, the natural linear map $M^* ⊗ N → Hom(M, N)$ is an equivalence. This function
provides this equivalence in return for a basis of `M`. -/
-- We manually create simp-lemmas because `@[simps]` generates a malformed lemma
noncomputable def dualTensorHomEquivOfBasis : Module.Dual R M ⊗[R] N ≃ₗ[R] M →ₗ[R] N :=
LinearEquiv.ofLinear (dualTensorHom R M N)
(∑ i, TensorProduct.mk R _ N (b.dualBasis i) ∘ₗ (LinearMap.applyₗ (R := R) (b i)))
(by
ext f m
simp only [applyₗ_apply_apply, coeFn_sum, dualTensorHom_apply, mk_apply, id_coe, _root_.id, Fintype.sum_apply,
Function.comp_apply, Basis.coe_dualBasis, coe_comp, Basis.coord_apply, ← f.map_smul,
_root_.map_sum (dualTensorHom R M N), ← _root_.map_sum f, b.sum_repr])
(by
ext f m
simp only [applyₗ_apply_apply, coeFn_sum, dualTensorHom_apply, mk_apply, id_coe, _root_.id, Fintype.sum_apply,
Function.comp_apply, Basis.coe_dualBasis, coe_comp, compr₂_apply, tmul_smul, smul_tmul', ← sum_tmul,
Basis.sum_dual_apply_smul_coord])
