Commit 2025-05-20 07:44 cdcc52b1

feat(GroupTheory.GroupAction.SubMulAction.OfStabilizer) : action of stabilizer on complement of a point (#23962) The SubMulAction of the stabilizer of a point on the complement of that point When a group G acts on a type α, the stabilizer of a point a : α acts naturally on the complement of that point. Such actions (and similar ones for other sets than singletons) are useful to study the multiple transitivity of the group G, since n-transitivity of G on α is equivalent to n - 1-transitivity of stabilizer G a on the complement of a. We define equivariant maps that relate various of these sub_mul_actions and permit to manipulate them in a relatively smooth way.

• SubMulAction.ofStabilizer a : the action of stabilizer G a on {a}ᶜ
• SubMulAction.Enat_card_ofStabilizer_eq_add_one, SubMulAction.nat_card_ofStabilizer_eq compute the cardinality of the carrier of that action. Consider a b : α and g : G such that hg : g • b = a.
• SubMulAction.conjMap hg is the equivariant map from SubMulAction.ofStabilizer G a to SubMulAction.ofStabilizer G b.
• SubMulAction.ofStabilizer.isPretransitive_iff_conj hg shows that this actions are equivalently pretransitive or
• SubMulAction.ofStabilizer.isMultiplyPretransitive_iff_conj hg shows that this actions are equivalently n-pretransitive for all n : ℕ.
• SubMulAction.ofStabilizer.append : given x : Fin n ↪ ofStabilizer G a, append a to obtain y : Fin n.succ ↪ α
• SubMulAction.ofStabilizer.isMultiplyPretransitive_iff : is the action of G on α is pretransitive, then it is n.succ pretransitive if and only if the action of stabilizer G a on ofStabilizer G a is n-pretransitive.