Finitely generated residually finite groups are Hopfian

Malcev's theorem: a surjective endomorphism f of a finitely generated residually finite group G is injective. Indeed, for a finite quotient π : G →* Q, precomposition with f is an injective self-map of the set G →* Q, which is finite because a finitely generated group has only finitely many homomorphisms to a finite one (Monoid.FG.finite_monoidHom). It is therefore a bijection, so π factors through f and kills its kernel. Residual finiteness then forces the kernel to be trivial. Free groups of finite rank are therefore Hopfian, which is how one recognizes that a surjection between free groups of the same finite rank is an isomorphism.

Main result

• Group.ResiduallyFinite.injective_of_surjective: a surjective endomorphism of a finitely generated residually finite group is injective.

References

• A. I. Malcev, On isomorphic matrix representations of infinite groups, Mat. Sb. 8 (50) (1940), 405–422.

theorem Group.ResiduallyFinite.injective_of_surjective {G : Type u_1} [Group G] [FG G] [ResiduallyFinite G] {f : G →* G} (hf : Function.Surjective ⇑f) : Function.Injective ⇑f

Malcev's theorem. A surjective endomorphism of a finitely generated residually finite group is injective: such a group is Hopfian.