Bases and dimensionality of tensor products of modules #
These can not go into LinearAlgebra.TensorProduct since they depend on
LinearAlgebra.FinsuppVectorSpace which in turn imports LinearAlgebra.TensorProduct.
def
Basis.tensorProduct
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
{ι : Type u_4}
{κ : Type u_5}
[CommRing R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
(b : Basis ι R M)
(c : Basis κ R N)
:
Basis (ι × κ) R (TensorProduct R M N)
If b : ι → M and c : κ → N are bases then so is fun i ↦ b i.1 ⊗ₜ c i.2 : ι × κ → M ⊗ N.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
Basis.tensorProduct_apply
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
{ι : Type u_4}
{κ : Type u_5}
[CommRing R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
(b : Basis ι R M)
(c : Basis κ R N)
(i : ι)
(j : κ)
:
↑(Basis.tensorProduct b c) (i, j) = ↑b i ⊗ₜ[R] ↑c j
theorem
Basis.tensorProduct_apply'
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
{ι : Type u_4}
{κ : Type u_5}
[CommRing R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
(b : Basis ι R M)
(c : Basis κ R N)
(i : ι × κ)
:
↑(Basis.tensorProduct b c) i = ↑b i.fst ⊗ₜ[R] ↑c i.snd
@[simp]
theorem
Basis.tensorProduct_repr_tmul_apply
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
{ι : Type u_4}
{κ : Type u_5}
[CommRing R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
(b : Basis ι R M)
(c : Basis κ R N)
(m : M)
(n : N)
(i : ι)
(j : κ)
:
↑(↑(Basis.tensorProduct b c).repr (m ⊗ₜ[R] n)) (i, j) = ↑(↑b.repr m) i * ↑(↑c.repr n) j