English
There is a natural equivalence between all functions α → β and semigroup homomorphisms FreeSemigroup α →⋅ β. The lift operation sends a function f: α → β to the corresponding semigroup homomorphism FreeSemigroup α →⋅ β, and its inverse composes with the embedding of α into FreeSemigroup α.
Русский
Существует естественное биективное соответствие между функциями α → β и полугумомоморфизмами FreeSemigroup α →⋅ β. Лифтинг отображает f: α → β в соответствующий гомоморфизм FreeSemigroup α →⋅ β, а обратное восстанавливает функцию через композицию с включением α в FreeSemigroup α.
LaTeX
$$lift : (α → β) ≃ (FreeSemigroup α →⋅ β)$$
Lean4
/-- Lifts a function `α → β` to a semigroup homomorphism `FreeSemigroup α → β` given
a semigroup `β`. -/
@[to_additive (attr := simps symm_apply) /-- Lifts a function `α → β` to an additive semigroup
homomorphism `FreeAddSemigroup α → β` given an additive semigroup `β`. -/
]
def lift : (α → β) ≃ (FreeSemigroup α →ₙ* β)
where
toFun
f :=
{ toFun := fun x ↦ x.2.foldl (fun a b ↦ a * f b) (f x.1)
map_mul' := fun x y ↦ by
simp [head_mul, tail_mul, ← List.foldl_map, List.foldl_append, List.foldl_cons, List.foldl_assoc] }
invFun f := f ∘ of
