Commit 2025-07-23 08:49 1e28d511

View on Github →

feat(GroupTheory/SpecificGroups/Alternating/KleinFour): the Klein Four subgroup of alternatingGroup on 4 letters (#27057) Let α be a finite type.

alternatingGroup.center_eq_bot: when 4 ≤ Nat.card α, then center of alternatingGroup α is trivial. We now assume that Nat.card α = 4.
alternatingGroup.kleinFour : the subgroup of alternatingGroup α generated by permutations of cycle type (2, 2).
alternatingGroup.kleinFour_isKleinFour:alternatingGroup.kleinFour α satisfies IsKleinFour. (When 4 < Nat.card α, it is equal to ⊤, when Nat.card α < 4, it is trivial.)
alternatingGroup.two_sylow_eq_kleinFour_of_four: All 2-sylow subgroups of alternatingGroup α are equal to kleinFour α.
alternatingGroup.characteristic_kleinFour: the subgroup alternatingGroup.kleinFour α is characteristic.
alternatingGroup.normal_kleinFour: the subgroup alternatingGroup.kleinFour α is normal.
alternatingGroup.kleinFour_eq_commutator: the subgroup alternatingGroup.kleinFour α is the commutator subgroup of alternatingGroup α. (When 4 < Nat.card α, the commutator subgroup of alternatingGroup α is equal to ⊤; when Nat.card α < 3, it is trivial.)

Remark on implementation

We start from kleinFour α as given by its definition. We first prove that it is equal to any 2-sylow subgroup: the elements of such a sylow subgroup S have order a power of 2, and this implies that their cycle type is () or (2,2). Since there are exactly 4 elements of that cycle type, we conclude that kleinFour α = S. Since all 2-sylow subgroups are conjugate, we conclude that there is only one 2-sylow subgroup and that it is normal, and then characteristic.