The two subgroups of the symmetric group on three points

Equiv.Perm (Fin 3) is the symmetric group S₃, and it has two kinds of proper nontrivial subgroup. The stabilizer of a point a is the two-element subgroup generated by the transposition of the two other points, which are a + 1 and a + 2 whichever a is; this file identifies that stabilizer -- by membership, as a set, as a cyclic subgroup and by its order -- and records that it is not normal, conjugating its transposition by one that moves a off the stabilizer. The alternating subgroup A₃ is the other one, and what is recorded of it here is that it has order three, that nothing outside it centralizes it, and that it is the commutator subgroup, so that S₃ is as far from abelian along A₃ as it could be and its abelianization has order two. The two sit together as a semidirect decomposition S₃ = A₃ ⋊ ⟨(a+1 a+2)⟩ whose complement acts on A₃ without nonidentity fixed points, which exhibits the stabilizer as a Frobenius complement and S₃ as the smallest Frobenius group.

All the facts about Fin 3 that the arguments need are settled by decide over the six permutations.

Main statements

• Equiv.Perm.fin_three_cases: every permutation of three points is the identity, one of the three transpositions, or one of the two rotations.
• TauCeti.mem_stabilizer_perm_fin_three_iff: a permutation of three points fixes a exactly when it is the identity or the transposition of the other two points.
• TauCeti.coe_stabilizer_perm_fin_three: the same, as an equality of sets.
• TauCeti.stabilizer_perm_fin_three_eq_zpowers: the stabilizer is the subgroup generated by that transposition.
• TauCeti.card_stabilizer_perm_fin_three: it has order two.
• TauCeti.not_normal_stabilizer_perm_fin_three: it is not normal.
• TauCeti.sign_eq_one_or_card_fixedPoints_eq_one_perm_fin_three: a permutation of three points is even or fixes exactly one point.
• TauCeti.sign_mul_card_fixedPoints_fin_three: the ring-valued form of that disjunction, the sign times the number of fixed points as their sum less one.
• TauCeti.card_alternatingGroup_fin_three: the alternating subgroup has order three.
• TauCeti.commutator_perm_fin_three_eq_alternatingGroup: the commutator subgroup of S₃ is A₃.
• TauCeti.card_abelianization_perm_fin_three and TauCeti.exponent_abelianization_perm_fin_three: the abelianization of S₃ has order two and exponent two.
• TauCeti.centralizer_alternatingGroup_fin_three_le: only the alternating subgroup centralizes the alternating subgroup.
• TauCeti.fixedPointFree_conjNormal_alternatingGroup_fin_three: a point stabilizer acts on the alternating subgroup by conjugation without nonidentity fixed points, a transposition inverting each of the two rotations.
• TauCeti.isComplement'_alternatingGroup_stabilizer_perm_fin_three: the two subgroups are complementary, S₃ = A₃ ⋊ ⟨(a+1 a+2)⟩.
• TauCeti.isTISubgroup_stabilizer_perm_fin_three: a point stabilizer is a trivial-intersection subgroup.
• TauCeti.isFrobeniusComplement_stabilizer_perm_fin_three: S₃ is a Frobenius group with complement a point stabilizer.

theorem Equiv.Perm.fin_three_cases (ρ : Perm (Fin 3)) : ρ = 1 ∨ ρ = swap 0 1 ∨ ρ = swap 1 2 ∨ ρ = swap 0 2 ∨ ρ = finRotate 3 ∨ ρ = (finRotate 3)⁻¹

The six permutations of Fin 3: the identity, the three transpositions, and the two rotations.

theorem TauCeti.mem_stabilizer_perm_fin_three_iff (a : Fin 3) (σ : Equiv.Perm (Fin 3)) : σ ∈ MulAction.stabilizer (Equiv.Perm (Fin 3)) a ↔ σ = 1 ∨ σ = Equiv.swap (a + 1) (a + 2)

A permutation of three points fixing a is the identity or the transposition of the other two points. Written with a + 1 and a + 2 so that the statement is uniform in a: those are the two points other than a, whichever a is.

theorem TauCeti.coe_stabilizer_perm_fin_three (a : Fin 3) : ↑(MulAction.stabilizer (Equiv.Perm (Fin 3)) a) = {1, Equiv.swap (a + 1) (a + 2)}

The point stabilizer of S₃, as a set: the identity and one transposition.

theorem TauCeti.stabilizer_perm_fin_three_eq_zpowers (a : Fin 3) : MulAction.stabilizer (Equiv.Perm (Fin 3)) a = Subgroup.zpowers (Equiv.swap (a + 1) (a + 2))

The point stabilizer of S₃ is generated by a transposition: it is the roadmap's ⟨(1 2)⟩, written at the point it stabilizes.

theorem TauCeti.card_stabilizer_perm_fin_three (a : Fin 3) : Nat.card ↥(MulAction.stabilizer (Equiv.Perm (Fin 3)) a) = 2

The point stabilizer of S₃ has order two: it is the two-element subgroup generated by a transposition, the roadmap's ⟨(1 2)⟩.

theorem TauCeti.not_normal_stabilizer_perm_fin_three (a : Fin 3) : ¬(MulAction.stabilizer (Equiv.Perm (Fin 3)) a).Normal

The point stabilizer of S₃ is not normal: conjugating its transposition by a transposition moving a produces a permutation that no longer fixes a.

theorem TauCeti.sign_eq_one_or_card_fixedPoints_eq_one_perm_fin_three (σ : Equiv.Perm (Fin 3)) : Equiv.Perm.sign σ = 1 ∨ Nat.card { x : Fin 3 // σ • x = x } = 1

An odd permutation of three points fixes exactly one point, stated as a disjunction: a permutation of three points is either even or has exactly one fixed point. The two cases are exhaustive and disjoint -- the even permutations are the identity, fixing all three points, and the two three-cycles, fixing none, while the three transpositions are odd and fix exactly one -- so the disjunction is what a case split on the parity consumes.

theorem TauCeti.sign_mul_card_fixedPoints_fin_three {k : Type u_1} [NonAssocRing k] (σ : Equiv.Perm (Fin 3)) : ↑↑(Equiv.Perm.sign σ) * ↑(Nat.card { x : Fin 3 // σ • x = x }) = ↑↑(Equiv.Perm.sign σ) + ↑(Nat.card { x : Fin 3 // σ • x = x }) - 1

The sign of a permutation of three points against its number of fixed points: writing F for the number of points that σ fixes, sgn σ · F = sgn σ + F - 1 in any ring. This is the ring-valued form of TauCeti.sign_eq_one_or_card_fixedPoints_eq_one_perm_fin_three, and it is what turns the product of the sign character of S₃ with a permutation character into a sum.

theorem TauCeti.card_alternatingGroup_fin_three : Nat.card ↥(alternatingGroup (Fin 3)) = 3

The alternating subgroup of S₃ has order three: half of 3! = 6.

@[simp]

theorem TauCeti.commutator_perm_fin_three_eq_alternatingGroup : commutator (Equiv.Perm (Fin 3)) = alternatingGroup (Fin 3)

The commutator subgroup of S₃ is A₃. The commutator subgroup of any permutation group lies in the alternating subgroup, and on three points the alternating subgroup consists of the identity and the two rotations, each of which is a commutator.

@[simp]

theorem TauCeti.card_abelianization_perm_fin_three : Nat.card (Abelianization (Equiv.Perm (Fin 3))) = 2

The abelianization of S₃ has order two. The commutator subgroup is A₃, of order 3 inside a group of order 6.

@[simp]

theorem TauCeti.exponent_abelianization_perm_fin_three : Monoid.exponent (Abelianization (Equiv.Perm (Fin 3))) = 2

The abelianization of S₃ has exponent two: it is a group of prime order two.

theorem TauCeti.centralizer_alternatingGroup_fin_three_le : Subgroup.centralizer ↑(alternatingGroup (Fin 3)) ≤ alternatingGroup (Fin 3)

Nothing outside A₃ centralizes A₃. A permutation commuting with every even permutation of three points is itself even; equivalently, the centralizer of the alternating subgroup is the alternating subgroup, since an abelian subgroup centralizes itself. This is the failure of commutation that makes a faithful linear character of A₃ induce irreducibly to S₃.

theorem TauCeti.fixedPointFree_conjNormal_alternatingGroup_fin_three (a : Fin 3) (h : ↥(MulAction.stabilizer (Equiv.Perm (Fin 3)) a)) : h ≠ 1 → MonoidHom.FixedPointFree ⇑(MulAut.conjNormal ↑h)

A point stabilizer of S₃ acts on A₃ without nonidentity fixed points: conjugation by a nonidentity element of the stabilizer of a fixes no nonidentity element of the alternating subgroup. This is the fixed-point hypothesis of TauCeti.isTISubgroup_of_isComplement'_of_fixedPointFree.

theorem TauCeti.isComplement'_alternatingGroup_stabilizer_perm_fin_three (a : Fin 3) : (alternatingGroup (Fin 3)).IsComplement' (MulAction.stabilizer (Equiv.Perm (Fin 3)) a)

A₃ is a normal complement to a point stabilizer in S₃: the two have orders 3 and 2, which are coprime and multiply to 3! = 6.

theorem TauCeti.isTISubgroup_stabilizer_perm_fin_three (a : Fin 3) : IsTISubgroup (MulAction.stabilizer (Equiv.Perm (Fin 3)) a)

A point stabilizer of S₃ is a trivial-intersection subgroup, by the fixed-point-free action of TauCeti.isTISubgroup_of_isComplement'_of_fixedPointFree on the alternating complement.

theorem TauCeti.isFrobeniusComplement_stabilizer_perm_fin_three (a : Fin 3) : IsFrobeniusComplement (MulAction.stabilizer (Equiv.Perm (Fin 3)) a)

S₃ is a Frobenius group with complement a point stabilizer. Properness and nontriviality come from the stabilizer not being normal, which ⊥ and ⊤ both are.