English
Let R be a commutative semiring and M an R-module. For every element x in the direct sum ⨁_n ⨂^n_R M, applying the canonical embedding of the direct sum into the tensor algebra and then projecting back to the direct sum yields x; i.e., toDirectSum(ofDirectSum(x)) = x.
Русский
Пусть R — коммутативное полугруппа, M — модуль над R. Для любого элемента x из прямой суммы ⨁_n ⨂^n_R M применение канонического включения прямой суммы в тензорную алгебру, а затем проекция обратно в прямую сумму возвращает x; то есть toDirectSum(ofDirectSum(x)) = x.
LaTeX
$$$\\forall x \\in \\bigoplus_{n \\in \\mathbb{N}} M^{\\otimes n}_R\\;:\\; \\mathrm{toDirectSum}(\\mathrm{ofDirectSum}(x)) = x.$$$
Lean4
@[simp]
theorem toDirectSum_ofDirectSum (x : ⨁ n, ⨂[R]^n M) : TensorAlgebra.toDirectSum (ofDirectSum x) = x :=
AlgHom.congr_fun toDirectSum_comp_ofDirectSum x
