The centralizer of a transitive group of permutations

A permutation commuting with every element of a transitive group of permutations, and fixing one letter, is the identity: transitivity carries the fixed letter to any other letter, and the commutation then makes the permutation fix that letter too. So the centralizer of a transitive group of permutations, acting on the letters by evaluation, has trivial stabilizers, and on a finite set of letters its order divides the number of letters.

This bounds the size of the centralizer of a transitive permutation group, which is the semiregularity step behind the order bound for the automorphism group of a permutation group action.

Main results

• Subgroup.eq_one_of_mem_centralizer_of_apply_eq: a commuting permutation fixing a letter is the identity.
• Subgroup.centralizer_stabilizer_eq_bot: the centralizer of a transitive group of permutations acts freely on the letters.
• Subgroup.natCard_centralizer_dvd: the Nat.card of that centralizer divides the Nat.card of the letters.
• Subgroup.card_centralizer_dvd: on a finite set of letters, the order of that centralizer divides the number of letters.

The counting step is orbit-stabilizer: a set on which a group acts with trivial stabilizers is in bijection with the product of its orbit space with the acting group, so the number of letters is the number of orbits times the order of the centralizer.

theorem Subgroup.eq_one_of_mem_centralizer_of_apply_eq {α : Type u_1} {G : Subgroup (Equiv.Perm α)} (hG : MulAction.IsPretransitive (↥G) α) {τ : Equiv.Perm α} (hτ : τ ∈ centralizer ↑G) {i : α} (hi : τ i = i) : τ = 1

A permutation commuting with a transitive group of permutations and fixing one letter is the identity: transitivity moves the fixed letter to any other letter, where commutation forces it to be fixed as well.

theorem Subgroup.centralizer_stabilizer_eq_bot {α : Type u_1} {G : Subgroup (Equiv.Perm α)} (hG : MulAction.IsPretransitive (↥G) α) (i : α) : MulAction.stabilizer (↥(centralizer ↑G)) i = ⊥

The centralizer of a transitive group of permutations, acting on the letters by evaluation, has trivial stabilizers.

theorem Subgroup.natCard_centralizer_dvd {α : Type u_1} (G : Subgroup (Equiv.Perm α)) (hG : MulAction.IsPretransitive (↥G) α) : Nat.card ↥(centralizer ↑G) ∣ Nat.card α

The cardinality of the centralizer of a transitive group of permutations divides the cardinality of the letters, the centralizer being free on them and so exhibiting the letters as the product of their orbit space with the centralizer. Since Nat.card is 0 on an infinite carrier, this bounds the order of the centralizer only on a finite set of letters, where TauCeti.Subgroup.card_centralizer_dvd is the bound.

theorem Subgroup.card_centralizer_dvd {α : Type u_1} [Fintype α] (G : Subgroup (Equiv.Perm α)) (hG : MulAction.IsPretransitive (↥G) α) : Nat.card ↥(centralizer ↑G) ∣ Fintype.card α

The order of the centralizer of a transitive group of permutations divides the number of letters: on a finite set of letters the centralizer is free on them, so its order divides their number.