Upper-unitriangular matrix groups

For a ring R, the upper-unitriangular group Uₙ(R) consists of the invertible upper-triangular matrices whose diagonal entries are all one. This file packages these matrices as a subgroup of GLₙ(R), proves functoriality for commutative coefficient rings, and verifies that their natural linear action is unipotent in the commutative case.

The nilpotence calculation is valid over every ring: if N is a strictly upper-triangular n × n matrix, then N ^ n = 0. Applying it to g - 1 proves that every element of Uₙ(R) is unipotent. This is the matrix-group input for the upper-unitriangular embedding characterization in Layer 5, "Unipotent groups", of the ReductiveGroups roadmap.

Main declarations

• TauCeti.upperUnitriangularGroup: the subgroup Uₙ(R) of GLₙ(R).
• TauCeti.UpperUnitriangularGroup.ext: upper-unitriangular group elements are determined by their entries strictly above the diagonal.
• TauCeti.UpperUnitriangularGroup.map: base change along a ring homomorphism.
• TauCeti.UpperUnitriangularGroup.isUnipotent_toLin: the natural representation of every element of Uₙ(R) is unipotent.

References

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

noncomputable def Matrix.IsUpperUnitriangular.toGL {R : Type u_1} {m : Type u_2} [Fintype m] [LinearOrder m] [Ring R] {M : Matrix m m R} (hM : M.IsUpperUnitriangular) : GL m R

Package an upper-unitriangular matrix as an element of the general linear group.

Equations

• hM.toGL = ⋯.unit

@[simp]

theorem Matrix.IsUpperUnitriangular.coe_toGL {R : Type u_1} {m : Type u_2} [Fintype m] [LinearOrder m] [Ring R] {M : Matrix m m R} (hM : M.IsUpperUnitriangular) : ↑hM.toGL = M

The matrix underlying IsUpperUnitriangular.toGL is the original matrix.

def TauCeti.upperUnitriangularGroup (m : Type u_1) [Fintype m] [LinearOrder m] (R : Type u) [Ring R] : Subgroup (GL m R)

The upper-unitriangular subgroup of GLₘ(R) for a finite linearly ordered index type m.

Equations

• TauCeti.upperUnitriangularGroup m R = { carrier := {g : GL m R | (↑g).IsUpperUnitriangular}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

@[simp]

theorem TauCeti.UpperUnitriangularGroup.mem_iff {m : Type u_1} [Fintype m] [LinearOrder m] {R : Type u} [Ring R] {g : GL m R} : g ∈ upperUnitriangularGroup m R ↔ (↑g).IsUpperUnitriangular

Membership in the upper-unitriangular group means that the underlying matrix is upper unitriangular.

theorem TauCeti.UpperUnitriangularGroup.isUpperUnitriangular {m : Type u_1} [Fintype m] [LinearOrder m] {R : Type u} [Ring R] (g : ↥(upperUnitriangularGroup m R)) : (↑↑g).IsUpperUnitriangular

The underlying matrix of an element of Uₙ(R) is upper unitriangular.

theorem TauCeti.UpperUnitriangularGroup.isUpperTriangular {m : Type u_1} [Fintype m] [LinearOrder m] {R : Type u} [Ring R] (g : ↥(upperUnitriangularGroup m R)) : (↑↑g).IsUpperTriangular

An upper-unitriangular matrix is upper triangular.

@[simp]

theorem TauCeti.UpperUnitriangularGroup.apply_diag {m : Type u_1} [Fintype m] [LinearOrder m] {R : Type u} [Ring R] (g : ↥(upperUnitriangularGroup m R)) (i : m) : ↑↑g i i = 1

Every diagonal entry of an upper-unitriangular matrix is one.

theorem TauCeti.UpperUnitriangularGroup.ext {m : Type u_1} [Fintype m] [LinearOrder m] {R : Type u} [Ring R] {g h : ↥(upperUnitriangularGroup m R)} (heq : ∀ (i j : m), i < j → ↑↑g i j = ↑↑h i j) : g = h

Two upper-unitriangular group elements are equal if their entries strictly above the diagonal agree.

theorem TauCeti.UpperUnitriangularGroup.ext_iff {m : Type u_1} [Fintype m] [LinearOrder m] {R : Type u} [Ring R] {g h : ↥(upperUnitriangularGroup m R)} : g = h ↔ ∀ (i j : m), i < j → ↑↑g i j = ↑↑h i j

theorem TauCeti.UpperUnitriangularGroup.toGL_mem_upperUnitriangularGroup {m : Type u_1} [Fintype m] [LinearOrder m] {R : Type u} [Ring R] {M : Matrix m m R} (hM : M.IsUpperUnitriangular) : hM.toGL ∈ upperUnitriangularGroup m R

Packaging an upper-unitriangular matrix as an element of GLₘ(R) lands in the upper-unitriangular subgroup.

def TauCeti.UpperUnitriangularGroup.map {m : Type u_1} [Fintype m] [LinearOrder m] {R : Type u} [CommRing R] {S : Type u_2} [CommRing S] (f : R →+* S) : ↥(upperUnitriangularGroup m R) →* ↥(upperUnitriangularGroup m S)

Applying a ring homomorphism entrywise gives the base-change homomorphism between upper-unitriangular groups.

Equations

• TauCeti.UpperUnitriangularGroup.map f = ((Matrix.GeneralLinearGroup.map f).domRestrict (TauCeti.upperUnitriangularGroup m R)).codRestrict (TauCeti.upperUnitriangularGroup m S) ⋯

@[simp]

theorem TauCeti.UpperUnitriangularGroup.coe_map {m : Type u_1} [Fintype m] [LinearOrder m] {R : Type u} [CommRing R] {S : Type u_2} [CommRing S] (f : R →+* S) (g : ↥(upperUnitriangularGroup m R)) : ↑((map f) g) = (Matrix.GeneralLinearGroup.map f) ↑g

The underlying GLₘ element of base change is Mathlib's base change map.

theorem TauCeti.UpperUnitriangularGroup.map_apply {m : Type u_1} [Fintype m] [LinearOrder m] {R : Type u} [CommRing R] {S : Type u_2} [CommRing S] (f : R →+* S) (g : ↥(upperUnitriangularGroup m R)) (i j : m) : ↑↑((map f) g) i j = f (↑↑g i j)

Base change acts entrywise on upper-unitriangular matrices.

@[simp]

theorem TauCeti.UpperUnitriangularGroup.map_id {m : Type u_1} [Fintype m] [LinearOrder m] {R : Type u} [CommRing R] : map (RingHom.id R) = MonoidHom.id ↥(upperUnitriangularGroup m R)

Base change along the identity ring homomorphism is the identity.

@[simp]

theorem TauCeti.UpperUnitriangularGroup.map_comp {m : Type u_1} [Fintype m] [LinearOrder m] {R : Type u} [CommRing R] {S : Type u_2} {T : Type u_3} [CommRing S] [CommRing T] (f : R →+* S) (g : S →+* T) : map (g.comp f) = (map g).comp (map f)

Successive base changes agree with base change along the composite ring homomorphism.

theorem TauCeti.UpperUnitriangularGroup.isUnipotent_toLin {m : Type u_1} [Fintype m] [LinearOrder m] {R : Type u} [CommRing R] (g : ↥(upperUnitriangularGroup m R)) : (Matrix.GeneralLinearGroup.toLin ↑g).IsUnipotent

The natural linear action of every upper-unitriangular matrix is unipotent.