English
For each i, there is an injection of M_i into CoprodI M, sending m in M_i to the word representing ⟨i, m⟩, thus embedding summands inside the free product.
Русский
Для каждого i существует внедрение M_i в CoprodI M, отправляющее m в M_i в слово ⟨i,m⟩, т.е. вложение слагаемых в свободный копродукт.
LaTeX
$$$\\operatorname{of}: M_i \\to^* \\mathrm{CoprodI}(M)$ is the embedding sending \\; m \\mapsto \\mathrm{Con.mk'}(\\_, \\langle i,m \\rangle).$$$
Lean4
/-- The inclusion of a summand into the free product. -/
def of {i : ι} : M i →* CoprodI M
where
toFun x := Con.mk' _ (FreeMonoid.of <| Sigma.mk i x)
map_one' := (Con.eq _).mpr (ConGen.Rel.of _ _ (CoprodI.Rel.of_one i))
map_mul' x y := Eq.symm <| (Con.eq _).mpr (ConGen.Rel.of _ _ (CoprodI.Rel.of_mul x y))
