English
Under the ping-pong hypotheses, the lift map from the free product to G is injective.
Русский
При выполнении условий Пинг-Понг отображение lift из свободного произведения в G инъективно.
LaTeX
$$$\operatorname{Injective}(\mathrm{lift}(f))$$$
Lean4
/-- The **Ping-Pong-Lemma**.
Given a group action of `G` on `X` so that the `H i` acts in a specific way on disjoint subsets
`X i` we can prove that `lift f` is injective, and thus the image of `lift f` is isomorphic to the
free product of the `H i`.
Often the Ping-Pong-Lemma is stated with regard to subgroups `H i` that generate the whole group;
we generalize to arbitrary group homomorphisms `f i : H i →* G` and do not require the group to be
generated by the images.
Usually the Ping-Pong-Lemma requires that one group `H i` has at least three elements. This
condition is only needed if `# ι = 2`, and we accept `3 ≤ # ι` as an alternative.
-/
theorem lift_injective_of_ping_pong : Function.Injective (lift f) := by
classical
apply (injective_iff_map_eq_one (lift f)).mpr
rw [(CoprodI.Word.equiv).forall_congr_left]
intro w Heq
dsimp [Word.equiv] at *
rw [empty_of_word_prod_eq_one f hcard X hXnonempty hXdisj hpp Heq, Word.prod_empty]
