English
If a finite set S of swaps generates a pretransitive permutation action, then the corresponding permutation homomorphism is surjective onto the full symmetric group.
Русский
Если конечный набор транспозиций порождает предпереносимое действие перестановок, то соответствующий гомоморфизм на перестановки сюрьективен на полной симметрической группе.
LaTeX
$$$\\text{surjective}((MulAction.toPermHom)\\ G \\alpha) = \\top$$$
Lean4
/-- A transitive permutation group generated by transpositions must be the whole symmetric group -/
theorem surjective_of_isSwap_of_isPretransitive [Finite α] (S : Set G)
(hS1 : ∀ σ ∈ S, Perm.IsSwap (MulAction.toPermHom G α σ)) (hS2 : Subgroup.closure S = ⊤)
[h : MulAction.IsPretransitive G α] : Function.Surjective (MulAction.toPermHom G α) :=
by
rw [← MonoidHom.range_eq_top]
have := MulAction.IsPretransitive.of_compHom (α := α) (MulAction.toPermHom G α).rangeRestrict
rw [MonoidHom.range_eq_map, ← hS2, MonoidHom.map_closure] at this ⊢
exact closure_of_isSwap_of_isPretransitive (Set.forall_mem_image.2 hS1)
