# Group presentation in the category of finite group

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

1. $$\{g(i) | i \in I\}$$ generate $$G$$;
2. The relations $$R$$ holds in $$G$$, that is for any $$r\in R$$, then $$\prod_{i : r} g(i) = 1$$;
3. 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'$$ ?

 added ($$R$$ and $$I$$ finite in the above rephasing).

• The groups satisfying such a property are the quotient of the group $H$ defined by this presentation (in the usual sense) by normal subgroups that are contained in the finite residual (=intersection of finite index subgroups of $H$).
– YCor
Oct 15 at 9:10
• Your rephrased question is equivalent to whether every group is residually finite (take $H=1$).
– YCor
Oct 15 at 9:13
• @YCor: So I guess my question is : is any finite group residually finite. Wikipedia claims it is. Do you have any reference for that ? I'm coming from algebraic combinatorics and I'm mostly knowledgable in Coxeter groups where it goes to group theory. Oct 15 at 9:18
• @YCor: I should have written one or two more finite in the rephrasing ! Anyway having an infinite presentation (either in the generator or the relations) for a finite group seems to be silly to me... Oct 15 at 13:34
• @hivert but the core of the issue in your question lies in presentations of the trivial group. So no, it's definitely not silly and let me give an example: generators $h_n=1$ ($n\ge 0$), with relators $h_{n+1}^2=h_n$ $\forall n\ge 0$ and $h_0^2=1$. Then such relators in a finite group force $h_0=1$ (and, by induction force $h_n=1$ for all $n$). But $h_0=1$ does not formally follow from these relators, since it is easy to find an infinite group with such elements with these relations, but $h_0\neq 1$.
– YCor
Oct 15 at 14:20

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.
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$$.