English
Let φ be a family of group homomorphisms φ_i: H → G_i indexed by ι, and let w be a word in the coproduct that is reduced with respect to φ. Then there exists a normal word w' in the transversal d such that the product of w' equals the image of w under the coproduct, and the sequence of first components (fst) of w' equals that of w.
Русский
Пусть φ — семейство гомоморфизмов φ_i: H → G_i, индексируемых ι, и пусть w — слово в копродукте, которое является сокращённым относительно φ. Тогда существует нормальное слово w' в переходе d такое, что prod(w') = ofCoprodI(prod(w)) и список первых компонент Sigma.fst у w' совпадает со списком Sigma.fst у w.
LaTeX
$$$\\exists w' : NormalWord d, w'.prod = ofCoprodI w.prod \\land w'.toList.map \\Sigma.fst = w.toList.map \\Sigma.fst$$$
Lean4
theorem exists_normalWord_prod_eq (d : Transversal φ) {w : Word G} (hw : Reduced φ w) :
∃ w' : NormalWord d, w'.prod = ofCoprodI w.prod ∧ w'.toList.map Sigma.fst = w.toList.map Sigma.fst := by
classical
induction w using Word.consRecOn with
| empty => exact ⟨empty, by simp, rfl⟩
| cons i g w hIdx hg1
ih =>
rcases ih (fun _ hg => hw _ (List.mem_cons_of_mem _ hg)) with ⟨w', hw'prod, hw'map⟩
refine ⟨cons g w' ?_ ?_, ?_⟩
· rwa [Word.fstIdx, ← List.head?_map, hw'map, List.head?_map]
· exact hw _ List.mem_cons_self
· simp [hw'prod, hw'map]
