Generation of the general linear group

Stream: PR reviews

[Antoine Chambert-Loir]

In a series of PRs, I formalized Dieudonné's theorem on the generation of the general linear group over a division ring K.

There is a bit of vocabulary to state all of this.

The fixedSubmodule of a linear equivalence e : V ≃ₗ[K] V is the submodule of all x such that e x = x. Passing to the quotients, any such e defines a linear equivalence e.fixedReduce (V ⧸ e.fixedSubmodule) ≃ₗ[K] (V ⧸ e.fixedSubmodule).

Among linear equivalences, one can distinguish dilatransvections which are those which differ from identity by a linear map of rank at most one. Equivalently, the rank of V ⧸ e.fixedSubmodule is at most 1. transvections are characterized among them by the fact that e.fixedReduce = 1. This fact is proved in #33348.

[Antoine Chambert-Loir]

Then Dieudonné's theorem can be stated as follows:
Unless e.fixedReduce is a non-trivial homothety of V ⧸ e.fixedSubmodule, the linear equivalence e can be written as the product of finrank K (V ⧸ e.fixedSubmodule) - 1 transvections and
one dilatransvection.

This is proved in #33392.

[Antoine Chambert-Loir]

In the exceptional case, there are two results.

First of all, any e can be written as the product of finrank K (V ⧸ e.fixedSubmodule) transvection and one dilatransvection. This is #33402.

[Antoine Chambert-Loir]

Conversely, if e can be written as the product of finrank K (V ⧸ e.fixedSubmodule) - 1 transvections and
one dilatransvection, then it is not exceptional. This is proved in #33485.

[Antoine Chambert-Loir]

The study of non-exceptional equivalences uses a classic criterion (proved in #33282) that a linear endomorphism f is a homothety (with central ratio) if and only if f x and x are collinear, for all x. (In the noncommutative case, one needs to assume that the rank of the ambient space is at least 2.)

[Antoine Chambert-Loir]

#3692 specializes the preceding generation results to docs#SpecialLinearGroup.

[Antoine Chambert-Loir]

#33882 studies the commutators in docs#SpecialLinearGroup. With two exceptions (SL(2,2) and SL(2,3)), every transvection is a commutator, and the special linear group is equal to its commutator subgroup.

[Antoine Chambert-Loir]

#33715 defines the action of the special linear group on the projectivization of the space, and shows that it is 2-transitive, hence primitive.

[Antoine Chambert-Loir]

#33916 uses the Iwasawa criterion to conclude that docs#SpecialLinearGroup is quasi-simple, namely is simple modulo its center.