English
A pretransitive action of the fixator yields pretransitive or primitive properties for the full action.
Русский
Предтранситивное действие фиксатора порождает предтранситивные или примитивные свойства полного действия.
LaTeX
$$IsMultiplyPretransitive (fixingSubgroup G s) (SubMulAction.ofFixingSubgroup G s) n$$
Lean4
/-- The fixator of a subset of cardinal `d` in an `n`-primitive action
acts `n-d`-primitively on the remaining (`d ≤ n`) -/
@[to_additive]
theorem isMultiplyPreprimitive {m n : ℕ} [IsMultiplyPreprimitive M α n] {s : Set α} [Finite s] (hs : s.ncard + m = n) :
IsMultiplyPreprimitive (fixingSubgroup M s) (SubMulAction.ofFixingSubgroup M s) m
where
isMultiplyPretransitive := by apply ofFixingSubgroup.isMultiplyPretransitive _ s hs
isPreprimitive_ofFixingSubgroup {t}
ht := by
let t' : Set α := Subtype.val '' t
have htt' : t = Subtype.val ⁻¹' t' := (Set.preimage_image_eq _ Subtype.coe_injective).symm
rw [htt']
suffices IsPreprimitive (fixingSubgroup M (s ∪ t')) (ofFixingSubgroup M (s ∪ t')) by
apply IsPreprimitive.of_surjective map_ofFixingSubgroupUnion_bijective.surjective
apply IsMultiplyPreprimitive.isPreprimitive_ofFixingSubgroup _ n
rw [Set.encard_union_eq _]
· rw [Subtype.coe_injective.encard_image, add_assoc, ht, ← hs, Nat.cast_add, Set.Finite.cast_ncard_eq]
exact Set.toFinite s
· apply disjoint_val_image
