English
We can form a new normal word by prepending a pair head,tail to an existing word, after normalizing the head into the base group and transversal form; this defines a canonical construction rcons.
Русский
Можно получить новое нормальное слово, прицепив в начало пару head, tail к уже существующему слову, после приведения головы к базовой группе и формa transversal; это определение rcons.
LaTeX
$$$$\\text{noncomputable def } rcons(i)(p) : \\mathrm{NormalWord}\, d \\text{ is obtained by normalizing } p.head \\text{ and forming } w := (\\text{Word.equivPair } i)^{-1} \\{ p.toPair with head := p^{\\text{head}} \\}.$$$$
Lean4
/-- Given a pair `(head, tail)`, we can form a word by prepending `head` to `tail`, but
putting head into normal form first, by making sure it is expressed as an element
of the base group multiplied by an element of the transversal. -/
noncomputable def rcons (i : ι) (p : Pair d i) : NormalWord d :=
letI n := (d.compl i).equiv p.head
let w := (Word.equivPair i).symm { p.toPair with head := n.2 }
{ toWord := w
head := (MonoidHom.ofInjective (d.injective i)).symm n.1
normalized := fun i g hg => by
dsimp [w] at hg
rw [Word.equivPair_symm, Word.mem_rcons_iff] at hg
rcases hg with hg | ⟨_, rfl, rfl⟩
· exact p.normalized _ _ hg
· simp }
