English
A permutation lies in the closure generated by a set of swaps if and only if it has finite fixed-by complement and preserves orbit structure.
Русский
Перестановка принадлежит замыканию множества транспозиций тогда и только тогда, когда её дополнение к фиксированию конечной, и она сохраняет орбиту.
LaTeX
$$$f \\in closure S \\iff (fixedBy \\ α f)^{c}.Finite ∧ ∀ x, f x ∈ orbit(closure S) x$$$
Lean4
/-- If a subgroup is generated by transpositions, then a transposition `swap x y` lies in the
subgroup if and only if `x` lies in the same orbit as `y`. -/
theorem swap_mem_closure_isSwap {S : Set (Perm α)} (hS : ∀ f ∈ S, f.IsSwap) {x y : α} :
swap x y ∈ closure S ↔ x ∈ orbit (closure S) y :=
by
refine ⟨fun h ↦ ⟨⟨swap x y, h⟩, swap_apply_right x y⟩, fun hf ↦ ?_⟩
by_contra h
have :=
exists_smul_notMem_of_subset_orbit_closure S {x | swap x y ∈ closure S} (fun f hf ↦ ?_) (fun z hz ↦ ?_) h ⟨y, ?_⟩
· obtain ⟨σ, hσ, a, ha, hσa⟩ := this
obtain ⟨z, w, hzw, rfl⟩ := hS σ hσ
have := ne_of_mem_of_not_mem ha hσa
rw [Perm.smul_def, ne_comm, swap_apply_ne_self_iff, and_iff_right hzw] at this
refine hσa (SubmonoidClass.swap_mem_trans (closure S) ?_ ha)
obtain rfl | rfl := this <;> simpa [swap_comm] using subset_closure hσ
· obtain ⟨x, y, -, rfl⟩ := hS f hf; rwa [swap_inv]
· exact orbit_eq_iff.mpr hf ▸ ⟨⟨swap z y, hz⟩, swap_apply_right z y⟩
· rw [mem_setOf, swap_self]; apply one_mem
