Freeness detected by a quotient (source code)

= Freeness detected by a quotient

Suppose a <group homomorphism> $\pi:G\to Q$ is injective on a subgroup freely generated by $x_1,\ldots,x_n$. If $y_i$ have $\pi(y_i)=\pi(x_i)$, then the $y_i$ freely generate their subgroup: a relation among them projects to a relation among the free basis images, so the corresponding abstract reduced word must be empty. In particular, this applies to $y_i=x_ig$ when the <normal closure> of $g$ intersects $\langle x_1,\ldots,x_n\rangle$ trivially.