Tits's simplicity criterion for the normal closure of a split unipotent subgroup

Let G carry a Tits system (B, N) with irreducible Weyl group, and let U be a solvable subgroup normalized by B with B ≤ U (B ∩ N). Neither U ≤ B nor equality is assumed; the split case B = U (B ∩ N), as for the unipotent radical of the Borel subgroup of a split BN-pair, is the main example. Put

Z  = ⋂_{g : G} g B g⁻¹,        H⁺ = normal closure of U in G.

The group G itself need not be perfect or generated by the conjugates of U: for the finite groups of Lie type, G is the group of fixed points of a Steinberg endomorphism and H⁺ is the subgroup generated by its root subgroups, typically the derived subgroup. This file proves Tits's simplicity criterion for H⁺, under the assumption that H⁺ is perfect:

• every normal subgroup of H⁺ lies in Z ∩ H⁺ or is all of H⁺;
• if moreover Z ∩ U = 1, then Z ∩ H⁺ is the centre of H⁺;
• hence H⁺ / (Z ∩ H⁺) is simple whenever it is nontrivial, and when H⁺ = [G, G] the derived central quotient [G, G] / Z([G, G]) is simple whenever it is nontrivial;
• if Z ∩ U = 1, then H⁺ / (Z ∩ H⁺) is nontrivial as soon as U ≠ 1. When H⁺ = [G, G], the derived central quotient is nontrivial as soon as U ≠ 1, for any perfect [G, G] (TauCeti.Group.IsPerfect.nontrivial_quotient_center).

Either H⁺ ≤ Z, and everything is degenerate, or H⁺ B = G by Tits's theorem on normal subgroups. In the second case G = H⁺ (B ∩ N), so (B, N) pulls back to a Tits system on H⁺ (TauCeti.TitsSystem.comap) with the same Weyl group and simple reflections, in which the conjugates of U generate. Tits's simplicity theorem for that Tits system gives the first statement, because the normal core of B ∩ H⁺ in H⁺ is Z ∩ H⁺. If Z ∩ U = 1, then Z commutes with U, hence with each conjugate of U, so Z ∩ H⁺ is central; conversely the centre of the perfect group H⁺ cannot be all of H⁺ unless H⁺ is trivial.

Main results

• TauCeti.TitsSystem.le_normalCore_subgroupOf_or_eq_top_of_normal: the normal-subgroup theorem for H⁺.
• TauCeti.TitsSystem.center_normalClosure_eq_normalCore_subgroupOf: the centre of H⁺ is Z ∩ H⁺ when Z ∩ U = 1.
• TauCeti.TitsSystem.isSimpleGroup_quotient_normalCore_subgroupOf: H⁺ / (Z ∩ H⁺) is simple whenever it is nontrivial.
• TauCeti.TitsSystem.isSimpleGroup_derivedCentralQuotient: if H⁺ = [G, G], the derived central quotient of G is simple whenever it is nontrivial.
• TauCeti.TitsSystem.nontrivial_quotient_normalCore_subgroupOf: H⁺ / (Z ∩ H⁺) is nontrivial when Z ∩ U = 1 and U ≠ 1.

References

• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Chapter IV, §2, no. 7.
• B. Conrad, handout on Tits systems for Math 249B (Stanford, Winter 2016), Theorem 2.4.
• R. W. Carter, Simple Groups of Lie Type (1972), Chapter 11.

The normal closure of a split unipotent subgroup

theorem TauCeti.TitsSystem.nontrivial_quotient_normalCore_subgroupOf {G : Type u} [Group G] (T : TitsSystem G) {U : Subgroup G} (hZU : T.subgroupB.normalCore ⊓ U = ⊥) (hU : U ≠ ⊥) : Nontrivial (↥(Subgroup.normalClosure ↑U) ⧸ T.subgroupB.normalCore.subgroupOf (Subgroup.normalClosure ↑U))

If Z = ⋂ g B g⁻¹ meets U ≠ 1 trivially, then the quotient H⁺ / (Z ∩ H⁺) of the normal closure H⁺ of U is nontrivial, since otherwise U ≤ H⁺ ≤ Z.

theorem TauCeti.TitsSystem.le_normalCore_subgroupOf_or_eq_top_of_normal {G : Type u} [Group G] (T : TitsSystem G) {U : Subgroup G} (hirr : T.IsIrreducible) [Group.IsSolvable ↥U] (hBU : T.subgroupB ≤ Subgroup.normalizer ↑U) (hsplit : T.subgroupB ≤ U ⊔ T.subgroupB ⊓ T.subgroupN) [Group.IsPerfect ↥(Subgroup.normalClosure ↑U)] (K : Subgroup ↥(Subgroup.normalClosure ↑U)) [K.Normal] : K ≤ T.subgroupB.normalCore.subgroupOf (Subgroup.normalClosure ↑U) ∨ K = ⊤

Tits's theorem on normal subgroups of the normal closure of U. Suppose the Weyl group is irreducible, U is a solvable subgroup normalized by B with B ≤ U (B ∩ N), and the normal closure H⁺ of U is perfect. Then every normal subgroup of H⁺ either lies in Z ∩ H⁺, where Z = ⋂ g B g⁻¹ is the normal core of B, or is all of H⁺.

theorem TauCeti.TitsSystem.center_normalClosure_eq_normalCore_subgroupOf {G : Type u} [Group G] (T : TitsSystem G) {U : Subgroup G} (hirr : T.IsIrreducible) [Group.IsSolvable ↥U] (hBU : T.subgroupB ≤ Subgroup.normalizer ↑U) (hsplit : T.subgroupB ≤ U ⊔ T.subgroupB ⊓ T.subgroupN) [Group.IsPerfect ↥(Subgroup.normalClosure ↑U)] (hZU : T.subgroupB.normalCore ⊓ U = ⊥) : Subgroup.center ↥(Subgroup.normalClosure ↑U) = T.subgroupB.normalCore.subgroupOf (Subgroup.normalClosure ↑U)

The centre of the normal closure of U. Under the hypotheses of TauCeti.TitsSystem.le_normalCore_subgroupOf_or_eq_top_of_normal, if moreover Z ∩ U = 1, then the centre of the normal closure H⁺ of U is Z ∩ H⁺.

theorem TauCeti.TitsSystem.isSimpleGroup_quotient_normalCore_subgroupOf {G : Type u} [Group G] (T : TitsSystem G) {U : Subgroup G} (hirr : T.IsIrreducible) [Group.IsSolvable ↥U] (hBU : T.subgroupB ≤ Subgroup.normalizer ↑U) (hsplit : T.subgroupB ≤ U ⊔ T.subgroupB ⊓ T.subgroupN) [Group.IsPerfect ↥(Subgroup.normalClosure ↑U)] [Nontrivial (↥(Subgroup.normalClosure ↑U) ⧸ T.subgroupB.normalCore.subgroupOf (Subgroup.normalClosure ↑U))] : IsSimpleGroup (↥(Subgroup.normalClosure ↑U) ⧸ T.subgroupB.normalCore.subgroupOf (Subgroup.normalClosure ↑U))

Tits's simplicity criterion for the normal closure of U. Under the hypotheses of TauCeti.TitsSystem.le_normalCore_subgroupOf_or_eq_top_of_normal, the quotient H⁺ / (Z ∩ H⁺) of the normal closure H⁺ of U by its intersection with Z = ⋂ g B g⁻¹ is simple whenever it is nontrivial.

theorem TauCeti.TitsSystem.isSimpleGroup_derivedCentralQuotient {G : Type u} [Group G] (T : TitsSystem G) {U : Subgroup G} (hirr : T.IsIrreducible) [Group.IsSolvable ↥U] (hBU : T.subgroupB ≤ Subgroup.normalizer ↑U) (hsplit : T.subgroupB ≤ U ⊔ T.subgroupB ⊓ T.subgroupN) (hZU : T.subgroupB.normalCore ⊓ U = ⊥) (hU : Subgroup.normalClosure ↑U = commutator G) [Group.IsPerfect ↥(commutator G)] [Nontrivial (DerivedCentralQuotient G)] : IsSimpleGroup (DerivedCentralQuotient G)

Simplicity of the derived central quotient from a split Tits system. Suppose the Weyl group is irreducible, U is a solvable subgroup normalized by B with B ≤ U (B ∩ N) and Z ∩ U = 1 for Z = ⋂ g B g⁻¹, the normal closure of U is the derived subgroup [G, G], and [G, G] is perfect. Then the derived central quotient [G, G] / Z([G, G]) is simple whenever it is nontrivial.