English
The ith canonical injection of A_i into the free product is given as a linear map from A_i into FreeProduct R A, obtained by composing the direct sum injection into the direct sum with the quotient map.
Русский
Пусть i-й каноническая инъекция из A_i в свободное произведение задаётся как линейное отображение из A_i в FreeProduct R A, получаемое путём композиции инъекции прямой суммы в DirectSum и соответствующего квартового отображения.
LaTeX
$$$\iota'_R A(i) : A_i \to_{\mathrm{Lin}} \mathrm{FreeProduct}(R,A)$ with $\iota'_R A(i)= (\mathrm{mkAlgHom}\;R\;A)\circ_{\mathrm{Lin}} (\mathrm{DirectSum}.lof\;R\;I\;A\;i)$$$
Lean4
/-- The canonical linear map from the direct sum of the `A i` to the free product -/
abbrev ι' : (⨁ i, A i) →ₗ[R] FreeProduct R A :=
(mkAlgHom R A).toLinearMap ∘ₗ TensorAlgebra.ι R (M := ⨁ i, A i)
