English
There exists a natural equivalence between functions α → β and magma homomorphisms from the free magma on α to β, given by extending a function to a unique magma homomorphism.
Русский
Существует естественное биективное соответствие между отображениями α → β и морфизмами умножения из свободной магмы на α в β, задаваемое единственным продолжением отображения до гомоморфизма магмы.
LaTeX
$$$\mathrm{lift} : (\alpha \to \beta) \simeq (\mathrm{MulHom}(\mathrm{FreeMagma}(\alpha), \beta))$$$
Lean4
/-- The universal property of the free magma expressing its adjointness. -/
@[to_additive (attr := simps symm_apply) /--
The universal property of the free additive magma expressing its adjointness. -/
]
def lift : (α → β) ≃ (FreeMagma α →ₙ* β)
where
toFun
f :=
{ toFun := liftAux f
map_mul' := fun _ _ ↦ rfl }
invFun F := F ∘ of
