English
Two group homomorphisms out of a free group are equal if they agree on the generators.
Русский
Две гомоморфизмы по свободной группе совпадают, если согласованы на генерирующих элементах.
LaTeX
$$$\\forall f,g:\\ FreeGroup(\\alpha) \\to_* M,\\; (\\forall a:\\alpha,\\ f(of(a))=g(of(a))) \\Rightarrow f=g$$$
Lean4
/-- Two homomorphisms out of a free group are equal if they are equal on generators.
See note [partially-applied ext lemmas]. -/
@[to_additive (attr := ext) /-- Two homomorphisms out of a free additive group are equal if they are
equal on generators. See note [partially-applied ext lemmas]. -/
]
theorem ext_hom {M : Type*} [Monoid M] (f g : FreeGroup α →* M) (h : ∀ a, f (of a) = g (of a)) : f = g :=
by
ext x
have this (x) : f (of x)⁻¹ = g (of x)⁻¹ :=
by
trans f (of x)⁻¹ * f (of x) * g (of x)⁻¹
· simp_rw [mul_assoc, h, ← _root_.map_mul, mul_inv_cancel, _root_.map_one, mul_one]
· simp_rw [← _root_.map_mul, inv_mul_cancel, _root_.map_one, one_mul]
induction x <;> simp [*]
