English
Another version: given a nontrivial fixed point condition, the same mk' construction yields preprimitivity.
Русский
Еще одна версия: при условии ненулевого фиксированного множества и аналогичных блоков, конструкт mk' дает предпримитивность.
LaTeX
$$theorem mk' (Hnt : fixedPoints G X ≠ ⊤) (H : ∀ {B : Set X} (_ : IsBlock G B), IsTrivialBlock B) : IsPreprimitive G X$$
Lean4
/-- A pretransitive action is preprimitive
iff the stabilizer of any point is a maximal subgroup (Wielandt, th. 7.5) -/
@[to_additive /-- A pretransitive action is preprimitive
iff the stabilizer of any point is a maximal subgroup (Wielandt, th. 7.5) -/
]
theorem isCoatom_stabilizer_iff_preprimitive [IsPretransitive G X] [Nontrivial X] (a : X) :
IsCoatom (stabilizer G a) ↔ IsPreprimitive G X :=
by
rw [← isSimpleOrder_blockMem_iff_isPreprimitive G a, ← Set.isSimpleOrder_Ici_iff_isCoatom]
simp only [isSimpleOrder_iff_isCoatom_bot]
rw [← OrderIso.isCoatom_iff (block_stabilizerOrderIso G a), OrderIso.map_bot]
