Normal subgroups of a group with a Tits system, and Tits's simplicity theorem

Let G carry a Tits system (B, N) with simple reflections S in the Weyl group W. For a normal subgroup H of G, the subgroup H ⊔ B = H B contains B, so it is a standard parabolic P_J. Tits's theorem on normal subgroups says that J and its complement in S commute elementwise. Consequently, if the Coxeter system (W, S) is irreducible, either H lies in B, hence in the normal core Z = ⋂ g B g⁻¹ of B, or H B = G.

Combined with a solvable subgroup U normalized by B whose conjugates generate a perfect group G, this gives Tits's simplicity theorem: every normal subgroup of G lies in Z or is all of G, so G / Z is simple as soon as S is nonempty. This is the abstract simplicity criterion behind the simplicity of the finite groups of Lie type.

Irreducibility is TauCeti.TitsSystem.IsIrreducible, defined with the Coxeter system of a Tits system.

Main results

• TauCeti.TitsSystem.simple_mul_comm_of_bruhatCell_subset_sup: if H is normal, a simple reflection whose cell lies in H B commutes with one whose cell does not.
• TauCeti.TitsSystem.exists_standardParabolic_eq_sup_of_normal: Tits's theorem on normal subgroups.
• TauCeti.TitsSystem.le_normalCore_or_sup_eq_top_of_normal: the irreducible dichotomy H ≤ Z or H B = G.
• TauCeti.TitsSystem.le_normalCore_or_eq_top_of_normal: Tits's simplicity theorem for normal subgroups.
• TauCeti.TitsSystem.isSimpleGroup_quotient_normalCore: the quotient G / Z is simple.

References

• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Chapter IV, §2, no. 7.
• J. E. Humphreys, Linear Algebraic Groups (1975), Section 29.5.

theorem TauCeti.TitsSystem.simple_mul_comm_of_bruhatCell_subset_sup {G : Type u} [Group G] (T : TitsSystem G) {H : Subgroup G} [H.Normal] {s t : T.WeylGroup} (hs : s ∈ T.simple) (ht : t ∈ T.simple) (hsH : T.bruhatCell s ⊆ ↑(H ⊔ T.subgroupB)) (htH : ¬T.bruhatCell t ⊆ ↑(H ⊔ T.subgroupB)) : s * t = t * s

The key step of Tits's theorem on normal subgroups. If H is normal, a simple reflection whose Bruhat cell lies in H ⊔ B commutes with every simple reflection whose cell does not.

theorem TauCeti.TitsSystem.exists_standardParabolic_eq_sup_of_normal {G : Type u} [Group G] (T : TitsSystem G) (H : Subgroup G) [H.Normal] : ∃ (J : Set ↑T.simple), T.standardParabolic J = H ⊔ T.subgroupB ∧ ∀ s ∈ J, ∀ t ∉ J, ↑s * ↑t = ↑t * ↑s

Tits's theorem on normal subgroups. For a normal subgroup H, the subgroup H ⊔ B is a standard parabolic P_J for a set J of simple reflections that commutes elementwise with its complement.

theorem TauCeti.TitsSystem.le_normalCore_or_sup_eq_top_of_normal {G : Type u} [Group G] (T : TitsSystem G) (hirr : T.IsIrreducible) (H : Subgroup G) [H.Normal] : H ≤ T.subgroupB.normalCore ∨ H ⊔ T.subgroupB = ⊤

Normal subgroups for an irreducible Weyl group. If every set of simple reflections commuting elementwise with its complement is empty or everything, then a normal subgroup H either lies in the normal core ⋂ g B g⁻¹ of B or satisfies H ⊔ B = G.

theorem TauCeti.TitsSystem.le_normalCore_or_eq_top_of_normal {G : Type u} [Group G] (T : TitsSystem G) (hirr : T.IsIrreducible) [Group.IsPerfect G] {U : Subgroup G} [Group.IsSolvable ↥U] (hBU : T.subgroupB ≤ Subgroup.normalizer ↑U) (hU : Subgroup.normalClosure ↑U = ⊤) (H : Subgroup G) [H.Normal] : H ≤ T.subgroupB.normalCore ∨ H = ⊤

Tits's simplicity theorem, for normal subgroups. Suppose the Weyl group is irreducible, G is perfect, and U is a solvable subgroup normalized by B whose conjugates generate G. Then every normal subgroup of G either lies in the normal core ⋂ g B g⁻¹ of B or is G.

theorem TauCeti.TitsSystem.isSimpleGroup_quotient_normalCore {G : Type u} [Group G] (T : TitsSystem G) (hS : T.simple.Nonempty) (hirr : T.IsIrreducible) [Group.IsPerfect G] {U : Subgroup G} [Group.IsSolvable ↥U] (hBU : T.subgroupB ≤ Subgroup.normalizer ↑U) (hU : Subgroup.normalClosure ↑U = ⊤) : IsSimpleGroup (G ⧸ T.subgroupB.normalCore)

Tits's simplicity theorem. Suppose there is at least one simple reflection, the Weyl group is irreducible, G is perfect, and U is a solvable subgroup normalized by B whose conjugates generate G. Then the quotient of G by the normal core ⋂ g B g⁻¹ of B is simple.