Boone–Higman theorem

TheoremBoone–Higman theorem (easy direction)#●ready to prove

Let \(\varphi \colon F_n \to G\) be a surjective homomorphism from the free group \(F_n\) on \(n\) generators onto a group \(G\). If there are injective homomorphisms \(G \to H\) and \(H \to K\), where \(H\) is a simple group and \(K\) is a finitely presented group, then the word problem of \(G\) with respect to \(\varphi\) is solvable.

public theorem_wanted 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 φ)
    : WordProblemSolvable φ

Sources

• 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. Problem boone_higman_embedding of the lean-eval benchmark.

Uses 1

Statement usesSolvable word problem

TheoremKuznetsov's theorem on finitely presented simple groups#●ready to prove

Let \(G\) be a simple group, let \(F_n\) be the free group on \(n\) generators, and let \(\varphi \colon F_n \to G\) be a surjective homomorphism whose kernel is the normal closure of finitely many elements. Then the word problem of \(G\) with respect to \(\varphi\) is solvable: there is an algorithm that decides, for every word \(w\) in the \(n\) generators and their inverses, whether \(\varphi(w) = 1\).

public theorem_wanted boone_higman_simple
    {G : Type*} [Group G] [IsSimpleGroup G]
    {n : ℕ} (φ : FreeGroup (Fin n) →* G)
    (_hsurj : Function.Surjective φ)
    (_hker : (MonoidHom.ker φ).IsFinitelyNormallyGenerated) :
    WordProblemSolvable φ

Sources

• A.V. Kuznetsov, 'Algorithms as operations in algebraic systems', Uspekhi Mat. Nauk 13 (1958) 240–241 (Russian); W.W. Boone and G. Higman, 'An algebraic characterization of groups with soluble word problem', J. Austral. Math. Soc. 18 (1974) 41–53. §122 in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf). Problem boone_higman_simple of the lean-eval benchmark.

Uses 1

Statement usesSolvable word problem

2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.