English
A group G is finitely generated iff there exists a finite subset S of G and a surjective homomorphism from the free group on S onto G.
Русский
Группа G конечно порождена тогда и только тогда, когда существует конечное подмножество S ⊆ G и сюръективный одоморфизм из свободной группы на S в G.
LaTeX
$$$\operatorname{FG}(G) \iff \exists S \subseteq G,\; S\text{ finite} \land \exists \varphi: \mathsf{FreeGroup}(S) \to^* G, \operatorname{Surjective}(\varphi)$$$
Lean4
/-- A group is finitely generated iff there exists a surjective homomorphism from a `FreeGroup`
on finitely many generators. -/
@[to_additive /-- An additive group is finitely generated iff there exists a surjective homomorphism
from a `FreeAddGroup` on finitely many generators. -/
]
theorem fg_iff_exists_freeGroup_hom_surjective :
Group.FG G ↔ ∃ (S : Set G) (_ : S.Finite) (φ : FreeGroup S →* G), Function.Surjective φ :=
by
refine ⟨fun ⟨S, hS⟩ ↦ ⟨S, S.finite_toSet, FreeGroup.lift Subtype.val, ?_⟩, ?_⟩
· rwa [← MonoidHom.range_eq_top, ← FreeGroup.closure_eq_range]
· rintro ⟨S, hfin : Finite S, φ, hφ⟩
refine fg_iff.mpr ⟨φ '' Set.range FreeGroup.of, ?_, Set.toFinite _⟩
simp [← MonoidHom.map_closure, hφ, FreeGroup.closure_range_of, ← MonoidHom.range_eq_map]
