Multiply preprimitive actions #
Let G be a group acting on a type α.
MulAction.IsMultiplyPreprimitive: The action is said to ben-primitive if, for every subsets : Set αwithnelements, the actions fstabilizer G son the complement ofsis primitive.MulAction.is_zero_preprimitive: any action is 0-primitiveMulAction.is_one_preprimitive_iff: an action is 1-primitive if and only if it is primitiveMulAction.isMultiplyPreprimitive_ofStabilizer: if an action isn + 1-primitive, then the action ofstabilizer G aon the complement of{a}isn-primitive.MulAction.isMultiplyPreprimitive_succ_iff_ofStabilizer: for1 ≤ n, an action isn + 1-primitive, then the action ofstabilizer G aon the complement of{a}isn-primitive. ofFixingSubgroup.isMultiplyPreprimitiveMulAction.ofFixingSubgroup.isMultiplyPreprimitive: If an action iss.ncard + m-primitive, then the action ofFixingSubgroup G son the complement ofsism-primitive.
An additive action is n-multiply preprimitive if is is n-multiply transitive
and if, when n ≥ 1, for every set s of cardinality n - 1,
the action of fixingAddSubgroup M s on the complement of s is preprimitive.
- isMultiplyPretransitive : IsMultiplyPretransitive M α n
An
n-preprimitive action isn-pretransitive - isPreprimitive_ofFixingAddSubgroup {s : Set α} (hs : s.encard + 1 = ↑n) : IsPreprimitive ↥(fixingAddSubgroup M s) ↥(SubAddAction.ofFixingAddSubgroup M s)
In an
n-preprimitive action, the action offixingAddSubgroup M sonofFixingAddSubgroup M sis preprimitive, for all setsssuch thats.encard + 1 = n
Instances
A group action is n-multiply preprimitive if is is n-multiply
transitive and if, when n ≥ 1, for every set s of cardinality
n - 1, the action of fixingSubgroup M s on the complement of s
is preprimitive.
- isMultiplyPretransitive : IsMultiplyPretransitive M α n
An
n-preprimitive action isn-pretransitive - isPreprimitive_ofFixingSubgroup {s : Set α} (hs : s.encard + 1 = ↑n) : IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)
In an
n-preprimitive action, the action offixingSubgroup M sonofFixingSubgroup M sis preprimitive, for all setsssuch thats.encard + 1 = n
Instances
Any action is 0-preprimitive
An action is preprimitive iff it is 1-preprimitive
The action of stabilizer M a is one-less preprimitive
A pretransitive action is n.succ-preprimitive iff
the action of stabilizers is n-preprimitive.
The fixator of a subset of cardinal d in an n-primitive action
acts n-d-primitively on the remaining (d ≤ n)
n.succ-pretransitivity implies n-preprimitivity.
n.succ-pretransitivity implies n-preprimitivity.
An n-preprimitive action is m-preprimitive for m ≤ n.
An n-preprimitive action is m-preprimitive for m ≤ n.