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}
{S : Type u_2}
{M : Type u_3}
{N : Type u_4}
{ι : Type u_5}
{κ : Type u_6}
[CommSemiring R]
[CommSemiring S]
[Algebra R S]
[AddCommMonoid M]
[Module R M]
[Module S M]
[IsScalarTower R S M]
[AddCommMonoid N]
[Module R N]
(b : Basis ι S M)
(c : Basis κ R N)
:
Basis (ι × κ) S (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_3}
{N : Type u_4}
{ι : Type u_5}
{κ : Type u_6}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
[AddCommMonoid 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_3}
{N : Type u_4}
{ι : Type u_5}
{κ : Type u_6}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
[AddCommMonoid N]
[Module R N]
(b : Basis ι R M)
(c : Basis κ R N)
(i : ι × κ)
:
(Basis.tensorProduct b c) i = b i.1 ⊗ₜ[R] c i.2
@[simp]
theorem
Basis.tensorProduct_repr_tmul_apply
{R : Type u_1}
{M : Type u_3}
{N : Type u_4}
{ι : Type u_5}
{κ : Type u_6}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
[AddCommMonoid 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