Boone–Higman theorem (easy direction)

boone_higman_embedding

Submitter: Kim Morrison.

Notes: If a finitely presented group G embeds in a simple group H that embeds in a finitely presented group K, then G has a solvable word problem — the 'if' half of the Boone–Higman characterisation. Trusted helper WordProblemSolvable (non-hole) via ComputablePred. Mathlib has finitely-presented/free/simple groups and computability but no word-problem notion or Boone–Higman theorem. The main Kuznetsov/Boone–Higman, Novikov, and Higman-infinite-simple statements of §122 are already in lean-eval. Candidate from §122 (additional 1).

Source: W. W. Boone & G. Higman, *An algebraic characterization of groups with soluble word problem*, J. Austral. Math. Soc. 18 (1974). Knill, *Some fundamental theorems in mathematics*, §122.

Informal solution: The easy direction. Embed G ↪ H ↪ K with H simple and K finitely presented. The word problem of K is recursively enumerable from its finite presentation (enumerate consequences of the relators). Words of G equal to 1 are those mapping to 1 in K (via the composite injection), which is r.e.; words not equal to 1 are detected through the simple group H: adjoining a nontrivial element as a relator collapses H, making 'w ≠ 1' also r.e. Both r.e. ⇒ decidable, so G's word problem is solvable. Uses the Kuznetsov/Boone–Higman recursively-enumerable-from-both-sides argument (r.e. equality from K's finite presentation, r.e. inequality from H simple), absent from Mathlib.

theorem declaration uses `sorry`boone_higman_embedding {G H K : Type*} [Group G] [Group H] [Group K]
    [IsSimpleGroup H] [Group.IsFinitelyPresented K]
    (f : G →* H) (hf : Function.Injective f)
    (g : H →* K) (hg : Function.Injective g)
    {n : ℕ} (φ : FreeGroup (Fin n) →* G)
    (hsurj : Function.Surjective φ)
    (hker : (MonoidHom.ker φ).IsNormalClosureFG) :
    LeanEval.GroupTheory.BooneHigmanEmbedding.WordProblemSolvable φ := byG:Type u_1H:Type u_2K:Type u_3inst✝⁴:Group Ginst✝³:Group Hinst✝²:Group Kinst✝¹:IsSimpleGroup Hinst✝:Group.IsFinitelyPresented Kf:G →* Hhf:Function.Injective ⇑fg:H →* Khg:Function.Injective ⇑gn:ℕφ:FreeGroup (Fin n) →* Ghsurj:Function.Surjective ⇑φhker:φ.ker.IsNormalClosureFG⊢ WordProblemSolvable φ
  sorryAll goals completed! 🐙

Solved by

• @GanjinZero with Seed Prover (ByteDance) on Jun 10, 2026