English
Define a functorial map from M ∗ N to M' ∗ N' by applying f to M and g to N inside the sum, i.e., map f g is obtained by lifting mk after mapping Sum.map f g.
Русский
Задаётся отображение map f g: M ∗ N → M' ∗ N', получаемое подъемом mk после отображения Sum.map f g.
LaTeX
$$$\mathrm{map}: (f: M \to M') (g: N \to N') \mapsto (\mathrm{Monoid.Coprod}.map\, f\, g): M \ast N \to M' \ast N'.$$$
Lean4
/-- Map `M ∗ N` to `M' ∗ N'` by applying `Sum.map f g` to each element of the underlying list. -/
@[to_additive /-- Map `AddMonoid.Coprod M N` to `AddMonoid.Coprod M' N'`
by applying `Sum.map f g` to each element of the underlying list. -/
]
def map (f : M →* M') (g : N →* N') : M ∗ N →* M' ∗ N' :=
clift (mk.comp <| FreeMonoid.map <| Sum.map f g)
(by simp only [MonoidHom.comp_apply, map_of, Sum.map_inl, map_one, mk_of_inl])
(by simp only [MonoidHom.comp_apply, map_of, Sum.map_inr, map_one, mk_of_inr])
(fun x y => by simp only [MonoidHom.comp_apply, map_of, Sum.map_inl, map_mul, mk_of_inl]) fun x y => by
simp only [MonoidHom.comp_apply, map_of, Sum.map_inr, map_mul, mk_of_inr]
