English
Given a basis b, there is a canonical bijection between functions ι → H and monoid homomorphisms G →* H, implemented by lifting via b.
Русский
Дано базис b, существует каноническая биекция между отображениями ι → H и гомоморфизмами G →* H, реализованная через подъём по b.
LaTeX
$$$ (ι \to H) \cong (G \to^* H) $$$
Lean4
/-- Given a free group basis of `G` over `ι`, there is a canonical bijection between maps from `ι`
to a group `H` and morphisms from `G` to `H`. -/
@[simps!]
def lift (b : FreeGroupBasis ι G) : (ι → H) ≃ (G →* H) :=
FreeGroup.lift.trans
{ toFun := fun f => f.comp b.repr.toMonoidHom
invFun := fun f => f.comp b.repr.symm.toMonoidHom
left_inv := fun f => by
ext
simp
right_inv := fun f => by
ext
simp }
