OAI.SimpleFInftyOvergroups.main

For a group G, a word in generators g₀,…,g_{n-1} is a list of pairs (i,b), each standing for g_i if b is true and for g_i⁻¹ if false, and evalWord multiplies these letters in order. HasDecidableWordProblem(G) is the proposition that there exist n and elements g₀,…,g_{n-1} of G generating G (the closure of their range is the whole group) such that the set of words evaluating to the identity is a computable predicate. HasTypeFInfty(H) is the proposition that there is a Hausdorff, connected topological space X carrying a CW complex structure on all of X of finite type, with a basepoint x such that H is isomorphic as a group to the fundamental group of X at x, and a surjective covering map p from some space E onto X with E contractible. The theorem states that for every finitely generated group G, in a universe u, that has decidable word problem in this sense, there exist a group H in the same universe that is nontrivial and simple and has type F∞ in this sense, together with an injective group homomorphism from G into H.