closure_cycle_adjacent_swap — Mathlib

English

Let α be a finite set with a decidable equality. If σ ∈ Sym(α) is a cycle and its support equals the whole alphabet, then for every x ∈ α the subgroup generated by σ and the transposition exchanging x with σ(x) is the full symmetric group on α.

Русский

Пусть α – конечное множество с заданной эквивалентностью. Если σ ∈ Sym(α) цикл и опорa σ равна всей α, тогда для любого x ∈ α порождающая подгруппа, порожденная σ и транспозицией, меняющей x и σ(x), порождает всю симметрическую группу на α.

LaTeX

$$$\\forall \\alpha \\ [DecidableEq \\alpha] \ [Fintype \\alpha], \\forall \\sigma \\in Perm(\\alpha),\\ IsCycle(\\sigma),\\ σ.support = univ \\Rightarrow \\forall x \\in \\alpha,\\ closure({\\sigma, swap(x, \\sigma x)} : Set (Perm(\\alpha))) = \\top$$$

Lean4

theorem closure_cycle_adjacent_swap {σ : Perm α} (h1 : IsCycle σ) (h2 : σ.support = univ) (x : α) :
    closure ({σ, swap x (σ x)} : Set (Perm α)) = ⊤ :=
  by
  let H := closure ({σ, swap x (σ x)} : Set (Perm α))
  have h3 : σ ∈ H := subset_closure (Set.mem_insert σ _)
  have h4 : swap x (σ x) ∈ H := subset_closure (Set.mem_insert_of_mem _ (Set.mem_singleton _))
  have step1 : ∀ n : ℕ, swap ((σ ^ n) x) ((σ ^ (n + 1) : Perm α) x) ∈ H :=
    by
    intro n
    induction n with
    | zero => exact subset_closure (Set.mem_insert_of_mem _ (Set.mem_singleton _))
    | succ n ih =>
      convert H.mul_mem (H.mul_mem h3 ih) (H.inv_mem h3)
      simp_rw [mul_swap_eq_swap_mul, mul_inv_cancel_right, pow_succ', coe_mul, comp_apply]
  have step2 : ∀ n : ℕ, swap x ((σ ^ n) x) ∈ H := by
    intro n
    induction n with
    | zero =>
      simp only [pow_zero, coe_one, id_eq, swap_self]
      convert H.one_mem
    | succ n ih =>
      by_cases h5 : x = (σ ^ n) x
      · rw [pow_succ', mul_apply, ← h5]
        exact h4
      by_cases h6 : x = (σ ^ (n + 1) : Perm α) x
      · rw [← h6, swap_self]
        exact H.one_mem
      rw [swap_comm, ← swap_mul_swap_mul_swap h5 h6]
      exact H.mul_mem (H.mul_mem (step1 n) ih) (step1 n)
  have step3 : ∀ y : α, swap x y ∈ H := by
    intro y
    have hx : x ∈ univ := Finset.mem_univ x
    rw [← h2, mem_support] at hx
    have hy : y ∈ univ := Finset.mem_univ y
    rw [← h2, mem_support] at hy
    obtain ⟨n, hn⟩ := IsCycle.exists_pow_eq h1 hx hy
    rw [← hn]
    exact step2 n
  have step4 : ∀ y z : α, swap y z ∈ H := by
    intro y z
    by_cases h5 : z = x
    · rw [h5, swap_comm]
      exact step3 y
    by_cases h6 : z = y
    · rw [h6, swap_self]
      exact H.one_mem
    rw [← swap_mul_swap_mul_swap h5 h6, swap_comm z x]
    exact H.mul_mem (H.mul_mem (step3 y) (step3 z)) (step3 y)
  rw [eq_top_iff, ← closure_isSwap, closure_le]
  rintro τ ⟨y, z, _, h6⟩
  rw [h6]
  exact step4 y z

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