Diagonal elements of the general linear group, and the diagonal torus

A family of units indexed by a finite type ι is the diagonal of an invertible diagonal matrix, and this assignment is an injective group homomorphism TauCeti.diagGL : (ι → kˣ) →* GL ι k. Its entries, trace and determinant are recorded here, together with the fact that the diagonal entries of an invertible diagonal matrix are units.

The image of diagGL is the diagonal torus

TauCeti.diagonalTorus k n = (TauCeti.diagGL : (Fin n → kˣ) →* GL (Fin n) k).range

of GL n k, for which three descriptions are given. As the range of an injective homomorphism it is isomorphic to the coordinatewise units Fin n → kˣ (TauCeti.diagonalTorusEquiv), whence its order (q - 1)ⁿ over a division semiring with q elements (TauCeti.natCard_diagonalTorus). An invertible matrix lies in it exactly when it is diagonal (TauCeti.mem_diagonalTorus_iff). And over a commutative semiring with cancellation by nonzero elements and at least two units it is its own centralizer (TauCeti.centralizer_diagonalTorus), hence a maximal abelian subgroup of GL n k.

The hypothesis that kˣ is nontrivial cannot be dropped: over a semiring with a single unit, such as 𝔽₂, the torus is trivial (TauCeti.diagonalTorus_eq_bot) while its centralizer is the whole of GL n k (TauCeti.centralizer_diagonalTorus_eq_top).

A scalar matrix is central in GL ι k over any commutative semiring (TauCeti.scalar_mem_center), and diagGL sends a constant family to the corresponding scalar element (TauCeti.diagGL_const).

Main definitions

• TauCeti.diagGL embeds a family of units as an invertible diagonal matrix.
• TauCeti.diagonalTorus: the subgroup of invertible diagonal matrices in GL n k.
• TauCeti.diagonalTorusEquiv: the identification (Fin n → kˣ) ≃* diagonalTorus k n.
• TauCeti.detOneRescale: the explicit rescaling of the first column of an invertible matrix that makes its determinant one.

Main statements

• TauCeti.isUnit_apply_of_isDiag: the diagonal entries of an invertible diagonal matrix are units.
• TauCeti.exists_det_eq_one_mul_map_eq_map_mul_diagGL: a matrix intertwining another matrix with a diagonal matrix can be normalized to have determinant one while preserving the equation.
• TauCeti.mem_diagonalTorus_iff: membership in the torus is diagonality of the matrix.
• TauCeti.mul_diagGL_of_coe_eq_permMatrix: a permutation matrix moves past a diagonal by relabelling its entries.
• TauCeti.natCard_diagonalTorus: the torus has (q - 1)ⁿ elements over a division semiring with q elements.
• TauCeti.centralizer_diagonalTorus: the diagonal torus is its own centralizer.
• TauCeti.centralizer_diagonalTorus_eq_top: over a semiring with a single unit the centralizer is instead the whole group.
• TauCeti.scalar_mem_center and TauCeti.centralizer_scalar: a scalar matrix is central, so its centralizer is the whole group.
• TauCeti.diagGL_const and TauCeti.notMem_range_scalar_diagGL: the diagonal embedding sends a constant family to the corresponding scalar element, and it is scalar only there.

References

• W. Fulton and J. Harris, Representation Theory: A First Course (1991), Lecture 15.

def TauCeti.diagGL {k : Type u} {ι : Type u_1} [Fintype ι] [DecidableEq ι] [Semiring k] : (ι → kˣ) →* GL ι k

Coordinatewise units embed in a general linear group as diagonal matrices.

Equations

• TauCeti.diagGL = (Units.map ↑(Matrix.diagonalRingHom ι k)).comp MulEquiv.piUnits.symm.toMonoidHom

@[simp]

theorem TauCeti.diagGL_coe {k : Type u} {ι : Type u_1} [Fintype ι] [DecidableEq ι] [Semiring k] (t : ι → kˣ) : ↑(diagGL t) = Matrix.diagonal fun (i : ι) => ↑(t i)

The matrix underlying diagGL t is the diagonal matrix with entries t i.

@[simp]

theorem TauCeti.diagGL_apply {k : Type u} {ι : Type u_1} [Fintype ι] [DecidableEq ι] [Semiring k] (t : ι → kˣ) (i j : ι) : ↑(diagGL t) i j = if i = j then ↑(t i) else 0

The entries of diagGL t vanish off the diagonal and equal t i on it.

theorem TauCeti.trace_diagGL {k : Type u} {ι : Type u_1} [Fintype ι] [DecidableEq ι] [Semiring k] (t : ι → kˣ) : (↑(diagGL t)).trace = ∑ i : ι, ↑(t i)

The trace of a diagonal element of the general linear group is the sum of its diagonal entries.

theorem TauCeti.diagGL_injective {k : Type u} {ι : Type u_1} [Fintype ι] [DecidableEq ι] [Semiring k] : Function.Injective ⇑diagGL

The diagonal embedding is injective.

@[simp]

theorem TauCeti.diagGL_const {k : Type u} {ι : Type u_1} [Fintype ι] [DecidableEq ι] [Semiring k] (a : kˣ) : (diagGL fun (x : ι) => a) = (Matrix.GeneralLinearGroup.scalar ι) a

A constant family of units embeds as the corresponding scalar element of the general linear group. Together with TauCeti.notMem_range_scalar_diagGL this says that the diagonal embedding is scalar exactly on the constant families.

theorem TauCeti.notMem_range_scalar_diagGL {k : Type u} {ι : Type u_1} [Fintype ι] [DecidableEq ι] [Semiring k] {t : ι → kˣ} {i j : ι} (ht : t i ≠ t j) : ↑(diagGL t) ∉ Set.range ⇑(Matrix.scalar ι)

An invertible diagonal matrix with two distinct diagonal entries is not scalar.

theorem TauCeti.mul_diagGL_of_coe_eq_permMatrix {k : Type u} {ι : Type u_1} [Fintype ι] [DecidableEq ι] [Semiring k] (g : GL ι k) (π : Equiv.Perm ι) (hg : ↑g = Equiv.Perm.permMatrix k π) (d : ι → kˣ) : g * diagGL d = diagGL (d ∘ ⇑π) * g

A general-linear element whose underlying matrix is the permutation matrix of π moves past a diagonal matrix by relabelling its diagonal entries along π.

theorem TauCeti.isUnit_apply_of_isDiag {k : Type u} {ι : Type u_1} [Fintype ι] [DecidableEq ι] [Semiring k] {g : GL ι k} (hg : (↑g).IsDiag) (i : ι) : IsUnit (↑g i i)

The diagonal entries of an invertible diagonal matrix are units. Unlike Mathlib's Matrix.isUnit_diagonal, this assumes no commutativity of k.

def TauCeti.diagonalTorus (k : Type u) [Semiring k] (n : ℕ) : Subgroup (GL (Fin n) k)

The diagonal torus of GL n k: the image of the coordinatewise units under diagGL.

Equations

• TauCeti.diagonalTorus k n = TauCeti.diagGL.range

theorem TauCeti.mem_diagonalTorus_iff_exists_diagGL {k : Type u} {n : ℕ} [Semiring k] {g : GL (Fin n) k} : g ∈ diagonalTorus k n ↔ ∃ (t : Fin n → kˣ), diagGL t = g

Membership in the diagonal torus, read off its definition as a range: an element lies in it exactly when it is diagGL t for a family of units t.

@[simp]

theorem TauCeti.mem_diagonalTorus_iff {k : Type u} {n : ℕ} [Semiring k] {g : GL (Fin n) k} : g ∈ diagonalTorus k n ↔ (↑g).IsDiag

An invertible matrix lies in the diagonal torus exactly when it is a diagonal matrix.

noncomputable def TauCeti.diagonalTorusEquiv (k : Type u) [Semiring k] (n : ℕ) : (Fin n → kˣ) ≃* ↥(diagonalTorus k n)

The diagonal torus is the group of coordinatewise units.

Equations

• TauCeti.diagonalTorusEquiv k n = MonoidHom.ofInjective ⋯

@[simp]

theorem TauCeti.coe_diagonalTorusEquiv_apply {k : Type u} {n : ℕ} [Semiring k] (t : Fin n → kˣ) : ↑((diagonalTorusEquiv k n) t) = diagGL t

The torus element attached to a family of units is diagGL t.

@[simp]

theorem TauCeti.coe_diagonalTorusEquiv_symm_apply {k : Type u} {n : ℕ} [Semiring k] (g : ↥(diagonalTorus k n)) (i : Fin n) : ↑((diagonalTorusEquiv k n).symm g i) = ↑↑g i i

The i-th coordinate character of a torus element is its (i, i) matrix entry.

theorem TauCeti.natCard_diagonalTorus (k : Type u) [DivisionSemiring k] (n : ℕ) : Nat.card ↥(diagonalTorus k n) = (Nat.card k - 1) ^ n

The order of the diagonal torus: over a division semiring with q elements it has (q - 1)ⁿ elements, one invertible scalar per diagonal entry. Over an infinite division semiring both sides vanish when n > 0.

theorem TauCeti.commute_diagonal_of_mem_centralizer {k : Type u} {n : ℕ} [Semiring k] {g : GL (Fin n) k} (hg : g ∈ Subgroup.centralizer ↑(diagonalTorus k n)) (t : Fin n → kˣ) : Commute (Matrix.diagonal fun (i : Fin n) => ↑(t i)) ↑g

An element centralizing the diagonal torus commutes, as a matrix, with every diagonal matrix of units.

theorem TauCeti.diagonalTorus_eq_bot {k : Type u} {n : ℕ} [Semiring k] [Subsingleton kˣ] : diagonalTorus k n = ⊥

Over a semiring with only one unit, such as 𝔽₂, the diagonal torus is trivial.

theorem TauCeti.centralizer_diagonalTorus_eq_top {k : Type u} {n : ℕ} [Semiring k] [Subsingleton kˣ] : Subgroup.centralizer ↑(diagonalTorus k n) = ⊤

Over a semiring with only one unit the centralizer of the diagonal torus is the whole group, while the torus itself is trivial by TauCeti.diagonalTorus_eq_bot. So the hypothesis Nontrivial kˣ of TauCeti.centralizer_diagonalTorus cannot simply be dropped: the two subgroups differ as soon as GL n k is nontrivial, as it is over 𝔽₂ for n ≥ 2.

instance TauCeti.instIsMulCommutativeDiagonalTorus {k : Type u} {n : ℕ} [CommSemiring k] : IsMulCommutative ↥(diagonalTorus k n)

The diagonal torus is commutative.

theorem TauCeti.scalar_mem_center {k : Type u} {ι : Type u_1} [Fintype ι] [DecidableEq ι] [CommSemiring k] (u : kˣ) : (Matrix.GeneralLinearGroup.scalar ι) u ∈ Subgroup.center (GL ι k)

A scalar matrix is central in GL ι k. Mathlib's Matrix.GeneralLinearGroup.scalar_commute asks for a commutative ring.

@[simp]

theorem TauCeti.centralizer_scalar {k : Type u} {ι : Type u_1} [Fintype ι] [DecidableEq ι] [CommSemiring k] (u : kˣ) : Subgroup.centralizer {(Matrix.GeneralLinearGroup.scalar ι) u} = ⊤

The centralizer of a scalar matrix is everything, scalar matrices being central. The size of its conjugacy class is TauCeti.ncard_carrier_mk_scalar, in TauCeti.LinearAlgebra.Matrix.GeneralLinearGroup.Centralizer.

theorem TauCeti.centralizer_diagonalTorus {k : Type u} {n : ℕ} [CommSemiring k] [IsLeftCancelMulZero k] [Nontrivial kˣ] : Subgroup.centralizer ↑(diagonalTorus k n) = diagonalTorus k n

The diagonal torus is its own centralizer, hence a maximal abelian subgroup of GL n k.

theorem TauCeti.eq_diagonalTorus_of_le_of_isMulCommutative {k : Type u} {n : ℕ} [CommSemiring k] [IsLeftCancelMulZero k] [Nontrivial kˣ] (H : Subgroup (GL (Fin n) k)) [IsMulCommutative ↥H] (hle : diagonalTorus k n ≤ H) : H = diagonalTorus k n

A commutative subgroup of GL n k containing the diagonal torus equals it: this is the maximality of the torus among abelian subgroups.

@[simp]

theorem TauCeti.det_diagGL {k : Type u} {ι : Type u_1} [Fintype ι] [DecidableEq ι] [CommRing k] (t : ι → kˣ) : Matrix.GeneralLinearGroup.det (diagGL t) = ∏ i : ι, t i

The determinant of a diagonal matrix is the product of its diagonal entries.

@[simp]

theorem TauCeti.map_diagGL {k : Type u} {ι : Type u_1} [Fintype ι] [DecidableEq ι] [CommRing k] {S : Type u_2} [CommRing S] (f : k →+* S) (t : ι → kˣ) : (Matrix.GeneralLinearGroup.map f) (diagGL t) = diagGL fun (i : ι) => (Units.map ↑f) (t i)

Mapping the entries of diagGL t along a ring homomorphism gives the diagonal matrix of the mapped units.

theorem TauCeti.exists_det_mul_diagGL_eq_one {k : Type u} {ι : Type u_1} [Fintype ι] [DecidableEq ι] [CommRing k] (P : GL ι k) : ∃ (u : ι → kˣ), Matrix.GeneralLinearGroup.det (P * diagGL u) = 1

Rescaling one column makes an invertible matrix have determinant one. For an empty index type, every invertible matrix already has determinant one.

def TauCeti.detOneRescale {k : Type u} {n : ℕ} [CommRing k] (g : GL (Fin n) k) : GL (Fin n) k

Rescale the first column of an invertible matrix by the inverse of its determinant. The result has determinant one (TauCeti.det_detOneRescale), and the operation is the identity on determinant-one matrices (TauCeti.detOneRescale_of_det_eq_one).

Unlike TauCeti.exists_det_mul_diagGL_eq_one, the rescaling is an explicit formula, so it commutes with entrywise ring homomorphisms (TauCeti.map_detOneRescale): it is a morphism of schemes GLₙ → SLₙ. In rank zero it is the identity.

Equations

• TauCeti.detOneRescale g = g * TauCeti.diagGL fun (i : Fin n) => if ↑i = 0 then (Matrix.GeneralLinearGroup.det g)⁻¹ else 1

theorem TauCeti.detOneRescale_def {k : Type u} {n : ℕ} [CommRing k] (g : GL (Fin n) k) : detOneRescale g = g * diagGL fun (i : Fin n) => if ↑i = 0 then (Matrix.GeneralLinearGroup.det g)⁻¹ else 1

The determinant-one rescaling multiplies on the right by the diagonal matrix diag((det g)⁻¹, 1, …, 1).

@[simp]

theorem TauCeti.det_detOneRescale {k : Type u} {n : ℕ} [CommRing k] (g : GL (Fin n) k) : Matrix.GeneralLinearGroup.det (detOneRescale g) = 1

The determinant-one rescaling has determinant one.

theorem TauCeti.detOneRescale_of_det_eq_one {k : Type u} {n : ℕ} [CommRing k] {g : GL (Fin n) k} (hg : Matrix.GeneralLinearGroup.det g = 1) : detOneRescale g = g

The determinant-one rescaling fixes matrices of determinant one.

theorem TauCeti.map_detOneRescale {k : Type u} {n : ℕ} [CommRing k] {S : Type u_2} [CommRing S] (f : k →+* S) (g : GL (Fin n) k) : (Matrix.GeneralLinearGroup.map f) (detOneRescale g) = detOneRescale ((Matrix.GeneralLinearGroup.map f) g)

The determinant-one rescaling commutes with mapping the entries along a ring homomorphism.

theorem TauCeti.exists_det_eq_one_mul_map_eq_map_mul_diagGL {k : Type u} {ι : Type u_1} [Fintype ι] [DecidableEq ι] [CommRing k] {Q : Type u_2} [CommRing Q] (f : k →+* Q) (M : GL ι Q) (P : GL ι k) (t : ι → Qˣ) (h : M * (Matrix.GeneralLinearGroup.map f) P = (Matrix.GeneralLinearGroup.map f) P * diagGL t) : ∃ (P' : GL ι k), Matrix.GeneralLinearGroup.det P' = 1 ∧ M * (Matrix.GeneralLinearGroup.map f) P' = (Matrix.GeneralLinearGroup.map f) P' * diagGL t

If P intertwines M with a diagonal matrix, there is an intertwining matrix of determinant one, obtained in the nonempty case by rescaling one of the columns of P.

theorem TauCeti.det_of_mem_diagonalTorus {k : Type u} {n : ℕ} [CommRing k] {g : GL (Fin n) k} (hg : g ∈ diagonalTorus k n) : ↑(Matrix.GeneralLinearGroup.det g) = ∏ i : Fin n, ↑g i i

The determinant of an element of the diagonal torus is the product of its diagonal entries.