exists_normalWord_prod_eq — Mathlib

English

For a transversal d and a reduced word w in the HNN extension, there exists a normal word w' with the same image under φ as w, and matching first-coordinate structure; moreover, the head of w' relates to the head of w via a subgroup condition tied to the first entry of w.

Русский

Для трансверсала d и редуцированного слова w в HNN-расширении существует нормальное слово w' с тем же изображением под φ, как и w, и совпадающей структурой первых координат; более того, голова w' связана со головой w через условие подгруппы, зависящее от первого элемента в w.

LaTeX

$$$\\exists w' : NormalWord(d),\n w'.prod φ = w.prod φ \\land\n w'.toList.map Prod.fst = w.toList.map Prod.fst \\land\n \\forall u \\in w.toList.head?.map Prod.fst,\, w'.head ∈ toSubgroup A B (-u).$$$

Lean4

theorem exists_normalWord_prod_eq (d : TransversalPair G A B) (w : ReducedWord G A B) :
    ∃ w' : NormalWord d,
      w'.prod φ = w.prod φ ∧
        w'.toList.map Prod.fst = w.toList.map Prod.fst ∧
          ∀ u ∈ w.toList.head?.map Prod.fst, w'.head⁻¹ * w.head ∈ toSubgroup A B (-u) :=
  by
  suffices
    ∀ w : ReducedWord G A B,
      w.head = 1 →
        ∃ w' : NormalWord d,
          w'.prod φ = w.prod φ ∧
            w'.toList.map Prod.fst = w.toList.map Prod.fst ∧
              ∀ u ∈ w.toList.head?.map Prod.fst, w'.head ∈ toSubgroup A B (-u)
    by
    by_cases hw1 : w.head = 1
    · simp only [hw1, inv_mem_iff, mul_one]
      exact this w hw1
    · rcases this ⟨1, w.toList, w.chain⟩ rfl with ⟨w', hw'⟩
      exact ⟨w.head • w', by simpa [ReducedWord.prod, mul_assoc] using hw'⟩
  intro w hw1
  rcases w with ⟨g, l, chain⟩
  dsimp at hw1; subst hw1
  induction l with
  | nil =>
    exact
      ⟨{  head := 1
          toList := []
          mem_set := by simp
          chain := List.isChain_nil }, by simp⟩
  | cons a l ih =>
    rcases ih (List.isChain_cons'.1 chain).2 with ⟨w', hw'1, hw'2, hw'3⟩
    clear ih
    refine ⟨(t ^ (a.1 : ℤ) * of a.2 : HNNExtension G A B φ) • w', ?_, ?_⟩
    · rw [prod_smul, hw'1]
      simp [ReducedWord.prod]
    · have : ¬Cancels a.1 (a.2 • w') :=
        by
        simp only [Cancels, group_smul_head, group_smul_toList, Option.map_eq_some_iff, Prod.exists, exists_and_right,
          exists_eq_right, not_and, not_exists]
        intro hS x hx
        have hx' := congr_arg (Option.map Prod.fst) hx
        rw [← List.head?_map, hw'2, List.head?_map, Option.map_some] at hx'
        have : w'.head ∈ toSubgroup A B a.fst := by simpa using hw'3 _ hx'
        rw [mul_mem_cancel_right this] at hS
        have : a.fst = -a.fst := by
          have hl : l ≠ [] := by rintro rfl; simp_all
          have : a.fst = (l.head hl).fst := (List.isChain_cons'.1 chain).1 (l.head hl) (List.head?_eq_head _) hS
          rwa [List.head?_eq_head hl, Option.map_some, ← this, Option.some_inj] at hx'
        simp at this
      rw [List.map_cons, mul_smul, of_smul_eq_smul, NormalWord.group_smul_def, t_pow_smul_eq_unitsSMul, unitsSMul]
      erw [dif_neg this]
      rw [← hw'2]
      simp [mul_assoc, unitsSMulGroup]

Похожие утверждения