Theorems · Theorem · linear algebra

TensorProduct.toMatrix_map

∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {M' : Type u_5} {N' : Type u_6} {ι : Type u_7} {κ : Type u_8}
  {ι' : Type u_10} {κ' : Type u_11} [inst : DecidableEq ι] [inst_1 : DecidableEq κ] [inst_2 : Fintype ι]
  [inst_3 : Fintype κ] [inst_4 : Finite ι'] [inst_5 : Finite κ'] [inst_6 : CommRing R] [inst_7 : AddCommGroup M]
  [inst_8 : AddCommGroup N] [inst_9 : AddCommGroup M'] [inst_10 : AddCommGroup N'] [inst_11 : Module R M]
  [inst_12 : Module R N] [inst_13 : Module R M'] [inst_14 : Module R N'] (bM : Module.Basis ι R M)
  (bN : Module.Basis κ R N) (bM' : Module.Basis ι' R M') (bN' : Module.Basis κ' R N') (f : M →ₗ[R] M') (g : N →ₗ[R] N'),
  (LinearMap.toMatrix (bM.tensorProduct bN) (bM'.tensorProduct bN')) (TensorProduct.map f g) =
    Matrix.kroneckerMap (fun x1 x2 => x1 * x2) ((LinearMap.toMatrix bM bM') f) ((LinearMap.toMatrix bN bN') g)

The linear map built from TensorProduct.map corresponds to the matrix built from Matrix.kronecker.

Defined in

Mathlib.LinearAlgebra.TensorProduct.Matrix

Cited by

1 results in Mathlib

Foundations

Depth 94 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DecidableEqDecidableEqFintypeFintypeFiniteFiniteCommRingAddCommGroupAddCommGroupAddCommGroupAddCommGroupModuleModuleModuleModule