Coefficients in a tensor product with a free module #
Two facts about Mathlib's TensorProduct.finsuppScalarLeft, which identifies (ι →₀ R) ⊗[R] N
with ι →₀ N by taking coefficients against the standard basis.
Main results #
TensorProduct.finsuppScalarLeft_lTensor_apply: taking coefficients is natural inN.TensorProduct.sum_single_tmul_finsuppScalarLeft: an element is the sum of its coefficients against the basis vectors.
@[simp]
theorem
TensorProduct.finsuppScalarLeft_lTensor_apply
{R : Type u_1}
[CommSemiring R]
{ι : Type u_2}
[DecidableEq ι]
{N : Type u_3}
{N' : Type u_4}
[AddCommMonoid N]
[Module R N]
[AddCommMonoid N']
[Module R N']
(g : N →ₗ[R] N')
(t : TensorProduct R (ι →₀ R) N)
(i : ι)
:
((finsuppScalarLeft R N' ι) ((LinearMap.lTensor (ι →₀ R) g) t)) i = g (((finsuppScalarLeft R N ι) t) i)
The coefficients of (1 ⊗ g) t in (ι →₀ R) ⊗ N' are the images under g of the
coefficients of t.
theorem
TensorProduct.sum_single_tmul_finsuppScalarLeft
{R : Type u_1}
[CommSemiring R]
{ι : Type u_2}
[DecidableEq ι]
{N : Type u_3}
[AddCommMonoid N]
[Module R N]
(t : TensorProduct R (ι →₀ R) N)
:
∑ i ∈ ((finsuppScalarLeft R N ι) t).support, Finsupp.single i 1 ⊗ₜ[R] ((finsuppScalarLeft R N ι) t) i = t
An element of (ι →₀ R) ⊗ N is the sum of its coefficients against the basis vectors.