English
If two maps f,g from free k G α to A agree on all generators, then f=g (extensionality for free objects).
Русский
Если две отображения f,g из свободного объекта совпадают на всех генераторах, то они равны (расширение свободного объекта).
LaTeX
$$$\\forall f,g:\\mathrm{free}\\ k\\ G\\ α \\to A,\\; (\\forall i\\in α, f(\\mathrm{single}\\ i (\\mathrm{single}\\,1\\,1)) = g(\\mathrm{single}\\ i (\\mathrm{single}\\,1\\,1)) ) \\Rightarrow f=g$$$
Lean4
@[ext]
theorem free_ext (f g : free k G α ⟶ A) (h : ∀ i : α, f.hom (single i (single 1 1)) = g.hom (single i (single 1 1))) :
f = g := by classical exact (freeLiftLEquiv α A).injective (funext_iff.2 h)
