The Jordan normal form of GL₂ and its centralizing subgroup

Alongside the scalars, the split torus and the non-split torus, the fourth family of conjugacy classes of GL₂(𝔽_q) is the non-semisimple one, represented by a single Jordan block !![a, 1; 0, a] with a repeated eigenvalue. This file names that normal form,

TauCeti.jordanGL a b = !![a, b; 0, a],

and the subgroup of GL (Fin 2) R in which its centralizer will be found: the matrices !![x, y; 0, x], the invertible elements of the algebra R[N] generated by a single nilpotent Jordan block N. That subgroup is the product of the scalar matrices with the unipotent radical of the Borel subgroup, Z U, so it is presented as the image of the homomorphism

TauCeti.scalarUnipotentHom : Rˣ × Multiplicative R →* GL (Fin 2) R, (x, t) ↦ x · (1 + t E₀₁),

built from Matrix.GeneralLinearGroup.scalar and the root subgroup TauCeti.transvectionHom, whose images commute because scalar matrices are central. The homomorphism is injective, so the subgroup is a faithful copy of Rˣ × (R, +) — the direct product Gₘ × Gₐ — and over a field with q elements it has (q - 1) q elements.

Nothing here is specific to a finite field, or even to a field: the normal form is stated over an arbitrary ring, the subgroup and the isomorphism Rˣ × (R, +) ≃* Z U over an arbitrary commutative ring, and only the order count asks for a field, where the nonzero elements are exactly the units.

The parameter b is left free rather than fixed to 1. That costs no generality: a Jordan block with b a unit is conjugate to the standard representative !![a, 1; 0, a] (TauCeti.isConj_jordanGL), by the diagonal matrix that rescales the off-diagonal entry. Leaving it free also lets the degenerate case b = 0, the scalar matrix, be named by the same construction; the results that need b ≠ 0 say so.

The centralizer computation itself, and the resulting conjugacy class size, are in TauCeti.LinearAlgebra.Matrix.GeneralLinearGroup.Centralizer, next to the split and non-split ones.

Main definitions

• TauCeti.jordanGL: the invertible matrix !![a, b; 0, a] with a repeated diagonal unit.
• TauCeti.scalarUnipotentHom: the homomorphism (x, t) ↦ !![x, x t; 0, x] from Rˣ times the additive group of R.
• TauCeti.GL2ScalarUnipotent: its range, the subgroup Z U of GL (Fin 2) R.
• TauCeti.GL2ScalarUnipotent.mulEquiv: the resulting isomorphism Rˣ × Multiplicative R ≃* Z U.

Main results

• TauCeti.jordanGL_eq_scalar_mul_transvectionUnit: a Jordan block is a scalar matrix times a transvection, M = a (1 + a⁻¹ b E₀₁).
• TauCeti.mem_gl2ScalarUnipotent_iff: an element of GL₂ lies in Z U exactly when it is !![x, y; 0, x] for a unit x.
• TauCeti.notMem_range_scalar_jordanGL: a Jordan block with b ≠ 0 is not a scalar matrix. Over a field that is exactly the hypothesis of TauCeti.commute_fin_two_iff, which is what makes such a block a regular element of GL₂.
• TauCeti.isConj_jordanGL: a Jordan block whose off-diagonal entry is a unit is conjugate to !![a, 1; 0, a].
• TauCeti.natCard_gl2ScalarUnipotent: over a field with q elements, |Z U| = (q - 1) q.

References

• Character theory roadmap, Layer 9, "The conjugacy classes (a build target)".
• C. Bonnafé, Representations of SL₂(𝔽_q) (2011), Chapter 1.
• W. Fulton and J. Harris, Representation Theory: A First Course (1991), Lecture 5.2.

def TauCeti.jordanGL {R : Type u} [Ring R] (a : Rˣ) (b : R) : GL (Fin 2) R

The Jordan block !![a, b; 0, a] in GL (Fin 2) R: the upper-triangular invertible matrix whose two diagonal entries are the same unit a. It is TauCeti.GL2Borel.mk with its two diagonal arguments made equal, so the whole Borel API — the diagonal projection, the determinant, the splitting B = T U — applies to it; for b = 0 it is the scalar matrix a (jordanGL_zero).

Over a field and for b ≠ 0 this is the non-semisimple normal form of GL₂, a single Jordan block with repeated eigenvalue a, and it is then one of the four conjugacy class representatives of GL₂(𝔽_q), alongside the scalars, TauCeti.diagGL and TauCeti.GL2NonSplitTorusHom. Over an arbitrary ring no such claim is made: only the matrix shape is.

Equations

• TauCeti.jordanGL a b = TauCeti.GL2Borel.mk a a b

@[simp]

theorem TauCeti.coe_jordanGL {R : Type u} [Ring R] (a : Rˣ) (b : R) : ↑(jordanGL a b) = !![↑a, b; 0, ↑a]

theorem TauCeti.trace_jordanGL {R : Type u} [Ring R] (a : Rˣ) (b : R) : (↑(jordanGL a b)).trace = 2 * ↑a

The trace of a Jordan block is twice its repeated eigenvalue.

@[simp]

theorem TauCeti.jordanGL_zero {R : Type u} [Ring R] (a : Rˣ) : jordanGL a 0 = (Matrix.GeneralLinearGroup.scalar (Fin 2)) a

A Jordan block with zero off-diagonal entry is the scalar matrix.

theorem TauCeti.jordanGL_injective2 {R : Type u} [Ring R] : Function.Injective2 jordanGL

Two Jordan blocks are equal exactly when their parameters are: the diagonal entry and the upper-right entry can both be read off the matrix.

theorem TauCeti.notMem_range_scalar_jordanGL {R : Type u} [Ring R] {a : Rˣ} {b : R} (hb : b ≠ 0) : ↑(jordanGL a b) ∉ Set.range ⇑(Matrix.scalar (Fin 2))

A Jordan block with a nonzero off-diagonal entry is not a scalar matrix. Over a field that is exactly the hypothesis of TauCeti.commute_fin_two_iff — it is what makes the block a regular (cyclic, nonderogatory) element of GL₂, with commutant the two-dimensional algebra F[M] — and it is exactly the non-semisimple case, b ≠ 0. Over a general ring no such conclusion is claimed here.

theorem TauCeti.jordanGL_mem_gl2Borel {R : Type u} [CommRing R] (a : Rˣ) (b : R) : jordanGL a b ∈ GL2Borel R

A Jordan block is upper triangular, so it lies in the Borel subgroup: it is TauCeti.GL2Borel.mk with its two diagonal arguments made equal.

@[simp]

theorem TauCeti.det_jordanGL {R : Type u} [CommRing R] (a : Rˣ) (b : R) : Matrix.GeneralLinearGroup.det (jordanGL a b) = a ^ 2

The determinant of a Jordan block is the square of its repeated eigenvalue.

def TauCeti.scalarUnipotentHom (R : Type u) [CommRing R] : Rˣ × Multiplicative R →* GL (Fin 2) R

The scalar–unipotent subgroup homomorphism of GL₂: a unit x and an element t of the additive group of R are sent to x · (1 + t E₀₁) = !![x, x t; 0, x].

It is the coproduct of the scalar matrices Matrix.GeneralLinearGroup.scalar and the root subgroup TauCeti.transvectionHom of the root ε₀ - ε₁, which commute because scalar matrices are central; so its image is the internal product Z U of the centre with the unipotent radical of the Borel subgroup. The coordinate t is the unipotent one rather than the upper-right matrix entry, which is what makes the assignment multiplicative: the upper-right entries of a product pick up the diagonal factors, while the unipotent coordinates simply add.

Equations

• TauCeti.scalarUnipotentHom R = (Matrix.GeneralLinearGroup.scalar (Fin 2)).noncommCoprod (TauCeti.transvectionHom TauCeti.scalarUnipotentHom._proof_2✝) ⋯

theorem TauCeti.scalarUnipotentHom_eq_mul (R : Type u) [CommRing R] (p : Rˣ × Multiplicative R) : (scalarUnipotentHom R) p = (Matrix.GeneralLinearGroup.scalar (Fin 2)) p.1 * (transvectionHom ⋯) p.2

The scalar–unipotent homomorphism is the product of its two factors: the scalar matrix of the first coordinate times the transvection of the second.

@[simp]

theorem TauCeti.scalarUnipotentHom_apply {R : Type u} [CommRing R] (p : Rˣ × Multiplicative R) : (scalarUnipotentHom R) p = jordanGL p.1 (↑p.1 * Multiplicative.toAdd p.2)

theorem TauCeti.jordanGL_eq_scalar_mul_transvectionUnit {R : Type u} [CommRing R] (a : Rˣ) (b : R) : jordanGL a b = (Matrix.GeneralLinearGroup.scalar (Fin 2)) a * transvectionUnit ⋯ (↑a⁻¹ * b)

A Jordan block is a scalar matrix times a transvection: !![a, b; 0, a] = a · (1 + a⁻¹ b E₀₁) is the decomposition M = a (1 + N) into a central factor and a unipotent one. It is TauCeti.scalarUnipotentHom_eq_mul read on the Jordan block, and it is what lets the root subgroup API — conjugation by the diagonal torus, in particular — be applied to M. Over a field it is the multiplicative Jordan decomposition of M, whose unipotent part is trivial exactly when b = 0; so it exhibits M as non-semisimple precisely in the case b ≠ 0.

theorem TauCeti.isConj_jordanGL {R : Type u} [CommRing R] (a b : Rˣ) : IsConj (jordanGL a ↑b) (jordanGL a 1)

Normalizing the off-diagonal entry. A Jordan block whose off-diagonal entry is a unit is conjugate, by the diagonal matrix diag (1, b), to the standard representative !![a, 1; 0, a]. The scalar factor of TauCeti.jordanGL_eq_scalar_mul_transvectionUnit is central, and conjugation rescales the parameter of the remaining transvection by the value 1 · b⁻¹ of the root ε₀ - ε₁ (TauCeti.diagGL_mul_transvectionUnit_mul_inv). Over a field this applies to every b ≠ 0 through Units.mk0, so leaving b free below costs no generality.

theorem TauCeti.scalarUnipotentHom_injective {R : Type u} [CommRing R] : Function.Injective ⇑(scalarUnipotentHom R)

The scalar–unipotent homomorphism is injective: the pair (x, t) is read back off the matrix !![x, x t; 0, x] as its upper-left entry and the quotient of its two top entries. So Z U is a faithful copy of Rˣ × (R, +), not a quotient of it.

def TauCeti.GL2ScalarUnipotent (R : Type u) [CommRing R] : Subgroup (GL (Fin 2) R)

The scalar–unipotent subgroup Z U of GL (Fin 2) R: the invertible matrices !![x, y; 0, x], that is, the units of the commutative subalgebra R[N] generated by a nilpotent Jordan block. It is the product of the centre with the unipotent radical of the Borel subgroup, and it is the centralizer of every Jordan block !![a, b; 0, a] whose off-diagonal entry b is left-regular — over a field, every b ≠ 0 (TauCeti.centralizer_jordanGL).

Equations

• TauCeti.GL2ScalarUnipotent R = (TauCeti.scalarUnipotentHom R).range

instance TauCeti.instIsMulCommutativeSubtypeGeneralLinearGroupFinOfNatNatMemSubgroupGL2ScalarUnipotent {R : Type u} [CommRing R] : IsMulCommutative ↥(GL2ScalarUnipotent R)

The scalar–unipotent subgroup is abelian: it is the image of the commutative group Rˣ × Multiplicative R.

@[simp]

theorem TauCeti.mem_gl2ScalarUnipotent_iff {R : Type u} [CommRing R] {g : GL (Fin 2) R} : g ∈ GL2ScalarUnipotent R ↔ ∃ (x : Rˣ) (y : R), g = jordanGL x y

Normal form for the scalar–unipotent subgroup: its elements are exactly the invertible matrices !![x, y; 0, x] with equal diagonal entries. The upper-right entry y is unconstrained; it is the product of the diagonal unit with the unipotent coordinate.

theorem TauCeti.jordanGL_mem_gl2ScalarUnipotent {R : Type u} [CommRing R] (x : Rˣ) (y : R) : jordanGL x y ∈ GL2ScalarUnipotent R

Every Jordan block lies in the scalar–unipotent subgroup, the degenerate case b = 0 — the scalar matrix — included.

noncomputable def TauCeti.GL2ScalarUnipotent.mulEquiv (R : Type u) [CommRing R] : Rˣ × Multiplicative R ≃* ↥(GL2ScalarUnipotent R)

The scalar–unipotent subgroup is Gₘ × Gₐ: the multiplicative group of R times its additive group, the scalar and unipotent coordinates. This is the isomorphism the order count runs on.

Equations

• TauCeti.GL2ScalarUnipotent.mulEquiv R = MonoidHom.ofInjective ⋯

theorem TauCeti.GL2ScalarUnipotent.coe_mulEquiv_apply {R : Type u} [CommRing R] (p : Rˣ × Multiplicative R) : ↑((mulEquiv R) p) = (scalarUnipotentHom R) p

The isomorphism Rˣ × (R, +) ≃* Z U is TauCeti.scalarUnipotentHom with its codomain cut down, so no unfolding of MonoidHom.ofInjective is needed to compute with it. This is not a simp lemma because its right-hand side is not in simp-normal form: simp rewrites it further by TauCeti.scalarUnipotentHom_apply, which is what the companion TauCeti.GL2ScalarUnipotent.coe_mulEquiv_apply_eq_jordanGL states.

@[simp]

theorem TauCeti.GL2ScalarUnipotent.coe_mulEquiv_apply_eq_jordanGL {R : Type u} [CommRing R] (p : Rˣ × Multiplicative R) : ↑((mulEquiv R) p) = jordanGL p.1 (↑p.1 * Multiplicative.toAdd p.2)

The matrix underlying TauCeti.GL2ScalarUnipotent.mulEquiv R p is the Jordan block !![x, x t; 0, x] read off the pair p = (x, t).

theorem TauCeti.natCard_gl2ScalarUnipotent (F : Type u) [Field F] : Nat.card ↥(GL2ScalarUnipotent F) = (Nat.card F - 1) * Nat.card F

The order of the scalar–unipotent subgroup: over a field with q elements it has (q - 1) q elements, one invertible scalar and one free unipotent coordinate. No finiteness is assumed: over an infinite field both sides vanish.