English
If a G-action on X is preprimitive, then every normal subgroup N of G that acts nontrivially on X has a pretransitive action on X.
Русский
Если действие G на X является предпримитивным, то любая нормальная подгруппа N G, действующая не тривиально на X, образует претривиальное действие на X.
LaTeX
$$$\\forall N \\trianglelefteq G,\\; (\\exists x \\in X,\\exists n \\in N:\\; n \\cdot x \\neq x) \\Rightarrow \\operatorname{IsPretransitive}(N,X)$$
Lean4
/-- In a preprimitive action, any normal subgroup that acts nontrivially is pretransitive
(Wielandt, th. 7.1). -/
@[to_additive /-- In a preprimitive additive action,
any normal subgroup that acts nontrivially is pretransitive (Wielandt, th. 7.1). -/
]
-- See note [lower instance priority]
instance (priority := 100) isQuasiPreprimitive [IsPreprimitive M α] : IsQuasiPreprimitive M α where
isPretransitive_of_normal {N} _
hNX := by
rw [Set.ne_univ_iff_exists_notMem] at hNX
obtain ⟨a, ha⟩ := hNX
rw [isPretransitive_iff_orbit_eq_univ a]
apply Or.resolve_left (isTrivialBlock_of_isBlock (IsBlock.orbit_of_normal a))
intro h
apply ha
simp only [mem_fixedPoints]
intro n
rw [← Set.mem_singleton_iff]
suffices orbit N a = { a } by rw [← this]; use n
ext b
rw [Set.Subsingleton.eq_singleton_of_mem h (MulAction.mem_orbit_self a)]
