TensorProduct.toMatrix_comm

theorem TensorProduct.toMatrix_comm : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {ι : Type u_7} {κ : Type u_8} [inst : DecidableEq ι] [inst_1 : DecidableEq κ] [inst_2 : Fintype ι] [inst_3 : Fintype κ] [inst_4 : CommRing R] [inst_5 : AddCommGroup M] [inst_6 : AddCommGroup N] [inst_7 : Module R M] [inst_8 : Module R N] (bM : Basis ι R M) (bN : Basis κ R N), (LinearMap.toMatrix (bM.tensorProduct bN) (bN.tensorProduct bM)) ↑(TensorProduct.comm R M N) = Matrix.submatrix 1 Prod.swap id

This theorem states that for any commutative ring `R` and additive commutative groups `M` and `N` that are also `R`-modules, given bases `bM` and `bN` for `M` and `N` respectively, the representation of the commutativity of the tensor product as a linear map (given by `TensorProduct.comm R M N`) in the matrix form with respect to the tensor product bases `bM.tensorProduct bN` and `bN.tensorProduct bM` is equivalent to the submatrix of the identity matrix obtained by swapping the factors of the product. In other words, the commutativity of the tensor product corresponds to a permutation of the identity matrix in this matrix representation. The types `ι` and `κ` are the index types for the bases, and we require decidable equality and finiteness on them for the basis representation.

More concisely: For any commutative rings `R`, additive commutative `R`-modules `M` and `N` with decidable equality and finiteness index types `ι` and `κ`, and bases `bM` and `bN` for `M` and `N` respectively, the commutativity of the tensor product of `M` and `N` over `R` is equivalent to the identity matrix representing this tensor product having a submatrix that is the transpose of its mirror image.