Iwasawa's criterion for central quotients

Mathlib's MulAction.IwasawaStructure attaches to every point x of a G-set a commutative subgroup T x of G, such that T (g • x) = g (T x) g⁻¹ and the subgroups T x generate G. Iwasawa's criterion MulAction.IwasawaStructure.isSimpleGroup says that a perfect group with such a structure is simple when its action is quasiprimitive and faithful.

The classical groups do not act faithfully on the points they are naturally attached to: the special linear, symplectic and unitary groups act on projective points, isotropic or not, and the kernel of the action consists of the scalar matrices in the group, which are central. The simple group is the quotient by that kernel. This file states Iwasawa's criterion in that form.

• A normal subgroup of a perfect group with an Iwasawa structure on a quasiprimitive action either acts trivially or is the whole group (MulAction.IwasawaStructure.fixedPoints_eq_univ_or_eq_top).
• Hence the quotient by any proper normal subgroup containing the kernel of the action is simple (MulAction.IwasawaStructure.isSimpleGroup_quotient), in particular the quotient by the centre when the kernel is central (MulAction.IwasawaStructure.isSimpleGroup_quotient_center).
• In that case the kernel is exactly the centre (MulAction.IwasawaStructure.mem_center_iff), so the centre of a concrete group can be read off from its action.
• The derived subgroup modulo its centre, TauCeti.DerivedCentralQuotient, is then simple (MulAction.IwasawaStructure.isSimpleGroup_derivedCentralQuotient). This is the form in which simplicity is needed for the fixed-point groups of Steinberg endomorphisms. When the group H of interest is not perfect but its derived subgroup is, the quotient criterion applies to an Iwasawa structure on commutator H itself: TauCeti.DerivedCentralQuotient H is by definition the quotient of commutator H by its centre.

The criterion needs one subgroup for every point. On a transitive action these are the conjugates of a single commutative subgroup T at a base point a that is normalized by the stabilizer of a; MulAction.IwasawaStructure.ofConj builds the structure from that data, provided the conjugates of T generate the group. This is the usual situation: T is a group of root elements (transvections, or the centre of the unipotent radical of a Borel subgroup) fixing the base point.

Main definitions

• MulAction.IwasawaStructure.ofConj: the Iwasawa structure given by the conjugates of one commutative subgroup normalized by a point stabilizer.

Main results

• MulAction.IwasawaStructure.fixedPoints_eq_univ_or_eq_top: the normal-subgroup dichotomy for a perfect group.
• MulAction.IwasawaStructure.isSimpleGroup_quotient: the quotient by a proper normal subgroup containing the kernel of the action is simple.
• MulAction.IwasawaStructure.isSimpleGroup_quotient_center: the quotient by the centre is simple when the kernel of the action is central.
• MulAction.IwasawaStructure.mem_center_iff: the centre is then the kernel of the action.
• MulAction.IwasawaStructure.isSimpleGroup_derivedCentralQuotient: the derived subgroup modulo its centre is simple.

References

• K. Iwasawa, Über die Einfachheit der speziellen projektiven Gruppen, Proc. Imp. Acad. Tokyo 17 (1941), 57--59.
• The faithful criterion and the normal-subgroup step MulAction.IwasawaStructure.commutator_le that every result here rests on are in Mathlib's Mathlib.GroupTheory.GroupAction.Iwasawa.

Iwasawa structures from a base point

noncomputable def MulAction.IwasawaStructure.ofConj {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] [IsPretransitive G α] (a : α) (T : Subgroup G) [IsMulCommutative ↥T] (hT : stabilizer G a ≤ Subgroup.normalizer ↑T) (hgen : Subgroup.normalClosure ↑T = ⊤) : IwasawaStructure G α

The Iwasawa structure of the conjugates of one subgroup. Let G act transitively on α, and let T be a commutative subgroup normalized by the stabilizer of a point a, whose conjugates generate G. The subgroup at the point g • a is the conjugate g T g⁻¹, which depends only on the point because the stabilizer of a normalizes T.

@[simp]

theorem MulAction.IwasawaStructure.ofConj_T_smul {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] [IsPretransitive G α] (a : α) (T : Subgroup G) [IsMulCommutative ↥T] (hT : stabilizer G a ≤ Subgroup.normalizer ↑T) (hgen : Subgroup.normalClosure ↑T = ⊤) (g : G) : (ofConj a T hT hgen).T (g • a) = MulAut.conj g • T

The subgroup of MulAction.IwasawaStructure.ofConj at the point g • a is g T g⁻¹.

@[simp]

theorem MulAction.IwasawaStructure.ofConj_T_self {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] [IsPretransitive G α] (a : α) (T : Subgroup G) [IsMulCommutative ↥T] (hT : stabilizer G a ≤ Subgroup.normalizer ↑T) (hgen : Subgroup.normalClosure ↑T = ⊤) : (ofConj a T hT hgen).T a = T

The subgroup of MulAction.IwasawaStructure.ofConj at the base point is T.

Simplicity of quotients

theorem MulAction.IwasawaStructure.fixedPoints_eq_univ_or_eq_top {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] [IsQuasiPreprimitive G α] (IwaS : IwasawaStructure G α) [Group.IsPerfect G] (N : Subgroup G) [N.Normal] : fixedPoints (↥N) α = Set.univ ∨ N = ⊤

Iwasawa's normal-subgroup theorem for a perfect group. If a perfect group has an Iwasawa structure on a quasiprimitive action, each of its normal subgroups either fixes every point or is the whole group.

theorem MulAction.IwasawaStructure.isSimpleGroup_quotient {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] [IsQuasiPreprimitive G α] (IwaS : IwasawaStructure G α) [Group.IsPerfect G] {N : Subgroup G} [N.Normal] (hN : N ≠ ⊤) (hker : ∀ (g : G), (∀ (x : α), g • x = x) → g ∈ N) : IsSimpleGroup (G ⧸ N)

Iwasawa's criterion for a quotient. Let a perfect group G have an Iwasawa structure on a quasiprimitive action. If a proper normal subgroup N contains every element acting trivially, then G ⧸ N is simple.

theorem MulAction.IwasawaStructure.isSimpleGroup_quotient_center {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] [IsQuasiPreprimitive G α] (IwaS : IwasawaStructure G α) [Group.IsPerfect G] [Nontrivial G] (hker : ∀ (g : G), (∀ (x : α), g • x = x) → g ∈ Subgroup.center G) : IsSimpleGroup (G ⧸ Subgroup.center G)

Iwasawa's criterion for the central quotient. Let a nontrivial perfect group G have an Iwasawa structure on a quasiprimitive action. If every element acting trivially is central, then G modulo its centre is simple.

theorem MulAction.IwasawaStructure.mem_center_iff {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] [IsQuasiPreprimitive G α] (IwaS : IwasawaStructure G α) [Group.IsPerfect G] (hker : ∀ (g : G), (∀ (x : α), g • x = x) → g ∈ Subgroup.center G) {g : G} : g ∈ Subgroup.center G ↔ ∀ (x : α), g • x = x

The centre is the kernel of the action. Let a perfect group G have an Iwasawa structure on a quasiprimitive action. If every element acting trivially is central, then the central elements are exactly the elements acting trivially.

theorem MulAction.IwasawaStructure.isSimpleGroup_derivedCentralQuotient {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] [IsQuasiPreprimitive G α] (IwaS : IwasawaStructure G α) [Group.IsPerfect G] [Nontrivial G] (hker : ∀ (g : G), (∀ (x : α), g • x = x) → g ∈ Subgroup.center G) : IsSimpleGroup (TauCeti.DerivedCentralQuotient G)

Iwasawa's criterion for the derived central quotient. Let a nontrivial perfect group G have an Iwasawa structure on a quasiprimitive action whose kernel is central. Then the derived subgroup of G modulo its centre, TauCeti.DerivedCentralQuotient G, is simple.