English
There is a canonical map sending α→β to a free-group homomorphism FreeGroup α → FreeGroup β; this is the universal map functor.
Русский
Существует каноническое отображение α→β в гомоморфизм свободной группы FreeGroup α → FreeGroup β; это универсальное отображение.
LaTeX
$$$FreeGroup.map: (\\alpha \\to \\beta) \\to (FreeGroup(\\alpha) \\to FreeGroup(\\beta))$$$
Lean4
/-- Any function from `α` to `β` extends uniquely to a group homomorphism from the free group over
`α` to the free group over `β`. -/
@[to_additive /-- Any function from `α` to `β` extends uniquely to an additive group homomorphism
from the additive free group over `α` to the additive free group over `β`. -/
]
def map : FreeGroup α →* FreeGroup β :=
MonoidHom.mk' (Quot.map (List.map fun x => (f x.1, x.2)) fun L₁ L₂ H => by cases H; simp) (by rintro ⟨L₁⟩ ⟨L₂⟩; simp)
