The four conjugacy normal forms of GL₂ over a finite field

TauCeti/LinearAlgebra/Matrix/GeneralLinearGroup/ConjugacyClasses.lean classifies the conjugacy classes of GL₂(F) by trace and determinant, with the companion matrix of the characteristic polynomial as the representative of each non-scalar class. That representative is uniform but anonymous. This file replaces it, over a finite field, by the four named normal forms the character theory of GL₂(𝔽_q) is written against:

• a central scalar matrix a • 1;
• a split semisimple TauCeti.diagGL ![a, b] with a ≠ b;
• a non-semisimple Jordan block TauCeti.jordanGL a 1;
• an elliptic TauCeti.GL2NonSplitTorusHom F E x, multiplication by an element of a degree-2 extension E/F that does not lie in F.

TauCeti.exists_isConj_normalForm is the resulting statement that every element of GL₂(F) is conjugate to one of the four. It is what turns the four character values computed at these normal forms in TauCeti/RepresentationTheory/CharacterTable/GL2/CharacterValues.lean into a full row of the character table of GL₂(𝔽_q): a character is a class function, so a row is determined once the normal forms exhaust the classes.

The two non-central split forms need no finiteness and no extension. Each is the same check against TauCeti.isConj_iff_of_notMem_range_scalar: the normal form is not scalar, and its trace and determinant are the prescribed ones. What the roots of X² - t X + d are is the only thing that distinguishes them — two distinct roots give diagGL, a repeated root gives jordanGL — and only in the repeated-root case need non-scalarness be assumed: a scalar matrix has a repeated root, so prescribing two distinct roots, or a root outside F, already rules it out.

The elliptic case is the one that needs a quadratic extension, and it is where the finiteness of F enters. Multiplication by x : E has trace Tr_{E/F} x and determinant N_{E/F} x (TauCeti.GL2NonSplitTorus.trace_gl2NonSplitTorusHom and TauCeti.GL2NonSplitTorus.val_det_gl2NonSplitTorusHom), so the normal form is pinned by the quadratic-extension lemmas of TauCeti/FieldTheory/Quadratic.lean: TauCeti.Algebra.trace_eq_of_mul_self_eq and TauCeti.Algebra.norm_eq_of_mul_self_eq identify those with t and d for an x outside F satisfying x² = t x - d, and TauCeti.exists_mul_self_eq_of_finite supplies such an x over a finite field.

Uniqueness — that the four families are pairwise disjoint and that the parameters are determined up to the evident symmetries (a, b) ↦ (b, a) and x ↦ x^q — is the second half of the file, and it runs on the same classification. Being scalar is a conjugacy invariant on its own (TauCeti.not_isConj_of_mem_range_scalar), which separates the central family from the other three; that is the one separation trace and determinant do not make, a scalar and a Jordan block with the same eigenvalue having the same characteristic polynomial. Among the three non-central families the characteristic polynomial does all the work, and what separates them is how it factors: two distinct roots in F for diagGL, a repeated root for jordanGL, and no root in F for the elliptic form. Reading that off is one equation per pair, and in the elliptic case it needs the torus parameter x to satisfy the quadratic built from its own trace and norm, Algebra.IsQuadraticExtension.sq_eq_trace_smul_sub_norm: an eigenvalue of a split or a Jordan form lies in F, and x does not.

None of those statements needs F finite, and the split and non-semisimple ones need no extension at all. What does need finiteness is the symmetry x ↦ x^q of the elliptic parameter, which is TauCeti.GL2NonSplitTorus.isConj_gl2NonSplitTorusHom_iff in TauCeti/LinearAlgebra/Matrix/GeneralLinearGroup/ConjugacyClasses.lean. Together with the results here it says that the four families, with their parameters read up to the two symmetries, index the conjugacy classes of GL₂(𝔽_q) without repetition — the description by named data of the indexing that TauCeti.conjClassesGLFinTwoEquiv supplies anonymously.

Main results

• TauCeti.isConj_diagGL_of_trace_of_det, TauCeti.isConj_jordanGL_one_of_trace_of_det and TauCeti.isConj_gl2NonSplitTorusHom_of_trace_of_det: the three non-central normal forms, each characterized by the roots of its characteristic polynomial, read off the trace and the determinant.
• TauCeti.exists_isConj_normalForm: every element of GL₂(F), for F finite with a degree-2 extension E, is conjugate to one of the four normal forms.
• TauCeti.not_isConj_scalar_diagGL, TauCeti.not_isConj_scalar_jordanGL_one, TauCeti.not_isConj_scalar_gl2NonSplitTorusHom, TauCeti.not_isConj_diagGL_jordanGL_one, TauCeti.not_isConj_diagGL_gl2NonSplitTorusHom and TauCeti.not_isConj_jordanGL_one_gl2NonSplitTorusHom: the four families are pairwise disjoint.
• TauCeti.isConj_diagGL_iff and TauCeti.isConj_jordanGL_one_iff: the parameters inside a family are determined, the split family up to the transposition of its two eigenvalues and the non-semisimple family outright. For the central family this is TauCeti.isConj_scalar_iff, which needs nothing about GL₂ and lives with the other scalar invariants in TauCeti/LinearAlgebra/Matrix/GeneralLinearGroup/ConjugacyClasses.lean.

References

• C. Bonnafé, Representations of SL₂(𝔽_q) (2011), Chapter 1.
• J.-P. Serre, Linear Representations of Finite Groups, GTM 42 (1977), §5.2.

Shape adapters for the two split normal forms

The normal forms below are written against the pair ![a, b] and the Jordan parameter 1, while TauCeti/LinearAlgebra/Matrix/GeneralLinearGroup/Diagonal/Basic.lean and TauCeti/LinearAlgebra/Matrix/GeneralLinearGroup/ScalarUnipotent.lean state non-scalarity, the trace and the determinant for a general family and a general off-diagonal entry. These six private lemmas do that adaptation once, so that no proof below recomputes the trace, the determinant or the non-scalarity of a normal form from its matrix entries.

The two split normal forms

theorem TauCeti.isConj_diagGL_of_trace_of_det {F : Type u_1} [Field F] {g : GL (Fin 2) F} {a b : Fˣ} (hab : a ≠ b) (htrace : (↑g).trace = ↑a + ↑b) (hdet : (↑g).det = ↑a * ↑b) : IsConj g (diagGL ![a, b])

The split semisimple normal form. An element of GL₂(F) whose characteristic polynomial has the two distinct roots a and b is conjugate to diagGL ![a, b]. Distinct roots already force the element to be non-scalar.

theorem TauCeti.isConj_jordanGL_one_of_trace_of_det {F : Type u_1} [Field F] {g : GL (Fin 2) F} (hg : ↑g ∉ Set.range ⇑(Matrix.scalar (Fin 2))) {a : Fˣ} (htrace : (↑g).trace = 2 * ↑a) (hdet : (↑g).det = ↑a * ↑a) : IsConj g (jordanGL a 1)

The non-semisimple normal form. A non-scalar element of GL₂(F) whose characteristic polynomial is (X - a)² is conjugate to the Jordan block jordanGL a 1.

The elliptic normal form

theorem TauCeti.isConj_gl2NonSplitTorusHom_of_trace_of_det {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] [Algebra.IsQuadraticExtension F E] {g : GL (Fin 2) F} {x : Eˣ} (hx : ↑x ∉ Set.range ⇑(algebraMap F E)) {t d : F} (hx2 : ↑x * ↑x = (algebraMap F E) t * ↑x - (algebraMap F E) d) (htrace : (↑g).trace = t) (hdet : (↑g).det = d) : IsConj g ((GL2NonSplitTorusHom F E) x)

The elliptic normal form. An element of GL₂(F) whose characteristic polynomial X² - t X + d is satisfied by an element x of a degree-2 extension E/F lying outside F is conjugate to the element x of the non-split torus. A root outside F already forces the element to be non-scalar.

The classification

theorem TauCeti.exists_isConj_normalForm {F : Type u_1} [Field F] [Finite F] (E : Type u_2) [Field E] [Algebra F E] [Algebra.IsQuadraticExtension F E] (g : GL (Fin 2) F) : (∃ (a : Fˣ), (Matrix.GeneralLinearGroup.scalar (Fin 2)) a = g) ∨ (∃ (a : Fˣ) (b : Fˣ), a ≠ b ∧ IsConj g (diagGL ![a, b])) ∨ (∃ (a : Fˣ), IsConj g (jordanGL a 1)) ∨ ∃ (x : Eˣ), ↑x ∉ Set.range ⇑(algebraMap F E) ∧ IsConj g ((GL2NonSplitTorusHom F E) x)

Every element of GL₂(F) is conjugate to one of the four normal forms, for F a finite field with a supplied degree-2 extension E: a central scalar, a split semisimple diagGL ![a, b] with a ≠ b, a non-semisimple Jordan block jordanGL a 1, or an elliptic element GL2NonSplitTorusHom F E x with x outside F.

This is what turns a computation of a character at these four normal forms into a full row of the character table of GL₂(𝔽_q).

Uniqueness of the normal form

The four families are pairwise non-conjugate, and inside each family the parameters are determined up to the evident symmetry. Only the order shown is proved; the reverse order follows from IsConj.symm.

theorem TauCeti.not_isConj_scalar_diagGL {F : Type u_1} [Field F] (a : Fˣ) {b c : Fˣ} (hbc : b ≠ c) : ¬IsConj ((Matrix.GeneralLinearGroup.scalar (Fin 2)) a) (diagGL ![b, c])

A scalar is not conjugate to a split semisimple normal form. The hypothesis b ≠ c is needed: diagGL ![b, b] is the scalar b.

theorem TauCeti.not_isConj_scalar_jordanGL_one {F : Type u_1} [Field F] (a b : Fˣ) : ¬IsConj ((Matrix.GeneralLinearGroup.scalar (Fin 2)) a) (jordanGL b 1)

A scalar is not conjugate to a Jordan block. The two have the same characteristic polynomial (X - a)² when their eigenvalues agree, so this is exactly where trace and determinant fail to separate the conjugacy classes of GL₂(F).

theorem TauCeti.not_isConj_diagGL_jordanGL_one {F : Type u_1} [Field F] (a b c : Fˣ) : ¬IsConj (diagGL ![a, b]) (jordanGL c 1)

A split semisimple normal form is not conjugate to a Jordan block. For distinct a and b equal traces and determinants would force (a - b)² = 0; for a = b the left-hand side is a scalar, which is not conjugate to a Jordan block either.

theorem TauCeti.isConj_diagGL_iff {F : Type u_1} [Field F] (a b c d : Fˣ) : IsConj (diagGL ![a, b]) (diagGL ![c, d]) ↔ a = c ∧ b = d ∨ a = d ∧ b = c

Two split semisimple normal forms are conjugate exactly when their eigenvalue pairs agree up to order. The transposition (a, b) ↦ (b, a) is the Weyl group of the split torus acting on the torus by permuting the diagonal entries, and it is the only identification among these normal forms. No distinctness is asked of either pair: when a pair repeats, its normal form is the corresponding scalar, and the statement specializes to TauCeti.isConj_scalar_iff.

theorem TauCeti.isConj_jordanGL_one_iff {F : Type u_1} [Field F] (a b : Fˣ) : IsConj (jordanGL a 1) (jordanGL b 1) ↔ a = b

Two Jordan blocks are conjugate exactly when their eigenvalues agree: the non-semisimple family carries no symmetry at all.

theorem TauCeti.not_isConj_scalar_gl2NonSplitTorusHom {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] [Algebra.IsQuadraticExtension F E] (a : Fˣ) {x : Eˣ} (hx : ↑x ∉ Set.range ⇑(algebraMap F E)) : ¬IsConj ((Matrix.GeneralLinearGroup.scalar (Fin 2)) a) ((GL2NonSplitTorusHom F E) x)

A scalar is not conjugate to an elliptic normal form.

theorem TauCeti.not_isConj_diagGL_gl2NonSplitTorusHom {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] [Algebra.IsQuadraticExtension F E] (a b : Fˣ) {x : Eˣ} (hx : ↑x ∉ Set.range ⇑(algebraMap F E)) : ¬IsConj (diagGL ![a, b]) ((GL2NonSplitTorusHom F E) x)

A split semisimple normal form is not conjugate to an elliptic one. Equal traces and determinants make x a root of (X - a) (X - b), so x would be a or b, and both lie in F.

theorem TauCeti.not_isConj_jordanGL_one_gl2NonSplitTorusHom {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] [Algebra.IsQuadraticExtension F E] (a : Fˣ) (x : Eˣ) : ¬IsConj (jordanGL a 1) ((GL2NonSplitTorusHom F E) x)

A Jordan block is not conjugate to an elliptic normal form. Equal traces and determinants make x a double root of (X - a)², so x would be a, which lies in F. No hypothesis is needed on x: a torus parameter inside F gives the corresponding scalar, which is not conjugate to a Jordan block either.