English
If a nontrivial group M acts faithfully on α with a quasiprimitive action and a perfect commutator, then M is simple.
Русский
Если не тривиальная группа M действует на α удовлетворяя условию квазипривативности и коммутатор M является whole group, то M простая.
LaTeX
$$$[M,M] = M \quad\Rightarrow\quad M \text{ is simple (under quasiprimitive, faithful action, and Iwasawa structure)}$$$
Lean4
/-- The Iwasawa criterion for simplicity -/
theorem isSimpleGroup [Nontrivial M] (is_perfect : commutator M = ⊤) [IsQuasiPreprimitive M α]
(IwaS : IwasawaStructure M α) (is_faithful : FaithfulSMul M α) : IsSimpleGroup M :=
by
apply IsSimpleGroup.mk
intro N nN
cases or_iff_not_imp_left.mpr (IwaS.commutator_le N) with
| inl h =>
refine Or.inl (N.eq_bot_iff_forall.mpr fun n hn => ?_)
apply is_faithful.eq_of_smul_eq_smul
intro x
rw [one_smul]
exact Set.eq_univ_iff_forall.mp h x ⟨n, hn⟩
| inr h => exact Or.inr (top_le_iff.mp (le_trans (ge_of_eq is_perfect) h))
