English
There is a natural equivalence between NormalWord d and Pair d i for each i, giving a bijection between reduced words and their head-tail representations.
Русский
Существует естественное эквивалентное соответствие между NormalWord d и Pair d i для каждого i, образующее биекцию между нормализованными словами и их представлениями головы и хвоста.
LaTeX
$$$$\\text{equivPair}(i) : \\mathrm{NormalWord}\, d \\simeq \\mathrm{Pair}\, d\, i.$$$$
Lean4
/-- The equivalence between `NormalWord`s and pairs. We can turn a `NormalWord` into a
pair by taking the head of the `List` if it is in `G i` and multiplying it by the element of the
base group. -/
noncomputable def equivPair (i) : NormalWord d ≃ Pair d i :=
letI toFun : NormalWord d → Pair d i := fun w =>
letI p := Word.equivPair i (CoprodI.of (φ i w.head) • w.toWord)
{ toPair := p
normalized := fun j g hg => by
dsimp only [p] at hg
rw [Word.of_smul_def, ← Word.equivPair_symm, Equiv.apply_symm_apply] at hg
dsimp at hg
exact w.normalized _ _ (Word.mem_of_mem_equivPair_tail _ hg) }
haveI leftInv : Function.LeftInverse (rcons i) toFun := fun w =>
ext_smul i <| by
simp only [toFun, rcons, Word.equivPair_symm, Word.equivPair_smul_same, Word.equivPair_tail_eq_inv_smul,
Word.rcons_eq_smul, MonoidHom.apply_ofInjective_symm, equiv_fst_eq_mul_inv, mul_assoc, map_mul, map_inv,
mul_smul, inv_smul_smul, smul_inv_smul]
{ toFun := toFun
invFun := rcons i
left_inv := leftInv
right_inv := fun _ => rcons_injective (leftInv _) }
