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
- 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 : κ) :
@[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 : κ) :