Point stabilizers in faithful primitive actions, and enlarging the acting group

This file records two small facts about primitive actions.

The first is the fixed-point property that distinguishes a nonregular primitive action from a regular one. In a faithful primitive action, a nontrivial point stabilizer fixes only its base point. Equivalently, it moves every other point. This is the local ingredient in the primitivity of the product action of a permutation wreath product: a stabilizer element can change one coordinate of a tuple while leaving a constant tuple fixed.

The second is monotonicity in the acting subgroup. A block for a subgroup is a block for every smaller subgroup, so primitivity passes from a subgroup to every larger one. This is how primitivity of a transitive permutation group is inherited by the groups containing it. (The corresponding statement for transitivity is Mathlib's MulAction.IsPretransitive.of_compHom.)

Main results

• MulAction.IsBlock.of_le, MulAction.IsPreprimitive.of_le: blocks pass to smaller subgroups and primitivity to larger ones.
• TauCeti.MulAction.fixedPoints_stabilizer_eq_singleton: a nontrivial point stabilizer in a faithful primitive action fixes exactly its base point.
• TauCeti.MulAction.exists_mem_stabilizer_smul_ne: such a stabilizer moves every other point.

theorem MulAction.IsBlock.of_le {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] {H K : Subgroup G} (h : H ≤ K) {B : Set X} (hB : IsBlock (↥K) B) : IsBlock (↥H) B

A block for a subgroup is a block for every smaller subgroup.

theorem MulAction.IsPreprimitive.of_le {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] {H K : Subgroup G} (h : H ≤ K) [IsPreprimitive (↥H) X] : IsPreprimitive (↥K) X

A subgroup acting primitively makes every larger subgroup act primitively.

@[simp]

theorem TauCeti.MulAction.fixedPoints_stabilizer_eq_singleton {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [FaithfulSMul G X] [MulAction.IsPreprimitive G X] [Nontrivial X] (a : X) (ha : MulAction.stabilizer G a ≠ ⊥) : MulAction.fixedPoints (↥(MulAction.stabilizer G a)) X = {a}

In a faithful primitive action, the fixed-point set of a nontrivial point stabilizer is the singleton consisting of that point.

theorem TauCeti.MulAction.exists_mem_stabilizer_smul_ne {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [FaithfulSMul G X] [MulAction.IsPreprimitive G X] [Nontrivial X] (a : X) (ha : MulAction.stabilizer G a ≠ ⊥) {b : X} (hab : b ≠ a) : ∃ g ∈ MulAction.stabilizer G a, g • b ≠ b

A nontrivial point stabilizer in a faithful primitive action moves every other point.