English
A pretransitive action is preprimitive if and only if the stabilizer of any point is a maximal subgroup (Wielandt, theorem 7.5).
Русский
Предперводимое действие—пока не преформализовано—бывает примитивным тогда и только тогда, когда стабилизатор любого элемента является максимальной подгруппой (теорема Велянтa).
LaTeX
$$IsCoatom (stabilizer G a) ↔ IsPreprimitive G X$$
Lean4
/-- If the action is pretransitive, then the trivial blocks condition implies preprimitivity
(based condition) -/
@[to_additive /-- If the action is pretransitive, then the trivial blocks condition implies preprimitivity
(based condition) -/
]
theorem of_isTrivialBlock_base [IsPretransitive G X] (a : X)
(H : ∀ {B : Set X} (_ : a ∈ B) (_ : IsBlock G B), IsTrivialBlock B) : IsPreprimitive G X where
isTrivialBlock_of_isBlock {B}
hB := by
obtain rfl | ⟨b, hb⟩ := B.eq_empty_or_nonempty
· simp [IsTrivialBlock]
· obtain ⟨g, hg⟩ := exists_smul_eq G b a
rw [← IsTrivialBlock.smul_iff g]
apply H _ (hB.translate g)
rw [← hg]
use b
