mathlib3 documentation

linear_algebra.tensor_product_basis

Bases and dimensionality of tensor products of modules #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

These can not go into linear_algebra.tensor_product since they depend on linear_algebra.finsupp_vector_space which in turn imports linear_algebra.tensor_product.

noncomputable def basis.tensor_product {R : Type u_1} {M : Type u_2} {N : Type u_3} {ι : Type u_4} {κ : Type u_5} [comm_ring R] [add_comm_group M] [module R M] [add_comm_group N] [module R N] (b : basis ι R M) (c : basis κ R N) :
basis × κ) R (tensor_product R M N)

If b : ι → M and c : κ → N are bases then so is λ i, b i.1 ⊗ₜ c i.2 : ι × κ → M ⊗ N.

Equations
@[simp]
theorem basis.tensor_product_apply {R : Type u_1} {M : Type u_2} {N : Type u_3} {ι : Type u_4} {κ : Type u_5} [comm_ring R] [add_comm_group M] [module R M] [add_comm_group N] [module R N] (b : basis ι R M) (c : basis κ R N) (i : ι) (j : κ) :
(b.tensor_product c) (i, j) = b i ⊗ₜ[R] c j
theorem basis.tensor_product_apply' {R : Type u_1} {M : Type u_2} {N : Type u_3} {ι : Type u_4} {κ : Type u_5} [comm_ring R] [add_comm_group M] [module R M] [add_comm_group N] [module R N] (b : basis ι R M) (c : basis κ R N) (i : ι × κ) :
@[simp]
theorem basis.tensor_product_repr_tmul_apply {R : Type u_1} {M : Type u_2} {N : Type u_3} {ι : Type u_4} {κ : Type u_5} [comm_ring R] [add_comm_group M] [module R M] [add_comm_group N] [module R N] (b : basis ι R M) (c : basis κ R N) (m : M) (n : N) (i : ι) (j : κ) :
(((b.tensor_product c).repr) (m ⊗ₜ[R] n)) (i, j) = ((b.repr) m) i * ((c.repr) n) j