English
If two reduced words have the same φ-product, then their sequences of first components are equal, and the leading t-exponent heads lie in the same left coset of the appropriate subgroup determined by the first entries.
Русский
Если два редуцированых слова имеют одинаковый образ под φ, то их последовательности первых координат совпадают, а головные элементы относительно первых входов лежат в одной левой косете соответствующей подгруппы.
LaTeX
$$$\\forall w_1,w_2 : ReducedWord G A B, \n w_1.prod φ = w_2.prod φ \\Rightarrow \n (w_1.toList.map Prod.fst = w_2.toList.map Prod.fst) \\land\n \\forall u \\in w_1.toList.head?.map Prod.fst, \\, w_1.head^{-1} * w_2.head \\in toSubgroup A B (-u).$$$
Lean4
/-- Two reduced words representing the same element of the `HNNExtension G A B φ` have the same
length corresponding list, with the same pattern of occurrences of `t^1` and `t^(-1)`,
and also the `head` is in the same left coset of `toSubgroup A B (-u)`, where `u : ℤˣ`
is the exponent of the first occurrence of `t` in the word. -/
theorem map_fst_eq_and_of_prod_eq {w₁ w₂ : ReducedWord G A B} (hprod : w₁.prod φ = w₂.prod φ) :
w₁.toList.map Prod.fst = w₂.toList.map Prod.fst ∧
∀ u ∈ w₁.toList.head?.map Prod.fst, w₁.head⁻¹ * w₂.head ∈ toSubgroup A B (-u) :=
by
rcases TransversalPair.nonempty G A B with ⟨d⟩
rcases exists_normalWord_prod_eq φ d w₁ with ⟨w₁', hw₁'1, hw₁'2, hw₁'3⟩
rcases exists_normalWord_prod_eq φ d w₂ with ⟨w₂', hw₂'1, hw₂'2, hw₂'3⟩
have : w₁' = w₂' := NormalWord.prod_injective φ d (by dsimp only; rw [hw₁'1, hw₂'1, hprod])
subst this
refine ⟨by rw [← hw₁'2, hw₂'2], ?_⟩
simp only [← leftCoset_eq_iff] at *
intro u hu
rw [← hw₁'3 _ hu, ← hw₂'3 _]
rwa [← List.head?_map, ← hw₂'2, hw₁'2, List.head?_map]
