Iwasawa criterion for simplicity

• IwasawaStructure : the structure underlying the Iwasawa criterion For a group G, this consists of an action of G on a type α and, for every a : α, of a subgroup T a, such that the following properties hold:
  • for all a, T a is commutative
  • for all g : G and a : α, `T (g • a) = MulAut.conj g • T a
  • the subgroups T a generate G

We then prove two versions of the Iwasawa criterion when there is an Iwasawa structure.

• IwasawaStructure.commutator_le asserts that if the action of G on α is quasiprimitive, then every normal subgroup that acts nontrivially contains commutator G

• IwasawaStructure.isSimpleGroup : the Iwasawa criterion for simplicity If the action of G on α is quasiprimitive and faithful, and G is nontrivial and perfect, then G is simple.

TODO

Additivize. The issue is that it requires to additivize commutator (which, moreover, lives in the root namespace)

structure MulAction.IwasawaStructure (M : Type u_1) [Group M] (α : Type u_2) [MulAction M α] : Type (max u_1 u_2)

The structure underlying the Iwasawa criterion

• T : α → Subgroup M

  The subgroups of the Iwasawa structure

• is_comm (x : α) : (self.T x).IsCommutative

  The commutativity property of the subgroups

• is_conj (g : M) (x : α) : self.T (g • x) = MulAut.conj g • self.T x

  The conjugacy property of the subgroups

• is_generator : iSup self.T = ⊤

  The subgroups generate the group

theorem MulAction.IwasawaStructure.commutator_le {M : Type u_1} [Group M] {α : Type u_2} [MulAction M α] (IwaS : IwasawaStructure M α) [IsQuasiPreprimitive M α] (N : Subgroup M) [nN : N.Normal] (hNX : fixedPoints (↥N) α ≠ Set.univ) : commutator M ≤ N

The Iwasawa criterion : If a quasiprimitive action of a group G on X has an Iwasawa structure, then any normal subgroup that acts nontrivially contains the group of commutators.

theorem MulAction.IwasawaStructure.isSimpleGroup {M : Type u_1} [Group M] {α : Type u_2} [MulAction M α] [Nontrivial M] (is_perfect : commutator M = ⊤) [IsQuasiPreprimitive M α] (IwaS : IwasawaStructure M α) (is_faithful : FaithfulSMul M α) : IsSimpleGroup M

The Iwasawa criterion for simplicity