Documentation

CompPoly.LinearAlgebra.TensorProduct.Basis

Bases for the right scalar action on tensor products #

Module.Basis.baseChangeRight lifts a basis of Left over K to a basis of Left ⊗[K] Right over Right, with scalars acting on the right tensor factor. The action is explicit in each declaration; importing this module preserves Mathlib's default action on the left factor, including when Left = Right.

For equal factors, select the right Algebra, Module, DistribMulAction and SMul locally when combining this basis with scalar notation and module laws. Tensor products provide independent default instances at each of these levels.

For background on tensor-product bases, see [Lan02]. For equal field factors, this right-action basis is the basis used for the row representation in [DP24], §2.5.

References #

source
noncomputable def Module.Basis.baseChangeRight {K : Type u_1} {Left : Type u_2} {Right : Type u_3} {ι : Type u_4} [CommSemiring K] [Semiring Left] [CommSemiring Right] [Algebra K Left] [Algebra K Right] (b : Basis ι K Left) :
Basis ι Right (TensorProduct K Left Right)

Lift a K-basis of Left to a Right-basis of Left ⊗[K] Right, using the right-factor scalar action. This is the right-sided counterpart to Basis.baseChange.

Instances For
    source
    @[simp]
    theorem Module.Basis.baseChangeRight_repr_tmul {K : Type u_1} {Left : Type u_2} {Right : Type u_3} {ι : Type u_4} [CommSemiring K] [Semiring Left] [CommSemiring Right] [Algebra K Left] [Algebra K Right] (b : Basis ι K Left) (x : Left) (y : Right) (i : ι) :
    (b.baseChangeRight.repr (x ⊗ₜ[K] y)) i = (b.repr x) i • y

    Coordinates of a pure tensor in the basis for the right-factor scalar action.

    source
    @[simp]
    theorem Module.Basis.baseChangeRight_apply {K : Type u_1} {Left : Type u_2} {Right : Type u_3} {ι : Type u_4} [CommSemiring K] [Semiring Left] [CommSemiring Right] [Algebra K Left] [Algebra K Right] (b : Basis ι K Left) (i : ι) :
    b.baseChangeRight i = b i ⊗ₜ[K] 1

    The right-action basis vectors are the original basis vectors tensored with one.