English
Let w be an element of the word container CoprodI.Word G. If, for a fixed index i and an element h in the base group H, all letters of w lie in the transversal in the sense that each letter ⟨i,g⟩ belongs to d.set i, and if multiplying w by φ i h on the left preserves this transversal property for every place j (i.e., each letter ⟨j,g⟩ in CoprodI.of (φ i h) • w lies in d.set j), then h must be the identity element 1 in H.
Русский
Пусть w — элемент слова CoprodI.Word G. Для фиксированного индекса i и элемента h в базовой группе H, если все буквы w лежат во transversal (то есть каждая буква ⟨i,g⟩ принадлежит d.set i), и если при умножении слева на w элемент φ i h сохраняет это свойство transversal для каждой позиции j (то есть каждая буква ⟨j,g⟩ в CoprodI.of (φ i h) • w принадлежит d.set j), тогда h равно единице 1.
LaTeX
$$$$\forall w : \mathrm{CoprodI.Word} \, G, \forall i : \iota, \forall h : H,\\[2mm] (\forall i,g,\langle i,g\rangle \in w.toList \Rightarrow g \in d.set i) \,\wedge\, (\forall j,g,\langle j,g\rangle \in (\mathrm{CoprodI.of}(\phi i h) \cdot w).toList \Rightarrow g \in d.set j) \Rightarrow h = 1.$$$$
Lean4
/-- Given a word in `CoprodI`, if every letter is in the transversal and when
we multiply by an element of the base group it still has this property,
then the element of the base group we multiplied by was one. -/
theorem eq_one_of_smul_normalized (w : CoprodI.Word G) {i : ι} (h : H) (hw : ∀ i g, ⟨i, g⟩ ∈ w.toList → g ∈ d.set i)
(hφw : ∀ j g, ⟨j, g⟩ ∈ (CoprodI.of (φ i h) • w).toList → g ∈ d.set j) : h = 1 :=
by
simp only [← (d.compl _).equiv_snd_eq_self_iff_mem (one_mem _)] at hw hφw
have hhead : ((d.compl i).equiv (Word.equivPair i w).head).2 = (Word.equivPair i w).head :=
by
rw [Word.equivPair_head]
split_ifs with h
· rcases h with ⟨_, rfl⟩
exact hw _ _ (List.head_mem _)
· rw [equiv_one (d.compl i) (one_mem _) (d.one_mem _)]
by_contra hh1
have := hφw i (φ i h * (Word.equivPair i w).head) ?_
· apply hh1
rw [equiv_mul_left_of_mem (d.compl i) ⟨_, rfl⟩, hhead] at this
simpa [((injective_iff_map_eq_one' _).1 (d.injective i))] using this
· simp only [Word.mem_smul_iff, not_true, false_and, ne_eq, Option.mem_def, mul_right_inj, exists_eq_right',
mul_eq_left, exists_prop, true_and, false_or]
constructor
· intro h
apply_fun (d.compl i).equiv at h
simp only [Prod.ext_iff, equiv_one (d.compl i) (one_mem _) (d.one_mem _),
equiv_mul_left_of_mem (d.compl i) ⟨_, rfl⟩, hhead, Subtype.ext_iff, Prod.ext_iff] at h
rcases h with ⟨h₁, h₂⟩
rw [h₂, equiv_one (d.compl i) (one_mem _) (d.one_mem _)] at h₁
erw [mul_one] at h₁
simp only [((injective_iff_map_eq_one' _).1 (d.injective i))] at h₁
contradiction
· rw [Word.equivPair_head]
dsimp
split_ifs with hep
· rcases hep with ⟨hnil, rfl⟩
rw [head?_eq_head hnil]
simp_all
· push_neg at hep
by_cases hw : w.toList = []
· simp [hw, Word.fstIdx]
· simp [head?_eq_head hw, Word.fstIdx, hep hw]
