English
There is a natural equivalence between the set of functions α → β and the group homomorphisms FreeAbelianGroup α →+ β, induced by the universal property of the free abelian group.
Русский
Существует естественная эквивалентность между множеством функций α → β и гомоморфизмами FreeAbelianGroup α →+ β, порожденная универсальным свойством свободной абелевой группы.
LaTeX
$$$\\operatorname{lift}: (\\alpha \\to \\beta) \\simeq (FreeAbelianGroup\\ \\alpha \\to_+ \\beta)$$$
Lean4
/-- The map `FreeAbelianGroup α →+ A` induced by a map of types `α → A`. -/
def lift {β : Type v} [AddCommGroup β] : (α → β) ≃ (FreeAbelianGroup α →+ β) :=
(@FreeGroup.lift _ (Multiplicative β) _).trans <|
(@Abelianization.lift _ _ (Multiplicative β) _).trans MonoidHom.toAdditive
