equivFinsuppOfBasisRight_apply_tmul_apply

English

The inverse of the right equivariant map is given by a left-linear combination of basis tensors.

Русский

Обратное отображение к правому эквиваленту записывается как линейная комбинация левых тензоров базисов.

LaTeX

$$(TensorProduct.equivFinsuppOfBasisRight 𝒞).symm.toLinearMap = Finsupp.lsum R (fun i ⇢ (TensorProduct.mk R M N).flip (𝒞 i))$$

Lean4

theorem equivFinsuppOfBasisRight_apply_tmul_apply (m : M) (n : N) (i : κ) :
    (TensorProduct.equivFinsuppOfBasisRight 𝒞) (m ⊗ₜ n) i = 𝒞.repr n i • m := by
  simp only [equivFinsuppOfBasisRight_apply_tmul, Finsupp.mapRange_apply]

Похожие утверждения