English
Let g be a homomorphism from FreeGroup α to FreeGroup β such that g(of x) = of (f x) for all x. Then g = map f on all of FreeGroup α.
Русский
Пусть g: FreeGroup α →* FreeGroup β — гомоморфизм, удовлетворяющий g(of x) = of (f x) для всех x. Тогда g = map f на всей FreeGroup α.
LaTeX
$$$ \\forall g: FreeGroup α →* FreeGroup β,\\; (\\forall x, g(FreeGroup.of x) = FreeGroup.of (f x)) \\Rightarrow \\forall x, g x = map f x $$$
Lean4
@[to_additive]
theorem unique (g : FreeGroup α →* FreeGroup β) (hg : ∀ x, g (FreeGroup.of x) = FreeGroup.of (f x)) :
∀ {x}, g x = map f x := by
rintro ⟨L⟩
exact
List.recOn L g.map_one fun ⟨x, b⟩ t (ih : g (FreeGroup.mk t) = map f (FreeGroup.mk t)) =>
Bool.recOn b
(show g ((FreeGroup.of x)⁻¹ * FreeGroup.mk t) = FreeGroup.map f ((FreeGroup.of x)⁻¹ * FreeGroup.mk t) by
simp [g.map_mul, g.map_inv, hg, ih])
(show g (FreeGroup.of x * FreeGroup.mk t) = FreeGroup.map f (FreeGroup.of x * FreeGroup.mk t) by
simp [g.map_mul, hg, ih])
