Suppose I have the group presentation $G=\langle x,y\ \ x^3=y^5=(yx)^2\rangle$. Now, $G$ is isomorphic to $SL(2,5)$ (see my proof here). This means the relation $x^6=1$ should hold in $G$. I was wondering if anyone knows how to derive that simply from the group presentation (not using central extensions, etc.). Even nicer would be an example of how software (GAP, Magma, Magnus, etc.) could automate that.

$\begingroup$ As Richard Kent pointed out in an answer I deleted, $yxy = x^2$, so $yx = x^2y^{1}$ and $yxyx = x^3 \implies yxx^2y^{1} = x^3$, so $x^3y = yx^3$. So all of the words in the relations of this presentation are in the center of $G$. $\endgroup$– Steve HuntsmanCommented Feb 13, 2010 at 18:05

$\begingroup$ Yeah that follows since $x^3=y^5$ implies $x^3$ is in both $<x>$ and $<y>$ which means it's centralized by both $x$ and $y$. $\endgroup$– Steve DCommented Feb 13, 2010 at 18:17

$\begingroup$ mathforum.org/kb/message.jspa?messageID=6963952&tstart=0 $\endgroup$– Steve HuntsmanCommented Feb 13, 2010 at 21:37
5 Answers
The theory (and practice) of automatic groups is the most generally useful systematic way to deal with these things. There is a nice package written by Derek Holt and his associates called kbmag (available for download here: http://www.warwick.ac.uk/~mareg/download/kbmag2/ ). There is a book "Word Processing in Groups" by Epstein, Cannon, Levy, Holt, Paterson and Thurston that describes the ideas behind this approach. It's not guaranteed to work (not all groups have an "automatic" presentation) but it is surprisingly effective.
I made up a short input file for kbmag, and it immediately came back with a "confluent" system of relations (a particular system which has a technical property that when you just do a series of string substitutions you always get the same answer no matter what order you do them in). For your edification, here they are (xi and yi are x^1 and yi^1 respectively, idWord is 1 [edited to show the derivations from kbmag):
#Initial equation number 1:
#x*xi > IdWord
#Initial equation number 2:
#xi*x > IdWord
#Initial equation number 3:
#y*yi > IdWord
#Initial equation number 4:
#yi*y > IdWord
#Initial equation number 5:
#y^4 > x^3*yi
#Initial equation number 6:
#y*x*y > x^2
#New equation number 7, from overlap 5, 3:
#x^3*yi^2>y^3
#New equation number 8, from overlap 4, 5:
#yi*x^3>y^4
#New equation number 9, from overlap 6, 3:
#x^2*yi>y*x
#New equation number 10, from overlap 4, 6:
#yi*x^2>x*y
#New equation number 11, from overlap 2, 7:
#xi*y^3>y*x*yi
#New equation number 12, from overlap 2, 9:
#xi*y*x>x*yi
#New equation number 13, from overlap 10, 1:
#x*y*xi>yi*x
#New equation number 14, from overlap 1, 11:
#x*y*x*yi>y^3
#New equation number 15, from overlap 11, 3:
#y*x*yi^2>xi*y^2
#New equation number 16, from overlap 12, 1:
#x*yi*xi>xi*y
#New equation number 17, from overlap 2, 13:
#xi*yi*x>y*xi
#New equation number 18, from overlap 4, 15:
#yi*xi*y^2>x*yi^2
#New equation number 19, from overlap 2, 16:
#xi^2*y>yi*xi
#New equation number 20, from overlap 17, 1:
#y*xi^2>xi*yi
#New equation number 21, from overlap 18, 3:
#x*yi^3>yi*xi*y
#New equation number 22, from overlap 19, 3:
#yi*xi*yi>xi^2
#New equation number 23, from overlap 2, 21:
#xi*yi*xi*y>yi^3
#New equation number 24, from overlap 23, 3:
#yi^4>xi*yi*xi
#New equation number 25, from overlap 3, 24:
#y*xi*yi*xi>yi^3
#New equation number 26, from overlap 25, 2:
#yi^3*x>y*xi*yi
#New equation number 27, from overlap 3, 26:
#y^2*xi*yi>yi^2*x
#New equation number 28, from overlap 27, 4:
#yi^2*x*y>y^2*xi
#New equation number 29, from overlap 3, 28:
#y^3*xi>yi*x*y
#New equation number 30, from overlap 29, 2:
#yi*x*y*x>y^3
#New equation number 31, from overlap 5, 5:
#y*x^3>x^3*y
#New equation number 32, from overlap 5, 6:
#y^3*x^2>x*y*x^2*y
#New equation number 33, from overlap 8, 7:
#yi*x*y^3>x*y^2*x*yi
#New equation number 34, from overlap 7, 8:
#y*x^2*y*x>x^2*y^3
#New equation number 35, from overlap 11, 6:
#y*x*yi*x*y>xi*y^2*x^2
#New equation number 36, from overlap 12, 9:
#xi*y^2*x>x*yi*x*yi
#New equation number 37, from overlap 10, 13:
#yi*x*yi*x>x*y^2*xi
#New equation number 38, from overlap 11, 15:
#y*x*yi*x*yi^2>xi*y^2*xi*y^2
#New equation number 39, from overlap 12, 16:
#xi*y*xi*y>x*yi^2*xi
#New equation number 40, from overlap 17, 13:
#y*xi*y*xi>xi*yi^2*x
#New equation number 41, from overlap 18, 15:
#yi*x*yi^2*xi*y>x*yi^2*x*yi^2
#New equation number 42, from overlap 18, 20:
#yi*xi*y*xi*yi>x*yi^2*xi^2
#New equation number 43, from overlap 19, 20:
#yi*xi^3>xi^3*yi
#New equation number 44, from overlap 17, 21:
#y*xi*yi^3>xi*yi^2*xi*y
#New equation number 45, from overlap 23, 20:
#yi^3*xi^2>xi*yi*xi^2*yi
#New equation number 46, from overlap 22, 24:
#yi*xi^2*yi*xi>xi^2*yi^3
#New equation number 47, from overlap 25, 19:
#yi^3*xi*y>y*xi*yi^2*xi
#New equation number 48, from overlap 22, 26:
#xi^2*yi^2*x>x*yi^2*xi^2
#New equation number 49, from overlap 27, 26:
#yi^2*x*yi^2*x>y*xi*yi^2*x*yi
#New equation number 50, from overlap 49, 1:
#y*xi*yi^2*xi*y>yi^2*x*yi^2
#New equation number 51, from overlap 7, 28:
#x^3*y^2*xi>y^2*x^2
#New equation number 52, from overlap 27, 28:
#yi*x*y^2*xi*y>y^2*xi*y^2*xi
#New equation number 53, from overlap 29, 12:
#yi*x*y^2*x>y^3*x*yi
#New equation number 54, from overlap 31, 7:
#x^3*y^2*x*yi>y*x^2*y^3
#New equation number 55, from overlap 32, 13:
#x*y*x^2*y^2*xi>y^3*x*yi*x
#New equation number 56, from overlap 32, 14:
#x*y*x^2*y^2*x*yi>y^2*x^2*y^2
#New equation number 57, from overlap 2, 56:
#y*x^2*y^2*x*yi>x^2*y^2*xi*y^2
#New equation number 58, from overlap 56, 4:
#y^2*x^2*y^3>x*y*x^2*y^2*x
#New equation number 59, from overlap 57, 4:
#x^2*y^3*x*yi>y*x^2*y^2*x
#New equation number 60, from overlap 33, 34:
#y^2*x^2*y^2*xi*y^2>x*y^2*x^2*y^2*x
#New equation number 61, from overlap 11, 35:
#x^2*y^2*xi*y^2*xi>y*x^2*y^2*xi*y
#New equation number 62, from overlap 35, 25:
#x*yi*x*yi^2*xi>xi*y^2*xi*y
#New equation number 63, from overlap 35, 32:
#x^2*y^2*x^2*y^2*xi>y*x^2*y^2*x^2*y
#New equation number 64, from overlap 33, 35:
#y^2*x^2*y^2*xi*y>yi*x*yi^2*x*yi^2
#New equation number 65, from overlap 64, 3:
#y^2*x^2*y^2>yi^2*x*yi^2
#New equation number 66, from overlap 4, 64:
#y*x^2*y^2*xi*y>xi*yi^2*x*yi^2*xi
#New equation number 67, from overlap 65, 3:
#y*x^2*y>xi*yi^2*xi
#New equation number 68, from overlap 4, 66:
#xi*y*xi*yi^2*xi>x^2*y^2*xi*y
#New equation number 69, from overlap 67, 3:
#xi*yi*xi^2>y*x^2
#New equation number 70, from overlap 4, 67:
#xi^2*yi*xi>x^2*y
#New equation number 71, from overlap 68, 2:
#x^2*y^2*x>xi*y*xi*yi
#New equation number 72, from overlap 1, 69:
#x*y*x^2>yi*xi^2
#New equation number 73, from overlap 69, 2:
#x^3*y>xi*yi*xi
#New equation number 74, from overlap 70, 2:
#x^2*y*x>xi^2*yi
#New equation number 75, from overlap 71, 1:
#xi*yi^3>x^2*y^2
#New equation number 76, from overlap 2, 71:
#yi*xi^2*yi>x*y^2*x
#New equation number 77, from overlap 72, 1:
#xi^3*yi>x*y*x
#New equation number 78, from overlap 73, 3:
#xi^3>x^3
#New equation number 79, from overlap 75, 4:
#x^2*y^3>xi*yi^2
#New equation number 80, from overlap 1, 78:
#x^4>xi^2
#New equation number 81, from overlap 2, 79:
#xi^2*yi^2>x*y^3
#New equation number 82, from overlap 29, 36:
#y^3*x*yi*x*yi>x*y^2*x*yi*x
#New equation number 83, from overlap 7, 37:
#y^3*x*yi*x>yi^2*xi*y*xi
#New equation number 84, from overlap 4, 83:
#xi*yi^2*xi^2>y*x*yi*x
#New equation number 85, from overlap 1, 84:
#yi^2*xi^2>y^3*x
#New equation number 86, from overlap 9, 37:
#yi^3*xi>y^2*x^2
#New equation number 87, from overlap 38, 8:
#x^2*y^2*xi*y^2>xi*yi^2*x*yi^2
#New equation number 88, from overlap 11, 38:
#xi*y^2*xi*y^2*xi*y>y^2*x*yi*x*yi^2
#New equation number 89, from overlap 88, 3:
#xi*y^2*xi*y^2*xi>y*xi*y^2*xi*y
#New equation number 90, from overlap 38, 37:
#y*xi*yi^2*x*yi^2*xi>yi*x*yi^2*x*yi^2
#New equation number 91, from overlap 39, 39:
#x*y^2*x^2>yi*xi*y*xi
#New equation number 92, from overlap 41, 39:
#yi*x*yi^2*x*yi^2*xi>x*yi*x*yi^2*x*yi^2
#New equation number 93, from overlap 42, 47:
#xi*y*xi*yi^2*x*yi^2>x*y^2*xi*y^2*xi*y
#New equation number 94, from overlap 93, 4:
#x*y^2*xi*y^2*xi*y^2>xi*y*xi*yi^2*x*yi
#New equation number 95, from overlap 2, 94:
#y^2*xi*y^2*xi*y^2>x*y^2*x*yi*x*yi
#68 eqns; total len: lhs, rhs = 299, 246; 77 states; 0 secs. max len: lhs, rhs = 8, 8.
#System is confluent.
#Halting with 68 equations. #Exit status is 0

$\begingroup$ I should add that kbmag also produces two finite state automata the first of which solves the word problem (i.e. given two words are they the same element) in time at most quadratic in the length of the words. By tracing how that automaton functions you will get a proof of your desired assertion. The second automaton tells you what happens when you add a generator onto the end of a word. $\endgroup$ Commented Feb 13, 2010 at 16:35

$\begingroup$ Hi Victor, can you explain a little bit more how this can be used to derive the identity? Also, does [x^2,xi] mean x^2 = xi? Because that's not true. $\endgroup$– Steve DCommented Feb 13, 2010 at 16:36

$\begingroup$ I followed your link, and found that the original question involved the group $\langle x,y  x^3 y^{5}, x^3 (y x)^2 \rangle$. I gave that presentation to kbmag and it came back with the answer that it was a finite group of cardinality 120, so it is isomorphic to $\text{SL}(2,5)$. $\endgroup$ Commented Feb 13, 2010 at 16:43

$\begingroup$ Yes, GAP is capable of telling me the group is $SL(2,5)$. I wanted to derive the relation $x^6=1$ from the presentation itself. That would entail either following GAP's calculations (probably very difficult) or doing something like you mentioned with the automaton (which sounds very interesting). $\endgroup$– Steve DCommented Feb 13, 2010 at 16:46

3$\begingroup$ @Steve: I just noticed when looking at the above system of equations that it had derived $x^3 = x^{3}$. I did rerun it with trace on and it gives the series of derivations (which can probably be edited down to only point to the relevant ones). $\endgroup$ Commented Feb 13, 2010 at 16:56
Let me give a totally useless pureexistence answer, while we wait for someone to show up with a better answer.
Namely, if it is true that those relations imply x^{6} = 1, then there definitely will be an elementary proof of this, using only the group axioms and the relations. That is, if it is true, then you can be confident that there is a elementary proof, involving just playing with group elements and equations in that group.
This is a consequence of Goedel's Completeness theorem, which says that every statement true in all models of a first order theory has a proof from that theory. In your case, if those relations imply that identity in all groups, then there will be a first order proof of this from the group axioms.
As for automating such questions, of course the word problem is undecidable, so in general it is impossible to automate the general question of determining whether a given identity is a consequence of a given set of relations.
But your question is not an instance of the word problem, since you are not asking whether the identity holds, but rather, you claim to know that it holds, and want an elementary proof of that. This problem is in principal computable. The reason is that the set of identities that hold in a given presentation is computably enumerableone can just search through the collection of all proofs, until the desired proof is found. Again, the completeness theorem ensures that there will be such a proof, and so there is a computable procedure to find it.
I apologize for my useless answer.

$\begingroup$ I like it! I do have a question about your last paragraph. The relations which hold in my group are a recursive set (is the same as what you said?), so is it also true the sequence of Tietze transformations to arrive at any relation is also a recursive set? So when you say "search through... all proofs", we can actually enumerate all possible paths to proving this relation? $\endgroup$– Steve DCommented Feb 13, 2010 at 16:06

$\begingroup$ Yes, if one has a computable (same as recursive=old fashioned terminology) set of axioms, then the set of theorems will be computably enumerable, since one can search through all possible proofs in a formal proof system. For example, one can computably enumerate all possible Tietze transformations, and if there is one leading to the desired identity, you will eventually find it, so this gives a computable procedure. Of course, this method is useless in practice, but it does show that the general problem is computable. The computer systems you mention, for example, use much better algorithms. $\endgroup$ Commented Feb 13, 2010 at 16:16

$\begingroup$ One could attack this with simulated annealing. Take $(2q)$ary strings representing presented elements of a group with $q$ generators, then run a parser to replace a substring chosen uniformly at random from the substrings in a (growable) database of words equal to the identity. If the resulting word is shorter, keep it. If it is longer, keep it with probability given by a Gibbs factor. Run this until you get your desired word in the database. Does anyone know if (something like) this might be more efficient than deterministic approaches? $\endgroup$ Commented Feb 13, 2010 at 16:32

2$\begingroup$ Goedel's completeness theorem for full firstorder logic certainly works, but we hardly need go that far. Of course if x^6 = 1, it can be derived from this presentation, and purely by equational/algebraic reasoning from the specified relations on the generators and (instances of) the group identities. Why? Because we can clearly take a quotient of the free group on these generators which imposes all and only the relations which can be derived in this manner, and, pretty much by definition, that resulting group is the one referred to by this presentation. $\endgroup$ Commented Feb 13, 2010 at 20:15

$\begingroup$ Sridhar, Yes, I agree. And I think there is a general universalalgebraic theorem along these lines also, about deriving equations from other equations. Yet, with both methods in the general case you basically have c.e. sets that are Turing equivalent to the halting problem, so there is a fundamental equivalence in the methods from the prespective of computability. $\endgroup$ Commented Feb 13, 2010 at 20:52
OK, here is the derivation, based completely on the amazing information provided by Victor Miller (who I should also thank for letting me know about kbmag). First, some identities:
(1) From $x^3=xyxy$ we get: (a) $x^2=yxy$; (b) $xyx^{1}=y^{1}x$; (c) $x^{1}yx=xy^{1}$.
(2) From $y^5=xyxy$ we get: (a) $y^4=xyx$; (b) $x^{1}y^3=yxy^{1}$; (c) $y^3x^{1}=y^{1}xy$.
(3) From (1a) and (3b) we get $(yxy)(yxy^{1})=(x^2)(x^{1}y^3) = xy^3$; so $xy^2xy^{1}=y^{1}xy^3$.
(4) From (2b) and (1b) we get $(yxy^{1})(xyx^{1}) = (x^{1}y^3)(y^{1}x) = x^{1}y^2x$, so that $yxy^{1}xy=x^{1}y^2x^2$.
(5) From (2c) we get $y^2x^{1}y^{1}=y^{2}x$; squaring that yields $y(yx^{1}yx^{1})y^{1}=y^{2}xy^{2}x$. (1c), inverse, squared, shows this is the same as $yx^{1}y^{2}xy^{1}=y^{2}xy^{2}x$.
(6) Similar to (5). From (2c) we get $y^2x^{1}=y^{2}xy$; squaring that yields $y^2x^{1}y^2x^{1}=y^{1}(y^{1}xy^{1}x)y$. (1b) squared shows this is the same as $y^2x^{1}y^2x^{1}=y^{1}xy^2x^{1}y$.
OK, now consider the word $(y^{1}xy^3)xy^{1}xy$. From (3) this is $xy^2x(y^{1}xy^{1}x)y$, which from (1b) squared is $xy^2x(xy^2x^{1})y=xy^2x^2y^2x^{1}y$.
This word can also be written as $y^{1}xy^2(yxy^{1}xy)$, which from (4) is $y^{1}xy^2(x^{1}y^2x^2)$. So the previous two computations show $y^2x^2y^2xy^{1}=x^{1}(y^{1}xy^2x^{1}y)yx^2$
$=x^{1}y^2x^{1}y^2(x^{1}yx)x$ ...... from (6)
$=x^{1}y^2(x^{1}y^2x)y^{1}x$ ....... from (1c)
$=(x^{1}y^2x)y^{1}xy^{2}x$ ......... from (1c) squared
$=xy^{1}x(y^{2}xy^{2}x)$ ........... from (1c) squared
$=xy^{1}(xyx^{1})y^{2}xy^{1}$ ..... from (5)
$=x(y^{2}xy^{2}x)y^{1}$ .............from (1b)
$=(xyx^{1})y^{2}xy^{2}$ ............ from (5)
$=y^{1}xy^{2}xy^{2}$ ............... from (1b).
So $y^2x^2y^2x^{1}y=y^{1}xy^{2}xy^{2}$, or $y^2x^2y^2=y^{1}xy^{2}xy^{3}x$. But $y^{1}xy^{2}x(y^{3}x)=y^{1}xy^{2}(xyx^{1})y^{1}=y^{1}x(y^{3}x)y^{1}=y^{1}(xyx^{1})y^{2}=y^{2}xy^{2}$ (through repeated application of (2b) inverse, and (1b)).
Thus $y^2x^2y^2=y^{2}xy^{2}$, or $y^4x^2y^4=x$, and from (2a) we get $xyx^4yx=x$, or $1=yx^4yx=(yxy)x^4=x^6$ (the second follows from $x^3$ being central and the third from (1a)).
Done!
This is a very basic answer to the last part of the question. One can derive the relation $x^6=1$ in gap and magma and even identify the group in this case. As a word of caution, these methods may break down depending on the automation one has in mind.
In gap:
gap> F:= FreeGroup(2); x:=F.1; y:=F.2;
<free group on the generators [ f1, f2 ]>
f1
f2
gap> G:= F/[x^3*y^5,x^3*(y*x)^2];
<fp group on the generators [ f1, f2 ]>
gap> Order(Subgroup(G,[G.1]));
6
To identify the whole group:
gap> Order(G); # note this line is not strictly necessary
120
gap> StructureDescription(G);
"SL(2,5)"
In magma, we can do the same operations:
> G<x,y>:=Group<x,yx^3=y^5=(y*x)^2>;
> Order(sub<Gx>);
6
> Order(G); # again this line is not strictly necessary
120
> IdentifyGroup(G);
<120, 5>
From here, you look up the group as the 5th group of order 120 in the small group data base (see http://magma.maths.usyd.edu.au/magma/handbook/text/703). In the alternative, you could put in your favorite presentation of $SL(2,5)$ and check that is it also group "<120, 5>."
It's a bit late answer, but there is a nice proof :).
Denote $t = x^3 = y^5$, so $t$ is in center of $G$. Add new symbol $u$ and state that it commutes with other symbols and $u^{30}=t$, so we obtain new group $E$ isomorphic to $Ext(C_{30},G)$. Now denote $a = u^{10}x, b=u^{6}y, c=u^{15}yx$. It is easy to check that $a^3=b^5=c^2=1$ and $bac=u$ in $E$. Denote $Q_1 = u^{1}ba, Q_2 =u^{1}ab$. You can check that $Q_1^2 = Q_2^2 = 1$. The next holds:
$$Q_1Q_2 = u^{2}b(a^2)b = u^{2}b(u^{2}bab)b = u^{4}b^2ab^2 = u^{4}b^2a(b^{1})b^3 = $$
$$= u^{4}b^2a(u^{2}aba)b^3 = u^{6}b^2a^2bab^3 = u^{6}(b^2a^2)b(b^2a^2)^{1}$$
Hence $(Q_1Q_2)^5=u^{30}=t$. But $(Q_2Q_1)^5 = Q_1(Q_1Q_2)^5Q_1 = t$ so $t^2=(Q_1Q_2)^5(Q_2Q_1)^5=1$ in $E$. Clearly, $t^2=1$ should holds in $G$ too.
The idea of this proof is from this article: "Scalar operators equal to the product of unitary roots of the identity operator", Yu. S. Samoilenko, D. Yu. Yakymenko, Ukrainian Mathematical Journal, November 2012, Volume 64, Issue 6, pp 938947.

$\begingroup$ Why is $E=\langle G,u\rangle$ isomorphic to $G\times C_{30}$, i.e. what is the generator of $C_{30}$ ? $\endgroup$– tj_Commented Sep 17, 2013 at 10:41

$\begingroup$ Yeah, it's just an extension $E = Ext(C_{30},G)$, not the product, my fault. But the idea is correct, adding relations $u^{30}=t, [u,x]=[u,y]=1$ doesn't affect relations between $x,y,t$. $\endgroup$– DanCommented Sep 17, 2013 at 11:40

$\begingroup$ I checked your computations  they look fine to me. But I wonder if there is some general idea or concept behind your proof (I haven't looked into the cited paper so far)? I'm asking because in the way it is presented the proof looks like "fallen from heaven" to me. $\endgroup$– tj_Commented Sep 17, 2013 at 12:33