English
Let α be a type and M a monoid. There is a natural bijection between functions f: α → M and monoid homomorphisms FreeMonoid α →* M; this bijection is realized by f ↦ lift f with inverse f ↦ f ∘ of.
Русский
Пусть α — множество, M — моноид. Естественная биекция между отображениями α → M и моноид-гомоморфизмами FreeMonoid α →* M; биекция задаётся f ↦ lift f и обратно f ↦ f ∘ of.
LaTeX
$$$ (\alpha \to M) \cong (FreeMonoid \alpha \to^* M) $$$
Lean4
/-- Equivalence between maps `α → M` and monoid homomorphisms `FreeMonoid α →* M`. -/
@[to_additive /-- Equivalence between maps `α → A` and additive monoid homomorphisms
`FreeAddMonoid α →+ A`. -/
]
def lift : (α → M) ≃ (FreeMonoid α →* M)
where
toFun
f :=
{ toFun := fun l ↦ prodAux ((toList l).map f)
map_one' := rfl
map_mul' := fun _ _ ↦ by simp only [prodAux_eq, toList_mul, List.map_append, List.prod_append] }
invFun f x := f (of x)
