English
There is a canonical quotient homomorphism from the FreeTensorAlgebra FreeTensorAlgebra R A to the FreeProduct FreeProduct R A, denoted by mkAlgHom, which encodes the quotient that defines the free product as a quotient of the tensor algebra by the relations rel R A.
Русский
Существует каноническое отношении-морфизм свободной тензорной алгебры в свободное произведение, обозначаемый mkAlgHom, который кодирует факторизацию через отношение rel R A, определяющее свободное произведение как отношение тензорной алгебры.
LaTeX
$$$\mathrm{mkAlgHom}:\; \mathrm{FreeTensorAlgebra}\; R\; A \;\to_{\mathrm{Alg}}\; \mathrm{FreeProduct}\; R\; A$$$
Lean4
/-- The canonical quotient map `FreeTensorAlgebra R A →ₐ[R] FreeProduct R A`,
as an `R`-algebra homomorphism -/
abbrev mkAlgHom : FreeTensorAlgebra R A →ₐ[R] FreeProduct R A :=
RingQuot.mkAlgHom R (rel R A)
