Bases and dimensionality of tensor products of modules #
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) :
If b : ι → M and c : κ → N are bases then so is λ i, b i.1 ⊗ₜ c i.2 : ι × κ → M ⊗ N.
Equations
- b.tensor_product c = finsupp.basis_single_one.map ((tensor_product.congr b.repr c.repr).trans ((finsupp_tensor_finsupp R R R ι κ).trans (finsupp.lcongr (equiv.refl (ι × κ)) (tensor_product.lid R R)))).symm
@[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 : κ) :
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 : ι × κ) :
@[protected, instance]
def
finite_dimensional_tensor_product
{K : Type u_1}
(V : Type u_2)
(W : Type u_3)
[field K]
[add_comm_group V]
[module K V]
[add_comm_group W]
[module K W]
[finite_dimensional K V]
[finite_dimensional K W] :
finite_dimensional K (V ⊗ W)
If V and W are finite dimensional K vector spaces, so is V ⊗ W.