Tensor-product basis coordinates

This file records how contractions against one factor of a tensor product detect equality when that factor is free, and how coordinates in a basis of one factor commute with maps of the other. It also proves that the coordinates in bases obtained by scalar extension commute with a map of the scalar-extension algebras, and that over a basis with at most one index a scalar extension consists of pure tensors.

Main declarations

• TensorProduct.tensor_eq_of_forall_tensorComponent_eq: contractions against a projective right factor detect equality.
• Module.Basis.equivFinsuppOfBasisLeft_lTensor_apply and Module.Basis.lTensor_eq_zero_iff_forall_equivFinsuppOfBasisLeft: coordinates in a basis of the left factor commute with maps of the right factor, so such a map kills an element exactly when it kills every coordinate.
• Module.Basis.map_baseChange_repr: applying a scalar map to a coordinate in a base-changed basis agrees with first mapping the tensor and then taking its coordinate.
• Module.Basis.eq_baseChange_repr_tmul_of_subsingleton: over a basis with at most one index, every element of a scalar extension is the pure tensor of its unique coordinate with the corresponding basis vector.
• Module.Basis.baseChange_toMatrix_baseChange: change-of-basis matrices between base-changed bases are obtained by mapping entries.
• Module.Basis.map_toMatrixAlgEquiv_baseChange: matrices in base-changed bases commute with scalar maps when the represented endomorphisms are intertwined by tensor-product base change.
• Module.Basis.toMatrix_baseChange_baseChange: matrices of scalar-extended endomorphisms are obtained by mapping entries.

theorem TensorProduct.tensor_eq_of_forall_tensorComponent_eq {R : Type u} {M : Type v} {N : Type w} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Module.Projective R N] {x y : TensorProduct R M N} (h : ∀ (φ : Module.Dual R N), (LinearMap.tensorComponent φ) x = (LinearMap.tensorComponent φ) y) : x = y

Equality of all contractions against the right factor detects equality in a tensor product over a commutative semiring when the right factor is projective.

@[simp]

theorem Module.Basis.equivFinsuppOfBasisLeft_lTensor_apply {R : Type u} {M : Type v} {N : Type w} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {ι : Type u_1} [DecidableEq ι] {P : Type u_2} [AddCommMonoid P] [Module R P] (ℬ : Basis ι R M) (g : N →ₗ[R] P) (x : TensorProduct R M N) (i : ι) : ((TensorProduct.equivFinsuppOfBasisLeft ℬ) ((LinearMap.lTensor M g) x)) i = g (((TensorProduct.equivFinsuppOfBasisLeft ℬ) x) i)

Coordinates in a basis of the left factor commute with maps of the right factor.

theorem Module.Basis.lTensor_eq_zero_iff_forall_equivFinsuppOfBasisLeft {R : Type u} {M : Type v} {N : Type w} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {ι : Type u_1} [DecidableEq ι] {P : Type u_2} [AddCommMonoid P] [Module R P] (ℬ : Basis ι R M) (g : N →ₗ[R] P) (x : TensorProduct R M N) : (LinearMap.lTensor M g) x = 0 ↔ ∀ (i : ι), g (((TensorProduct.equivFinsuppOfBasisLeft ℬ) x) i) = 0

Over a basis of the left factor, a map of the right factor kills an element of the tensor product exactly when it kills each of its coordinates.

@[simp]

theorem Module.Basis.map_baseChange_repr {R : Type u} [CommSemiring R] {M : Type x} [AddCommMonoid M] [Module R M] {ι : Type u_1} {S : Type v} [Semiring S] [Algebra R S] {T : Type w} [Semiring T] [Algebra R T] (b : Basis ι R M) (φ : S →ₗ[R] T) (z : TensorProduct R S M) (i : ι) : φ (((baseChange S b).repr z) i) = ((baseChange T b).repr ((TensorProduct.map φ LinearMap.id) z)) i

Coordinates in a base-changed basis are natural in the scalar-extension algebra.

theorem Module.Basis.eq_baseChange_repr_tmul_of_subsingleton {R : Type u} [CommSemiring R] {M : Type x} [AddCommMonoid M] [Module R M] {ι : Type u_1} {S : Type v} [Semiring S] [Algebra R S] [Subsingleton ι] (b : Basis ι R M) (z : TensorProduct R S M) (i : ι) : z = ((baseChange S b).repr z) i ⊗ₜ[R] b i

Over a basis with at most one index, every element of a scalar extension is the pure tensor of its unique coordinate with the corresponding basis vector. This isolates the tensor bookkeeping needed to reduce statements about rank-at-most-one scalar extensions to scalar multiples of a single vector.

@[simp]

theorem Module.Basis.baseChange_toMatrix_baseChange {R : Type u} [CommSemiring R] {M : Type x} [AddCommMonoid M] [Module R M] {ι : Type u_1} {S : Type v} [CommSemiring S] [Algebra R S] {ι' : Type u_2} (b : Basis ι R M) (b' : Basis ι' R M) : (baseChange S b).toMatrix ⇑(baseChange S b') = (b.toMatrix ⇑b').map ⇑(algebraMap R S)

The change-of-basis matrix between two base-changed bases is the entrywise scalar extension of the change-of-basis matrix between the original bases.

theorem Module.Basis.toMatrix_baseChange_baseChange {R : Type u} [CommSemiring R] {M : Type x} [AddCommMonoid M] [Module R M] {ι : Type u_1} {S : Type v} [CommSemiring S] [Algebra R S] [Fintype ι] [DecidableEq ι] (b : Basis ι R M) (f : M →ₗ[R] M) : (LinearMap.toMatrix (baseChange S b) (baseChange S b)) (LinearMap.baseChange S f) = ((LinearMap.toMatrix b b) f).map ⇑(algebraMap R S)

The matrix of a scalar-extended endomorphism is the entrywise scalar extension of its matrix in the original basis.

theorem Module.Basis.map_toMatrixAlgEquiv_baseChange {R : Type u} [CommSemiring R] {M : Type x} [AddCommMonoid M] [Module R M] {ι : Type u_1} {S : Type v} [CommSemiring S] [Algebra R S] {T : Type w} [CommSemiring T] [Algebra R T] [Fintype ι] [DecidableEq ι] (b : Basis ι R M) (φ : S →ₐ[R] T) (f : TensorProduct R S M →ₗ[S] TensorProduct R S M) (g : TensorProduct R T M →ₗ[T] TensorProduct R T M) (h : ∀ (z : TensorProduct R S M), (TensorProduct.map φ.toLinearMap LinearMap.id) (f z) = g ((TensorProduct.map φ.toLinearMap LinearMap.id) z)) : ((LinearMap.toMatrixAlgEquiv (baseChange S b)) f).map ⇑φ = (LinearMap.toMatrixAlgEquiv (baseChange T b)) g

Matrices in base-changed bases commute with a scalar map when the corresponding endomorphisms are intertwined by tensor-product base change.