Nilpotence of upper-unitriangular matrix groups

For a ring R, filter U_n(R) by requiring the entries on the first r - 1 superdiagonals to vanish. Multiplication of matrices supported at least r and s superdiagonals above the diagonal is supported at least r + s superdiagonals above it. This gives the central-series estimate

[U^r, U^s] ⊆ U^(r+s).

The first term is all of U_n(R), while the n-th term is trivial. Hence U_n(R) is nilpotent, and therefore solvable, over every ring.

Main declarations

• TauCeti.UpperUnitriangularGroup.superdiagonalSubgroup: the subgroup U^r whose first r - 1 superdiagonals vanish.
• TauCeti.UpperUnitriangularGroup.superdiagonalSubgroup_antitone: the filtration is decreasing.
• TauCeti.UpperUnitriangularGroup.commutator_superdiagonalSubgroup_le: the central-series estimate [U^r, U^s] ≤ U^(r+s).
• TauCeti.UpperUnitriangularGroup.instIsNilpotent: upper-unitriangular matrix groups are nilpotent.

References

• T. A. Springer, Linear Algebraic Groups, §2.4.
• J. C. Jantzen, Representations of Algebraic Groups, I.2.

This is the nilpotence input for Layer 5, "Lie--Kolchin; solvable groups", of the ReductiveGroups roadmap. Combined with the upper-unitriangular embedding characterization, it gives the implication from unipotence to solvability.

def TauCeti.UpperUnitriangularGroup.superdiagonalSubgroup {R : Type u} [Ring R] {n : ℕ} (r : ℕ) : Subgroup ↥(upperUnitriangularGroup (Fin n) R)

The subgroup U^r of upper-unitriangular matrices whose entries below the r-th superdiagonal vanish. Thus U^1 = U_n, and U^n = 1 for n × n matrices.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.UpperUnitriangularGroup.mem_superdiagonalSubgroup_iff {R : Type u} [Ring R] {n : ℕ} (r : ℕ) (g : ↥(upperUnitriangularGroup (Fin n) R)) : g ∈ superdiagonalSubgroup r ↔ ∀ (i j : Fin n), ↑j < ↑i + r → ↑↑g i j = 1 i j

Membership in U^r means that the matrix differs from the identity only on the r-th and higher superdiagonals.

theorem TauCeti.UpperUnitriangularGroup.superdiagonalSubgroup_antitone {R : Type u} [Ring R] {n : ℕ} : Antitone superdiagonalSubgroup

The superdiagonal filtration is decreasing: requiring more initial superdiagonals to vanish gives a smaller subgroup.

@[simp]

theorem TauCeti.UpperUnitriangularGroup.superdiagonalSubgroup_one {R : Type u} [Ring R] {n : ℕ} : superdiagonalSubgroup 1 = ⊤

The first superdiagonal subgroup is the whole upper-unitriangular group.

theorem TauCeti.UpperUnitriangularGroup.superdiagonalSubgroup_eq_bot_of_le {R : Type u} [Ring R] {n r : ℕ} (hnr : n ≤ r) : superdiagonalSubgroup r = ⊥

Once the filtration index reaches the matrix size, the superdiagonal subgroup is trivial.

theorem TauCeti.UpperUnitriangularGroup.commutator_superdiagonalSubgroup_le {R : Type u} [Ring R] {n : ℕ} (r s : ℕ) : ⁅superdiagonalSubgroup r, superdiagonalSubgroup s⁆ ≤ superdiagonalSubgroup (r + s)

Commutators add filtration degrees: [U^r, U^s] ≤ U^(r+s).

instance TauCeti.UpperUnitriangularGroup.instIsNilpotent {R : Type u} [Ring R] {m : Type u_1} [Fintype m] [LinearOrder m] : Group.IsNilpotent ↥(upperUnitriangularGroup m R)

Upper-unitriangular matrices over every finite linearly ordered index type form a nilpotent group over every ring.