The Steinberg character of GL₂(𝔽_q) on the four families of conjugacy classes

TauCeti.character_GL2Steinberg computes the Steinberg character of GL₂(𝔽_q) at g as the number of points of the projective line fixed by g, less one. The conjugacy classes of GL₂(𝔽_q) fall into four families, and TauCeti/LinearAlgebra/Matrix/GeneralLinearGroup/ProjectiveLine.lean counts the fixed points of a representative of each: q + 1 for a central scalar matrix, 2 for a split semisimple diagonal matrix with distinct entries, 1 for a non-semisimple Jordan block, and 0 for an elliptic element of the non-split torus that does not come from F. This file reads off the resulting row of the character table,

χ_St = q, 1, 0, -1

on the four families, together with the row of the boundary principal series Ind_B^{GL₂}(1 ⊗ 1) = 1 + χ_St, which is q + 1, 2, 1, 0 — the fixed-point counts themselves, as they must be for a permutation character.

That these four values determine the Steinberg character outright is a statement about the conjugacy classes, not about the representation: every element of GL₂(𝔽_q) is conjugate to one of the four representatives (TauCeti/LinearAlgebra/Matrix/GeneralLinearGroup/ConjugacyClasses.lean classifies the classes by trace and determinant, and the elliptic normal form is the one that needs the quadratic extension), and a character is a class function. That exhaustion is TauCeti.exists_isConj_normalForm of TauCeti/LinearAlgebra/Matrix/GeneralLinearGroup/NormalForm.lean; it is not invoked here, the values below being stated at the normal forms themselves.

Main results

• TauCeti.character_GL2Steinberg_scalar, TauCeti.character_GL2Steinberg_diagGL, TauCeti.character_GL2Steinberg_jordanGL and TauCeti.character_GL2Steinberg_gl2NonSplitTorusHom: the Steinberg character takes the values q, 1, 0 and -1 on the four families.
• TauCeti.character_GL2PrincipalSeries_one_one_scalar and its three companions: the character of the boundary principal series takes the values q + 1, 2, 1 and 0.

None of those eight values is a simp lemma. TauCeti.character_GL2Steinberg is itself @[simp], so simp rewrites the left-hand side of each of them to a fixed-coset count, and then, F being finite, on to a Fintype.card by Nat.card_eq_fintype_card; so none of the eight is in simp-normal form, and tagging any of them fails the simpNF linter.

References

This supplies the Steinberg row of the character-value formulas of Layer 9 ("the representation theory of GL₂(𝔽_q)") of TauCetiRoadmap/RepresentationTheory/CharacterTheory/README.md. See also W. Fulton and J. Harris, Representation Theory: A First Course, GTM 129, §5.2, and C. Bonnafé, Representations of SL₂(𝔽_q) (2011), Chapter 5.

The Steinberg character

theorem TauCeti.character_GL2Steinberg_scalar {F : Type u} [Field F] [Fintype F] (u : Fˣ) : (GL2Steinberg F).character ((Matrix.GeneralLinearGroup.scalar (Fin 2)) u) = ↑(Fintype.card F)

The Steinberg character at a central element is q. A scalar matrix fixes every point of the projective line, so the permutation character is q + 1 and the invariant line accounts for one of it.

theorem TauCeti.character_GL2Steinberg_diagGL {F : Type u} [Field F] [Fintype F] {a b : Fˣ} (hab : a ≠ b) : (GL2Steinberg F).character (diagGL ![a, b]) = 1

The Steinberg character at a split semisimple element is 1. A diagonal matrix with distinct entries fixes exactly the two coordinate axes.

theorem TauCeti.character_GL2Steinberg_jordanGL {F : Type u} [Field F] [Fintype F] (a : Fˣ) {b : F} (hb : b ≠ 0) : (GL2Steinberg F).character (jordanGL a b) = 0

The Steinberg character at a non-semisimple element is 0. A Jordan block fixes exactly the line of its single eigenvector, so the permutation character is 1 and the invariant line is all of it.

theorem TauCeti.character_GL2Steinberg_gl2NonSplitTorusHom {F : Type u} [Field F] [Fintype F] {E : Type u_1} [Field E] [Algebra F E] [Algebra.IsQuadraticExtension F E] {x : Eˣ} (hx : ↑x ∉ Set.range ⇑(algebraMap F E)) : (GL2Steinberg F).character ((GL2NonSplitTorusHom F E) x) = -1

The Steinberg character at an elliptic element is -1. An element of the non-split torus coming from E ∖ F has no eigenline over F, so it fixes no point of the projective line at all and only the invariant line contributes.

The boundary principal series

At α = β = 1 the principal series is the permutation representation of the projective line, so its character is the fixed-point count itself: one more than the Steinberg value. These four values are the general principal-series row (TauCeti/RepresentationTheory/CharacterTable/GL2/PrincipalSeries/CharacterValues.lean) at the trivial pair of characters, and are read off it rather than proved a second time.

theorem TauCeti.character_GL2PrincipalSeries_one_one_scalar {F : Type u} [Field F] [Fintype F] (u : Fˣ) : (GL2PrincipalSeries F 1 1).character ((Matrix.GeneralLinearGroup.scalar (Fin 2)) u) = ↑(Fintype.card F) + 1

The boundary principal series has character q + 1 at a central element.

theorem TauCeti.character_GL2PrincipalSeries_one_one_diagGL {F : Type u} [Field F] [Fintype F] {a b : Fˣ} (hab : a ≠ b) : (GL2PrincipalSeries F 1 1).character (diagGL ![a, b]) = 2

The boundary principal series has character 2 at a split semisimple element.

theorem TauCeti.character_GL2PrincipalSeries_one_one_jordanGL {F : Type u} [Field F] [Fintype F] (a : Fˣ) {b : F} (hb : b ≠ 0) : (GL2PrincipalSeries F 1 1).character (jordanGL a b) = 1

The boundary principal series has character 1 at a non-semisimple element.

theorem TauCeti.character_GL2PrincipalSeries_one_one_gl2NonSplitTorusHom {F : Type u} [Field F] [Fintype F] {E : Type u_1} [Field E] [Algebra F E] [Algebra.IsQuadraticExtension F E] {x : Eˣ} (hx : ↑x ∉ Set.range ⇑(algebraMap F E)) : (GL2PrincipalSeries F 1 1).character ((GL2NonSplitTorusHom F E) x) = 0

The boundary principal series has character 0 at an elliptic element: no point of the projective line is fixed, so the permutation character vanishes.