English
Under ping-pong data for a family of groups H_i with homomorphisms f_i : H_i → G into a group G, the image of every nonempty reduced word w in the free product is not the identity. Consequently, the induced lift from the free product to G is injective.
Русский
При данных Пинг-Понга для семейства групп H_i с гомоморфизмами f_i : H_i → G в группу G образ любого непустого сокращенного слова w в свободном произведении не равен единице. Следовательно, получаемое отображение от свободного произведения в G инъективно.
LaTeX
$$$\forall i,j\; \forall w \in \mathrm{NeWord}(H,i,j): \ \mathrm{lift}(f)(w.\mathrm{prod}) \neq 1$$$
Lean4
theorem lift_word_prod_nontrivial_of_not_empty {i j} (w : NeWord H i j) : lift f w.prod ≠ 1 := by
classical
rcases hcard with hcard | hcard
· obtain ⟨i, h1, h2⟩ := Cardinal.three_le hcard i j
exact lift_word_prod_nontrivial_of_other_i f X hXnonempty hXdisj hpp w h1 h2
· obtain ⟨k, hcard⟩ := hcard
by_cases hh : i = k <;> by_cases hl : j = k
· subst hh
subst hl
exact lift_word_prod_nontrivial_of_head_eq_last f X hXnonempty hXdisj hpp w
· subst hh
change j ≠ i at hl
exact lift_word_prod_nontrivial_of_head_card f X hXnonempty hXdisj hpp w hcard hl.symm
· subst hl
change i ≠ j at hh
have : lift f w.inv.prod ≠ 1 :=
lift_word_prod_nontrivial_of_head_card f X hXnonempty hXdisj hpp w.inv hcard hh.symm
intro heq
apply this
simpa using heq
· change i ≠ k at hh
change j ≠ k at hl
exact lift_word_prod_nontrivial_of_other_i f X hXnonempty hXdisj hpp w hh.symm hl.symm
