English
Let α be a finite set with a decidable equality. If σ is a cycle with full support and n is coprime to |α|, then for every x the subgroup generated by σ and swap x with (σ^n)(x) is the full symmetric group on α.
Русский
Пусть α – конечное множество с разрешённым равенством. Пусть σ – цикл с полной опорой и n взаимно простое с |α|; тогда для каждого x порождающая подгруппа, порождённая σ и обменом x с (σ^n)(x), есть всю симметрическую группу на α.
LaTeX
$$$\\forall \\alpha\\ [DecidableEq \\alpha] [Fintype \\alpha], \\forall n, \\forall \\sigma \\in Perm(\\alpha),\\ Nat.Coprime n (Fintype.card \\alpha) ∧ IsCycle(\\sigma) ∧ σ.support = univ ⟹ closure({\\sigma, swap(x, (\\sigma^n) x)} : Set (Perm(\\alpha))) = \\top$$$
Lean4
theorem closure_cycle_coprime_swap {n : ℕ} {σ : Perm α} (h0 : Nat.Coprime n (Fintype.card α)) (h1 : IsCycle σ)
(h2 : σ.support = Finset.univ) (x : α) : closure ({σ, swap x ((σ ^ n) x)} : Set (Perm α)) = ⊤ :=
by
rw [← Finset.card_univ, ← h2, ← h1.orderOf] at h0
obtain ⟨m, hm⟩ := exists_pow_eq_self_of_coprime h0
have h2' : (σ ^ n).support = univ := Eq.trans (support_pow_coprime h0) h2
have h1' : IsCycle ((σ ^ n) ^ (m : ℤ)) := by rwa [← hm] at h1
replace h1' : IsCycle (σ ^ n) := h1'.of_pow (le_trans (support_pow_le σ n) (ge_of_eq (congr_arg support hm)))
rw [eq_top_iff, ← closure_cycle_adjacent_swap h1' h2' x, closure_le, Set.insert_subset_iff]
exact
⟨Subgroup.pow_mem (closure _) (subset_closure (Set.mem_insert σ _)) n,
Set.singleton_subset_iff.mpr (subset_closure (Set.mem_insert_of_mem _ (Set.mem_singleton _)))⟩
