toMatrix_dualTensorHom

theorem toMatrix_dualTensorHom : ∀ {R : Type u} {M : Type v₁} {N : Type v₂} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] {m : Type u_1} {n : Type u_2} [inst_5 : Fintype m] [inst_6 : Finite n] [inst_7 : DecidableEq m] [inst_8 : DecidableEq n] (bM : Basis m R M) (bN : Basis n R N) (j : m) (i : n), (LinearMap.toMatrix bM bN) ((dualTensorHom R M N) (bM.coord j ⊗ₜ[R] bN i)) = Matrix.stdBasisMatrix i j 1

The theorem `toMatrix_dualTensorHom` states that for any commutative semiring `R` and additive commutative monoids `M` and `N` which are also `R`-modules, along with the basis `bM` and `bN` for `M` and `N` respectively, and given any elements `j` of type `m` (index for basis of `M`) and `i` of type `n` (index for basis of `N`), the matrix representation of the linear map `dualTensorHom R M N` evaluated at the tensor product of the `j`-th coordinate function of `bM` and the `i`-th basis vector of `bN` is a matrix with a single 1 at the (`i`, `j`)-th entry and zeros elsewhere. This matrix is precisely the standard basis matrix `Matrix.stdBasisMatrix i j 1`.

More concisely: For any commutative semiring R and additive commutative monoids M, N being R-modules with bases bM and bN, the matrix representation of the dual homomorphism of R-linear maps from M to N evaluated at the i-th basis vector of bN and j-th coordinate function of bM is the standard basis matrix.