I haven’t posted any research in ages! I haven’t done any research in ages! Here’s a rewriting of a theorem from Ronald Gatterdam’s doctoral thesis, in more sensible language. I’ve proved the same theorem for fundamental groups of graphs of groups.
The main problem with Gatterdam’s proof was that he didn’t invent any new notation to make life simpler, so he wrote out pages and pages of very repetitive function applications.
I’ve made up a lot of notation to make dealing with functions in the Grzegorczyk hierarchy a lot easier, so you’ll probably need to refer to my draft paper for a few things. I keep all my research notes in a repository on github, by the way.
Theorem
Let be -computable groups. Let be -decidable subgroups of the latter. Let be an isomorphism, with both -computable.
Then the free product of and with and amalgamated, , is -computable.
Proof
Let be the index of and be the index of . The dashes will be explained later.
We can assume, without loss of generality, that and for . (Might not even need this.)
By Magnus, Karrass, Solitar, etc., all elements have normal form
where , and the are coset representatives of , , such that .
The following proof becomes a lot easier if we redefine the factor group indices as follows:
Now,
The subgroup isomorphism also needs to be redefined:
In order to do multiplication, we need to be able to split every , , into a word of the form , where and is a coset representative of in .
Define:
Now we can define by
(encode it as a Gödel number)
is -decidable because if and only if:
- is a Gödel number
- ,
- , .
Now define a function which does multiplication of elements of on the left by elements of and .
is defined by cases in a decision tree, so here’s some programming-ish syntax:
If {}
If {}
else
If {}
If { }
else
endif
else
endif
endif
else
If { }
else
If { }
If { }
else
endif
else
endif
endif
endif
Now we can do multiplication on in general:
And inversion:
( means a list of the form . I borrowed this syntax from Haskell. I need to show that you can define recursive functions on lists like this, but I hope you agree it works)
The functions and are defined recursively. Because we don’t know anything about how quickly the original multiplication functions grow, the recursion is unbounded, so the best we can do is to say that the index of is at worst -computable.
QED
Gatterdam also shows that the embeddings are natural, but I lost the will.
Comments
Comments
David Roberts
‘Free product with amalgamation’, also known an a pushout of groups. 🙂 This result is really quite useful for computing homotopy groups using the van Kampen theorem, which states that given a pushout of pointed spaces space with all maps open embeddings, and all spaces path connected, then the fundamental group of the pushout is the pushout of the fundamental groups. I have no idea what ‘E^n computable’ means, but I’m sure it is nice!