English
Every finite symmetric group is generated by adjacent transpositions; in particular, the closure of adjacent swaps equals the full group.
Русский
Каждая конечная симметрическая группа порождается соседними транспозициями; замыкание соседних транспозиций даёт всю группу.
LaTeX
$$$ \\forall n,\\; \\mathrm{Submonoid}.closure(\\{ \\mathrm{swap} (i.castSucc) i.succ \\mid i : Fin n \\}) = \\top $$$
Lean4
/-- Every finite symmetric group is generated by transpositions of adjacent elements. -/
theorem mclosure_swap_castSucc_succ (n : ℕ) :
Submonoid.closure (Set.range fun i : Fin n ↦ swap i.castSucc i.succ) = ⊤ :=
by
apply top_unique
rw [← mclosure_isSwap, Submonoid.closure_le]
rintro _ ⟨i, j, ne, rfl⟩
wlog lt : i < j generalizing i j
· rw [swap_comm]; exact this _ _ ne.symm (ne.lt_or_gt.resolve_left lt)
induction j using Fin.induction with
| zero => cases lt
| succ j
ih =>
have mem : swap j.castSucc j.succ ∈ Submonoid.closure (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ) :=
Submonoid.subset_closure ⟨_, rfl⟩
obtain rfl | lts := (Fin.le_castSucc_iff.mpr lt).eq_or_lt
· exact mem
rw [swap_comm, ← swap_mul_swap_mul_swap (y := Fin.castSucc j) lts.ne lt.ne]
exact mul_mem (mul_mem mem <| ih lts.ne lts) mem
