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] [Semiring 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.

@[simp]

theorem Basis.tensorProduct_apply {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} {ι : Type u_5} {κ : Type u_6} [CommSemiring R] [Semiring 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) (i : ι) (j : κ) : (b.tensorProduct c) (i, j) = b i ⊗ₜ[R] c j

theorem Basis.tensorProduct_apply' {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} {ι : Type u_5} {κ : Type u_6} [CommSemiring R] [Semiring 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) (i : ι × κ) : (b.tensorProduct c) i = b i.1 ⊗ₜ[R] c i.2

@[simp]

theorem Basis.tensorProduct_repr_tmul_apply {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} {ι : Type u_5} {κ : Type u_6} [CommSemiring R] [Semiring 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) (m : M) (n : N) (i : ι) (j : κ) : ((b.tensorProduct c).repr (m ⊗ₜ[R] n)) (i, j) = (c.repr n) j • (b.repr m) i

noncomputable def Basis.baseChange {R : Type u_1} {M : Type u_3} {ι : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] (S : Type u_7) [Semiring S] [Algebra R S] (b : Basis ι R M) : Basis ι S (TensorProduct R S M)

The lift of an R-basis of M to an S-basis of the base change S ⊗[R] M.

Equations

• Basis.baseChange S b = ((Basis.singleton Unit S).tensorProduct b).reindex (Equiv.punitProd ι)

@[simp]

theorem Basis.baseChange_repr_tmul {R : Type u_1} {M : Type u_3} {ι : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] (S : Type u_7) [Semiring S] [Algebra R S] (b : Basis ι R M) (x : S) (y : M) (i : ι) : ((Basis.baseChange S b).repr (x ⊗ₜ[R] y)) i = (b.repr y) i • x

@[simp]

theorem Basis.baseChange_apply {R : Type u_1} {M : Type u_3} {ι : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] (S : Type u_7) [Semiring S] [Algebra R S] (b : Basis ι R M) (i : ι) : (Basis.baseChange S b) i = 1 ⊗ₜ[R] b i