Context: I'm trying to deal with presentations in the framework of Gonthier et al. formalization of the group theory in the proof assistant Coq. It was used to machine check the Feit-Thompson odd order theorem. In this formalisation, all groups are assumed to be finite and it would be a lot of work to remove the assumption. Actually, roughly speaking, all sets are assumed to be finite.
Summary question: Is there a finite group $G$ with a presentation where one of the relation can be deduced by the kownledge that $G$ is finite.
I'd like to define a presentation as follows:
Let $I$ be a finite set and $R$ be a finite collection of word in $I$. For any finite group $G$, and any map $g:I\to G$, I say that $(g, R)$ is a presentation of $G$ iff
- $\{g(i) | i \in I\}$ generate $G$;
- The relations $R$ holds in $G$, that is for any $r\in R$, then $\prod_{i : r} g(i) = 1$;
- For any finite group $H$ and any map $h : I \to H$, if $\prod_{i : r} h(i) = 1$ holds for any $r\in R$, then there is a group morphism $\phi : G \to H$ such that $\phi(g(i))=h(i)$ for all $i\in I$.
Allow me to stress once again that the universal properties of condition 3. only holds for finite groups.
My question is: does this coincide whith the usual definition of presentation ?
In particular, I'd like to prove that any word in the $\{g(i)\}$ is $1$ if it can be written as a concatenation of relators or their conjugates. But in order to do that I usually need to consider the quotient of the free group by the normal subgroup generated by the relators. However to prove that this quotient is finite, I need the exact propoerty I'm trying to prove.
Here is a rephrasing of my question:
Suppose that a finite group $H$ verify some relations $R$ ($R$ finite) on some generators $h_i$ ($I$ finite). Suppose that a word $w$ in the $h_i$ is equal to $1$ in $H$ but can't be written as a concatenation of the conjugate of the relators in $R$. Does there always exists a finite group $H'$ such that $H$ is a homomorphic image of $H'$ but $w$ is not $1$ in $H'$ ?
[edit] added ($R$ and $I$ finite in the above rephasing).
Best Answer
A well-known example, due to G. Higman, of an infinite finitely presented group with no nontrivial finite quotients is $$G = \langle a,b,c,d \mid a^{-1}ba=b^2,b^{-1}cb=c^2,c^{-1}dc=d^2,d^{-1}ad=a^2 \rangle.$$ Proving it has no nontrivial finite quotients is elementary and a nice exercise. The idea is to prove that $f(a) < f(b) < f(c) < f(d) < f(a)$, where $f(g)$ is the smallest prime factor of the order of $g$ in a candidate for a nontrivial finite quotient.
Proving it infinite can be done using the fact that the group is an amalgamated product of two HNN extensions: see here for example.
But according to your definition of a presentation of a finite group, this presentation would define the trivial group, because there are no other finite homomorphic images of $G$.
So the answer to your question is no, your definition of a presentation of a finite group is not equivalent to the standard notion of a group presentation.