Residual finiteness of semidirect products (source code)

= Residual finiteness of semidirect products

If $K$ is a <finitely generated group>, then the <semidirect product> $K\rtimes H$ is a <residually finite group> exactly when both $K$ and $H$ are <residually finite groups>. To separate an element whose $H$ coordinate is nontrivial, use a finite quotient of $H$. For $1\ne k\in K$, choose a finite-index normal subgroup $U$ omitting $k$, and intersect all subgroups of index at most $[K:U]$ to obtain a characteristic finite-index subgroup $C\leq U$. The induced map into $(K/C)\rtimes\operatorname{im}(H\to\operatorname{Aut}(K/C))$ has finite target and separates $k$. More generally, finite generation can be replaced by a separating family of finite-index normal subgroups invariant under the given $H$ action.