Upper-triangular general linear groups

For a commutative ring R, the upper-triangular general linear group consists of the invertible upper-triangular matrices over R. Reading off the diagonal defines a group homomorphism

B_m(R) → (m → Rˣ).

Its kernel is exactly the upper-unitriangular subgroup. The specialization to m = Fin 2 is TauCeti.GL2Borel; its pair-valued diagonal coordinates and its representation-theoretic API are defined in TauCeti.LinearAlgebra.Matrix.GeneralLinearGroup.Borel.

Main declarations

• TauCeti.upperTriangularGroup: the subgroup of upper-triangular elements of GL m R.
• TauCeti.UpperTriangularGroup.mem_comap_toGL_iff: its preimage in SL m R consists of the upper-triangular determinant-one matrices.
• TauCeti.UpperTriangularGroup.diag: the diagonal homomorphism to m → Rˣ.
• TauCeti.UpperTriangularGroup.diagonalHom: its section by diagonal matrices.
• TauCeti.UpperTriangularGroup.exists_det_eq_one_map_inv_mul_mul_map_mem: a triangularizing basis can be rescaled to have determinant one.
• TauCeti.UpperTriangularGroup.ker_diag: identification of the diagonal kernel.

References

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

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

The upper-triangular subgroup of GL_m(R) for a finite linearly ordered index type m.

Equations

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

@[simp]

theorem TauCeti.UpperTriangularGroup.mem_iff {m : Type u_1} [Fintype m] [LinearOrder m] {R : Type u} [CommRing R] {g : GL m R} : g ∈ upperTriangularGroup m R ↔ (↑g).IsUpperTriangular

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

theorem TauCeti.UpperTriangularGroup.isUpperTriangular {m : Type u_1} [Fintype m] [LinearOrder m] {R : Type u} [CommRing R] (g : ↥(upperTriangularGroup m R)) : (↑↑g).IsUpperTriangular

The matrix underlying an element of the upper-triangular group is upper triangular.

theorem TauCeti.UpperTriangularGroup.mem_comap_toGL_iff {m : Type u_1} [Fintype m] [LinearOrder m] {R : Type u} [CommRing R] {s : Matrix.SpecialLinearGroup m R} : s ∈ Subgroup.comap Matrix.SpecialLinearGroup.toGL (upperTriangularGroup m R) ↔ (↑s).IsUpperTriangular

A determinant-one matrix lies in the preimage of the upper-triangular group exactly when it is upper triangular.

def TauCeti.UpperTriangularGroup.map {m : Type u_1} [Fintype m] [LinearOrder m] {R : Type u} [CommRing R] {S : Type v} [CommRing S] (phi : R →+* S) : ↥(upperTriangularGroup m R) →* ↥(upperTriangularGroup m S)

Apply a ring homomorphism entrywise to an invertible upper-triangular matrix.

Equations

• TauCeti.UpperTriangularGroup.map phi = ((Matrix.GeneralLinearGroup.map phi).domRestrict (TauCeti.upperTriangularGroup m R)).codRestrict (TauCeti.upperTriangularGroup m S) ⋯

@[simp]

theorem TauCeti.UpperTriangularGroup.coe_map {m : Type u_1} [Fintype m] [LinearOrder m] {R : Type u} [CommRing R] {S : Type v} [CommRing S] (phi : R →+* S) (g : ↥(upperTriangularGroup m R)) : ↑((map phi) g) = (Matrix.GeneralLinearGroup.map phi) ↑g

The matrix underlying an entrywise-mapped upper-triangular element is the entrywise map of its underlying matrix.

theorem TauCeti.UpperTriangularGroup.map_apply {m : Type u_1} [Fintype m] [LinearOrder m] {R : Type u} [CommRing R] {S : Type v} [CommRing S] (phi : R →+* S) (g : ↥(upperTriangularGroup m R)) (i j : m) : ↑↑((map phi) g) i j = phi (↑↑g i j)

Entrywise application of a ring homomorphism to an upper-triangular matrix.

@[simp]

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

Entrywise mapping along the identity ring homomorphism is the identity.

@[simp]

theorem TauCeti.UpperTriangularGroup.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 entrywise maps agree with mapping along the composite ring homomorphism.

def TauCeti.UpperTriangularGroup.diag {m : Type u_1} [Fintype m] [LinearOrder m] {R : Type u} [CommRing R] : ↥(upperTriangularGroup m R) →* m → Rˣ

The diagonal projection from the upper-triangular group to the coordinatewise unit group.

Reading off the diagonal is multiplicative on upper-triangular matrices, so it is a homomorphism to m → R; MonoidHom.toHomUnits lifts it to the units of that product ring because the source is a group, and MulEquiv.piUnits distributes those units over the product.

Equations

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

@[simp]

theorem TauCeti.UpperTriangularGroup.diag_apply_val {m : Type u_1} [Fintype m] [LinearOrder m] {R : Type u} [CommRing R] (g : ↥(upperTriangularGroup m R)) (i : m) : ↑(diag g i) = ↑↑g i i

The value in R of the i-th coordinate of diag g is the i-th diagonal entry of g.

def TauCeti.UpperTriangularGroup.diagonalHom {m : Type u_1} [Fintype m] [LinearOrder m] {R : Type u} [CommRing R] : (m → Rˣ) →* ↥(upperTriangularGroup m R)

The diagonal matrices give a homomorphic section of the diagonal projection.

Equations

• TauCeti.UpperTriangularGroup.diagonalHom = TauCeti.diagGL.codRestrict (TauCeti.upperTriangularGroup m R) ⋯

@[simp]

theorem TauCeti.UpperTriangularGroup.coe_diagonalHom {m : Type u_1} [Fintype m] [LinearOrder m] {R : Type u} [CommRing R] (t : m → Rˣ) : ↑(diagonalHom t) = diagGL t

The element of GL underlying diagonalHom t is diagGL t.

@[simp]

theorem TauCeti.UpperTriangularGroup.diag_diagonalHom {m : Type u_1} [Fintype m] [LinearOrder m] {R : Type u} [CommRing R] (t : m → Rˣ) : diag (diagonalHom t) = t

Diagonal matrices form a section of the diagonal projection.

theorem TauCeti.UpperTriangularGroup.exists_det_eq_one_map_inv_mul_mul_map_mem {R : Type u} [CommRing R] {Q : Type u_2} {ι : Type u_3} [CommRing Q] [Fintype ι] [LinearOrder ι] (f : R →+* Q) (M : GL ι Q) (P : GL ι R) (h : ((Matrix.GeneralLinearGroup.map f) P)⁻¹ * M * (Matrix.GeneralLinearGroup.map f) P ∈ upperTriangularGroup ι Q) : ∃ (P' : GL ι R), Matrix.GeneralLinearGroup.det P' = 1 ∧ ((Matrix.GeneralLinearGroup.map f) P')⁻¹ * M * (Matrix.GeneralLinearGroup.map f) P' ∈ upperTriangularGroup ι Q

A triangularizing change of basis can be chosen with determinant one. Rescaling one column by the inverse determinant preserves the upper-triangular subgroup.

theorem TauCeti.UpperTriangularGroup.diag_surjective {m : Type u_1} [Fintype m] [LinearOrder m] {R : Type u} [CommRing R] : Function.Surjective ⇑diag

The diagonal projection is surjective.

theorem TauCeti.UpperTriangularGroup.upperUnitriangularGroup_le_upperTriangularGroup {m : Type u_1} [Fintype m] [LinearOrder m] {R : Type u} [CommRing R] : upperUnitriangularGroup m R ≤ upperTriangularGroup m R

The upper-unitriangular group is a subgroup of the upper-triangular group.

@[simp]

theorem TauCeti.UpperTriangularGroup.diag_eq_one_iff {m : Type u_1} [Fintype m] [LinearOrder m] {R : Type u} [CommRing R] {g : ↥(upperTriangularGroup m R)} : diag g = 1 ↔ ↑g ∈ upperUnitriangularGroup m R

The diagonal projection equals one exactly on elements whose underlying matrix is upper-unitriangular.

theorem TauCeti.UpperTriangularGroup.ker_diag {m : Type u_1} [Fintype m] [LinearOrder m] {R : Type u} [CommRing R] : diag.ker = (upperUnitriangularGroup m R).subgroupOf (upperTriangularGroup m R)

The kernel of the diagonal projection is the upper-unitriangular subgroup, viewed inside the upper-triangular group.