The conjugacy classes of GL₂ over a field

Rational canonical form in size two, proved in TauCeti.LinearAlgebra.Matrix.RationalCanonicalFormFinTwo, says that a non-scalar 2 × 2 matrix M over a field is similar to the companion matrix !![0, -det M; 1, trace M] of its characteristic polynomial X² - (trace M) X + det M. Read inside the group, it classifies the conjugacy classes of GL₂(F) completely: a scalar element is alone in its class, and two non-scalar elements are conjugate exactly when their traces and their determinants agree.

Counting the classes over a finite field is then a matter of counting the invariants. The scalar classes are indexed by the units a, giving q - 1 of them; the non-scalar classes are indexed by the pairs (trace, det) with the determinant a unit and the trace unconstrained, giving q (q - 1) of them. Altogether q² - 1, which is the number of irreducible complex representations of GL₂(𝔽_q).

The representative chosen here is uniform but anonymous. Over a finite field with a supplied degree-2 extension it can be replaced by the four named normal forms — a scalar, a diagonal matrix with distinct entries, a Jordan block, and an element of the non-split torus — in TauCeti/LinearAlgebra/Matrix/GeneralLinearGroup/NormalForm.lean.

Being scalar is spelled M ∈ Set.range (Matrix.scalar (Fin 2)), as in TauCeti.LinearAlgebra.Matrix.Commute, whose commutant computation is the companion result, describing the centralizer of a non-scalar matrix rather than its conjugacy class.

Main definitions

• TauCeti.companionGL: the companion matrix of X² - t X + d as an element of GL₂, for an invertible constant term.
• TauCeti.conjRepGLFinTwo: the chosen representative of each conjugacy class of GL₂(F), indexed by Fˣ ⊕ F × Fˣ.
• TauCeti.conjClassesGLFinTwoEquiv: the resulting indexing of ConjClasses (GL (Fin 2) F).

Main results

• TauCeti.isConj_companionGL: rational canonical form inside GL₂(F), a non-scalar element is conjugate to the companion element of its characteristic polynomial.
• TauCeti.eq_of_mem_range_scalar_of_isConj: a scalar element of GL n R is alone in its class, TauCeti.not_isConj_of_mem_range_scalar: it is therefore not conjugate to a non-scalar one, and TauCeti.isConj_scalar_iff: two scalar elements are conjugate only when they are equal.
• TauCeti.isConj_iff_of_notMem_range_scalar: the classification, two non-scalar elements of GL₂(F) are conjugate exactly when they have the same trace and the same determinant.
• TauCeti.GL2NonSplitTorus.isConj_gl2NonSplitTorusHom_iff: the elements of the non-split torus conjugate to an elliptic element u are exactly u and its Frobenius conjugate u^q.
• TauCeti.card_conjClasses_GL2: GL₂(𝔽_q) has q² - 1 conjugacy classes.

References

• Character theory roadmap, Layer 9, "The conjugacy classes (a build target)": class representatives and the count q² - 1 = Nat.card (ConjClasses (GL (Fin 2) F)), matching the number of irreducibles. The final theorem carries the name card_conjClasses_GL2 the roadmap gives it there.
• C. Bonnafé, Representations of SL₂(𝔽_q) (2011), Chapter 1.
• J.-P. Serre, Linear Representations of Finite Groups, GTM 42 (1977), §5.2.

Conjugacy invariants

theorem TauCeti.trace_val_eq_of_isConj {n : Type u_1} [DecidableEq n] [Fintype n] {R : Type u_2} [CommSemiring R] {g h : GL n R} (hgh : IsConj g h) : (↑g).trace = (↑h).trace

Conjugate elements of GL n R have the same trace.

theorem TauCeti.eq_of_mem_range_scalar_of_isConj {n : Type u_1} [DecidableEq n] [Fintype n] {R : Type u_2} [CommSemiring R] {g h : GL n R} (hg : ↑g ∈ Set.range ⇑(Matrix.scalar n)) (hgh : IsConj g h) : g = h

A scalar element of GL n R is alone in its conjugacy class: scalar matrices are central.

theorem TauCeti.not_isConj_of_mem_range_scalar {n : Type u_1} [DecidableEq n] [Fintype n] {R : Type u_2} [CommSemiring R] {g h : GL n R} (hg : ↑g ∈ Set.range ⇑(Matrix.scalar n)) (hh : ↑h ∉ Set.range ⇑(Matrix.scalar n)) : ¬IsConj g h

A scalar element and a non-scalar element of GL n R are never conjugate. The class of a scalar element is a single point, so it cannot contain a non-scalar one; being scalar is therefore a conjugacy invariant in its own right, and the one that trace and determinant miss: it separates a scalar matrix from a Jordan block with the same characteristic polynomial.

theorem TauCeti.isConj_scalar_iff {n : Type u_1} [DecidableEq n] [Fintype n] {R : Type u_2} [CommSemiring R] [Nonempty n] (a b : Rˣ) : IsConj ((Matrix.GeneralLinearGroup.scalar n) a) ((Matrix.GeneralLinearGroup.scalar n) b) ↔ a = b

Two scalar elements of GL n R are conjugate exactly when they are equal. A scalar element is alone in its class, and the scalar embedding is injective (Matrix.scalar_inj).

The classification in GL₂

def TauCeti.companionGL {F : Type u_1} [Field F] (t : F) (d : Fˣ) : GL (Fin 2) F

The companion matrix of X² - t X + d as an element of GL₂, for an invertible constant term d. Every non-scalar element of GL₂(F) is conjugate to exactly one of these, by TauCeti.isConj_companionGL and TauCeti.isConj_iff_of_notMem_range_scalar.

Equations

• TauCeti.companionGL t d = Matrix.GeneralLinearGroup.mkOfDetNeZero (TauCeti.companionFinTwo t ↑d) ⋯

@[simp]

theorem TauCeti.coe_companionGL {F : Type u_1} [Field F] (t : F) (d : Fˣ) : ↑(companionGL t d) = companionFinTwo t ↑d

@[simp]

theorem TauCeti.det_companionGL {F : Type u_1} [Field F] (t : F) (d : Fˣ) : Matrix.GeneralLinearGroup.det (companionGL t d) = d

The determinant of a companion element of GL₂ is its constant term, as a unit. The matrix-level statement is TauCeti.det_companionFinTwo, reached from here by Matrix.GeneralLinearGroup.val_det_apply.

theorem TauCeti.companionGL_notMem_range_scalar {F : Type u_1} [Field F] (t : F) (d : Fˣ) : ↑(companionGL t d) ∉ Set.range ⇑(Matrix.scalar (Fin 2))

A companion element of GL₂ is not scalar.

theorem TauCeti.scalar_ne_companionGL {F : Type u_1} [Field F] (t : F) (d a : Fˣ) : (Matrix.GeneralLinearGroup.scalar (Fin 2)) a ≠ companionGL t d

A scalar element of GL₂ is never a companion element.

theorem TauCeti.isConj_companionGL {F : Type u_1} [Field F] {g : GL (Fin 2) F} (hg : ↑g ∉ Set.range ⇑(Matrix.scalar (Fin 2))) : IsConj g (companionGL (↑g).trace (Matrix.GeneralLinearGroup.det g))

Rational canonical form inside GL₂(F): a non-scalar element is conjugate to the companion element of its characteristic polynomial.

theorem TauCeti.isConj_iff_of_notMem_range_scalar {F : Type u_1} [Field F] {g h : GL (Fin 2) F} (hg : ↑g ∉ Set.range ⇑(Matrix.scalar (Fin 2))) (hh : ↑h ∉ Set.range ⇑(Matrix.scalar (Fin 2))) : IsConj g h ↔ (↑g).trace = (↑h).trace ∧ (↑g).det = (↑h).det

The conjugacy classification of the non-scalar elements of GL₂(F): two of them are conjugate exactly when they have the same trace and the same determinant, that is, exactly when they have the same characteristic polynomial.

The hypotheses are necessary: a scalar matrix has the same characteristic polynomial as the corresponding Jordan block, and the two are not conjugate.

theorem TauCeti.GL2NonSplitTorus.isConj_gl2NonSplitTorusHom_iff {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] [Finite F] [Algebra.IsQuadraticExtension F E] {u v : Eˣ} (hu : ↑u ∉ Set.range ⇑(algebraMap F E)) : IsConj ((GL2NonSplitTorusHom F E) u) ((GL2NonSplitTorusHom F E) v) ↔ v = u ∨ v = u ^ Nat.card F

The elements of the elliptic torus conjugate to a given elliptic element. For u : Eˣ outside F, the matrix of v : Eˣ is conjugate to that of u exactly when v is u or its Frobenius conjugate u^q.

Conjugate matrices have the same trace and determinant, which on the torus are the trace and the norm of the field element; and u, u^q are the two roots of X² - Tr(u) X + N(u), so an element with those invariants is one of them.

Counting the classes

def TauCeti.conjRepGLFinTwo {F : Type u_1} [Field F] : Fˣ ⊕ F × Fˣ → GL (Fin 2) F

The chosen representatives of the conjugacy classes of GL₂(F): the scalar matrix a • 1 for a unit a, and the companion matrix of X² - t X + d for a scalar t and a unit d. The first family is the centre and the second exhausts the non-scalar classes.

Equations

• TauCeti.conjRepGLFinTwo (Sum.inl a) = (Matrix.GeneralLinearGroup.scalar (Fin 2)) a
• TauCeti.conjRepGLFinTwo (Sum.inr td) = TauCeti.companionGL td.1 td.2

@[simp]

theorem TauCeti.conjRepGLFinTwo_inl {F : Type u_1} [Field F] (a : Fˣ) : conjRepGLFinTwo (Sum.inl a) = (Matrix.GeneralLinearGroup.scalar (Fin 2)) a

@[simp]

theorem TauCeti.conjRepGLFinTwo_inr {F : Type u_1} [Field F] (t : F) (d : Fˣ) : conjRepGLFinTwo (Sum.inr (t, d)) = companionGL t d

theorem TauCeti.bijective_mk_conjRepGLFinTwo {F : Type u_1} [Field F] : Function.Bijective fun (x : Fˣ ⊕ F × Fˣ) => ConjClasses.mk (conjRepGLFinTwo x)

The representatives meet every conjugacy class of GL₂(F) exactly once. Surjectivity is rational canonical form, injectivity the classification: a scalar is alone in its class, a companion element is never scalar, and two companion elements with the same trace and determinant are equal.

noncomputable def TauCeti.conjClassesGLFinTwoEquiv {F : Type u_1} [Field F] : Fˣ ⊕ F × Fˣ ≃ ConjClasses (GL (Fin 2) F)

The conjugacy classes of GL₂(F) are indexed by Fˣ ⊕ F × Fˣ: a unit a indexes the class of the scalar a • 1, and a pair (t, d) the class of the elements with trace t and determinant d that are not scalar.

Equations

• TauCeti.conjClassesGLFinTwoEquiv = Equiv.ofBijective (fun (x : Fˣ ⊕ F × Fˣ) => ConjClasses.mk (TauCeti.conjRepGLFinTwo x)) ⋯

@[simp]

theorem TauCeti.conjClassesGLFinTwoEquiv_apply {F : Type u_1} [Field F] (x : Fˣ ⊕ F × Fˣ) : conjClassesGLFinTwoEquiv x = ConjClasses.mk (conjRepGLFinTwo x)

theorem TauCeti.card_conjClasses_GL2 (F : Type u_1) [Field F] [Finite F] : Nat.card (ConjClasses (GL (Fin 2) F)) = Nat.card F ^ 2 - 1

GL₂(𝔽_q) has q² - 1 conjugacy classes: q - 1 central ones and q (q - 1) non-scalar ones, indexed by their trace and their determinant. This is the number of irreducible complex representations of GL₂(𝔽_q), whose four families have dimensions 1, q, q + 1 and q - 1.

The name is the roadmap's; the statement is the roadmap's with [Fintype F] weakened to [Finite F], nothing in the argument deciding equality.