English
The alternating group is the only subgroup of index 2 of the permutation group.
Русский
Чередующаяся группа — единственная подгруппа индекса 2 в группе перестановок.
LaTeX
$$$$\\text{If } G \\le \\operatorname{Perm}(\\alpha) \\text{ and } [\\operatorname{Perm}(\\alpha) : G] = 2, \\text{ then } G = \\operatorname{alternatingGroup}(\\alpha).$$$$
Lean4
/-- The alternating group is the only subgroup of index 2 of the permutation group. -/
theorem eq_alternatingGroup_of_index_eq_two {G : Subgroup (Equiv.Perm α)} (hG : G.index = 2) : G = alternatingGroup α :=
by
nontriviality α
obtain ⟨_, ⟨a, b, hab, rfl⟩, habG⟩ : ∃ g : Perm α, g.IsSwap ∧ g ∉ G :=
by
by_contra! h
suffices G = ⊤ by rw [this, Subgroup.index_top] at hG; cases hG
rwa [eq_top_iff, ← closure_isSwap, G.closure_le]
ext g
refine swap_induction_on g (iff_of_true G.one_mem <| map_one _) fun g x y hxy ih ↦ ?_
rw [mul_mem_iff_of_index_two hG, mul_mem_iff_of_index_two alternatingGroup.index_eq_two, ih]
refine iff_congr (iff_of_false ?_ (by cases (sign_swap hxy).symm.trans ·)) Iff.rfl
contrapose! habG
rw [← (isConj_iff.mp <| isConj_swap hxy hab).choose_spec]
exact (normal_of_index_eq_two hG).conj_mem _ habG _
