A finitely presented group is presented on any finite generating set

Proved

GroupFiniteness.ker_isFinitelyNormallyGenerated_of_surjective

by dbenbenn · Sep 20, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatorial-group-theoryfinitely-presented-groupsgroup-theory

Let $C$ be a finitely presented group and let $\chi : F_n \to C$ be a surjective homomorphism from the free group on $n$ generators. Then $\ker \chi$ is the normal closure of a finite subset of $F_n$ , that is, $C$ is presented by the $n$ given generators subject to finitely many relations.

Being finitely presented asserts the existence of some finite presentation; this says the property does not depend on which finite generating set is chosen. Mathlib has the notion Subgroup.IsFinitelyNormallyGenerated (a subgroup that is the normal closure of a finite set) together with its behaviour under homomorphisms, and Group.IsFinitelyPresented, but not this independence.

Preamble

import Mathlib

Formal statement

namespace GroupFiniteness

/-- A finitely presented group is presented on *any* finite generating set, with finitely many
relations: if `C` is finitely presented and `χ : FreeGroup (Fin n) →* C` is surjective, then
`ker χ` is the normal closure of a finite set. This is the change-of-generators step of Tietze's
theorem (B. H. Neumann). Mathlib has `Subgroup.IsFinitelyNormallyGenerated` with its behaviour
under maps, and `Group.IsFinitelyPresented` asserting the existence of *some* such presentation,
but not the independence of the chosen generating set. -/
theorem ker_isFinitelyNormallyGenerated_of_surjective {C : Type*} [Group C]
    [Group.IsFinitelyPresented C] {n : ℕ} (χ : FreeGroup (Fin n) →* C)
    (hχ : Function.Surjective χ) : χ.ker.IsFinitelyNormallyGenerated := by
  sorry

end GroupFiniteness

Source

Standard change-of-generators (Tietze) fact for finitely presented groups. Cited as Kurosh, Theory of Groups, vol. II, p. 73 by Milnor, Growth of finitely generated solvable groups, Journal of Differential Geometry 2 (1968) 448, https://doi.org/10.4310/jdg/1214428659, in the proof of Lemma 2; this statement is not asserted in that form by Milnor's note, which uses it.

View graph