English
If the injectivity condition holds for all indices i, and w is a reduced word, and the image of w under the base inclusion lies in the base range, then w must be the empty word.
Русский
Пусть выполняется условие иньекции для всех индексов i, и w — сокращённое слово; если образ w под базовым включением лежит в диапазоне базы, то w равно пустому слову.
LaTeX
$$$\\bigl(\\forall i,\\; \\text{Injective}(\\phi_i)\\bigr) \\Rightarrow \\, (w: \\mathrm{Word}\; G) \\,\\land \\, \\mathrm{Reduced} \\; \\phi\\; w \\land\; ofCoprodI(w.prod) \\in (\\mathrm{base}\\; \\phi).\\mathrm{range} \\Rightarrow w = \\empty$$$
Lean4
/-- For any word `w` in the coproduct,
if `w` is reduced (i.e none its letters are in the image of the base monoid), and nonempty, then
`w` itself is not in the image of the base group. -/
theorem eq_empty_of_mem_range (hφ : ∀ i, Injective (φ i)) {w : Word G} (hw : Reduced φ w)
(h : ofCoprodI w.prod ∈ (base φ).range) : w = .empty :=
by
rcases transversal_nonempty φ hφ with ⟨d⟩
rcases hw.exists_normalWord_prod_eq d with ⟨w', hw'prod, hw'map⟩
rcases h with ⟨h, heq⟩
have : (NormalWord.prod (d := d) ⟨.empty, h, by simp⟩) = base φ h := by simp [NormalWord.prod]
rw [← hw'prod, ← this] at heq
suffices w'.toWord = .empty by
simp [this, @eq_comm _ []] at hw'map
ext
simp [hw'map]
rw [← prod_injective heq]
