Linear characters and Steinberg twists of GL₂(𝔽_q)

Every multiplicative character α : Fˣ →* ℂˣ gives a one-dimensional representation of GL₂(F) by precomposition with the determinant. This file packages that representation as TauCeti.GL2Linear F α, proves that distinct α give distinct character rows, and computes its character on the four families of conjugacy classes.

Tensoring with TauCeti.GL2Steinberg F gives the corresponding Steinberg twist TauCeti.GL2SteinbergTwist F α. Its character is the pointwise product of the determinant character and the untwisted Steinberg character, so the four values are

q α(a²), α(ab), 0, and -α(N_{E/F}(x))

on scalar, split semisimple, non-semisimple, and elliptic representatives. These are the two boundary rows of the principal series Ind_B^{GL₂}(α ⊗ α); their representation-level splitting is TauCeti.nonempty_iso_GL2PrincipalSeries_self in TauCeti/RepresentationTheory/CharacterTable/GL2/Boundary.lean.

Main definitions

• TauCeti.GL2LinearChar: the character α ∘ det as a homomorphism to ℂˣ.
• TauCeti.GL2LinearRep: the corresponding representation on the line ℂ.
• TauCeti.GL2Linear: its one-dimensional representation.
• TauCeti.GL2SteinbergTwist: the determinant-character twist of the Steinberg representation.

Main results

• TauCeti.character_GL2Linear and TauCeti.character_GL2SteinbergTwist: the character formulas at an arbitrary group element.
• TauCeti.GL2LinearChar_comp_gl2BorelSubtype: restriction to the Borel subgroup is the boundary character α ⊗ α.
• TauCeti.GL2Linear_character_injective: distinct multiplicative characters give distinct rows.
• TauCeti.character_GL2Linear_mem_irreducibleCharacters: the linear characters are irreducible characters of GL₂(F).
• The _scalar, _diagGL, _jordanGL, and _gl2NonSplitTorusHom theorems compute both families on the four class representatives.

References

• Character theory roadmap, Layer 9, "The boundary: linear and Steinberg constituents" and "Character-value formulas".
• W. Fulton and J. Harris, Representation Theory: A First Course (1991), §5.2.
• C. Bonnafé, Representations of SL₂(𝔽_q) (2011), Chapter 5.

The linear representations

def TauCeti.GL2LinearChar {F : Type u} [CommRing F] (α : Fˣ →* ℂˣ) : GL (Fin 2) F →* ℂˣ

The determinant character attached to α. This is the multiplicative character of GL₂(F) sending g to α(det g).

Equations

• TauCeti.GL2LinearChar α = α.comp Matrix.GeneralLinearGroup.det

@[simp]

theorem TauCeti.GL2LinearChar_apply {F : Type u} [CommRing F] (α : Fˣ →* ℂˣ) (g : GL (Fin 2) F) : (GL2LinearChar α) g = α (Matrix.GeneralLinearGroup.det g)

def TauCeti.GL2LinearRep {F : Type u} [CommRing F] (α : Fˣ →* ℂˣ) : Representation ℂ (GL (Fin 2) F) ℂ

The one-dimensional representation α ∘ det of GL₂(F).

Equations

• TauCeti.GL2LinearRep α = Representation.ofLinearCharacter (TauCeti.GL2LinearChar α)

theorem TauCeti.GL2LinearRep_def {F : Type u} [CommRing F] (α : Fˣ →* ℂˣ) : GL2LinearRep α = Representation.ofLinearCharacter (GL2LinearChar α)

TauCeti.GL2LinearRep is the generic one-dimensional representation associated to TauCeti.GL2LinearChar.

noncomputable def TauCeti.GL2Linear (F : Type u) [CommRing F] (α : Fˣ →* ℂˣ) : FDRep ℂ (GL (Fin 2) F)

The one-dimensional representation α ∘ det of GL₂(F), bundled in FDRep.

Equations

• TauCeti.GL2Linear F α = FDRep.of (TauCeti.GL2LinearRep α)

theorem TauCeti.GL2Linear_def {F : Type u} [CommRing F] (α : Fˣ →* ℂˣ) : GL2Linear F α = FDRep.of (GL2LinearRep α)

TauCeti.GL2Linear is the one-dimensional representation associated to TauCeti.GL2LinearChar.

@[simp]

theorem TauCeti.finrank_GL2Linear {F : Type u} [CommRing F] (α : Fˣ →* ℂˣ) : Module.finrank ℂ ↑(GL2Linear F α).V = 1

The linear representation has dimension one.

@[simp]

theorem TauCeti.character_GL2Linear {F : Type u} [CommRing F] (α : Fˣ →* ℂˣ) (g : GL (Fin 2) F) : (GL2Linear F α).character g = ↑(α (Matrix.GeneralLinearGroup.det g))

The character of TauCeti.GL2Linear F α is α ∘ det.

theorem TauCeti.GL2LinearChar_injective {F : Type u} [CommRing F] : Function.Injective GL2LinearChar

Determinant characters of GL₂ remember their parameter. Surjectivity of the determinant shows that precomposition with it is injective.

theorem TauCeti.GL2Linear_character_injective {F : Type u} [CommRing F] : Function.Injective fun (α : Fˣ →* ℂˣ) => (GL2Linear F α).character

Distinct parameters give distinct linear character rows of GL₂.

@[simp]

theorem TauCeti.character_GL2Linear_mem_irreducibleCharacters {F : Type u} [CommRing F] (α : Fˣ →* ℂˣ) : (GL2Linear F α).character ∈ irreducibleCharacters ℂ (GL (Fin 2) F)

The linear characters α ∘ det are irreducible characters of GL₂(F), being the characters of one-dimensional representations.

@[simp]

theorem TauCeti.GL2LinearChar_comp_gl2BorelSubtype {F : Type u} [CommRing F] (α : Fˣ →* ℂˣ) : (GL2LinearChar α).comp (GL2Borel F).subtype = GL2Borel.linearChar α α

The determinant character restricts to the boundary Borel character α ⊗ α.

@[simp]

theorem TauCeti.GL2LinearRep_comp_gl2BorelSubtype {F : Type u} [CommRing F] (α : Fˣ →* ℂˣ) : MonoidHom.comp (GL2LinearRep α) (GL2Borel F).subtype = GL2Borel.linearRep α α

The linear representation restricts to the one-dimensional Borel representation at the boundary pair (α, α).

The linear character row

theorem TauCeti.character_GL2Linear_scalar {F : Type u} [CommRing F] (α : Fˣ →* ℂˣ) (a : Fˣ) : (GL2Linear F α).character ((Matrix.GeneralLinearGroup.scalar (Fin 2)) a) = ↑(α (a ^ 2))

The linear character at a scalar matrix is α(a²).

theorem TauCeti.character_GL2Linear_diagGL {F : Type u} [CommRing F] (α : Fˣ →* ℂˣ) (a b : Fˣ) : (GL2Linear F α).character (diagGL ![a, b]) = ↑(α (a * b))

The linear character at a split semisimple representative is α(ab). The formula does not need the usual a ≠ b hypothesis because it is an identity for every diagonal matrix.

theorem TauCeti.character_GL2Linear_jordanGL {F : Type u} [CommRing F] (α : Fˣ →* ℂˣ) (a : Fˣ) (b : F) : (GL2Linear F α).character (jordanGL a b) = ↑(α (a ^ 2))

The linear character at a Jordan-form matrix jordanGL a b is α(a²). The value does not depend on the upper-right entry b, so no hypothesis on it is needed; the matrix represents the non-semisimple family exactly when b ≠ 0.

theorem TauCeti.character_GL2Linear_gl2NonSplitTorusHom {F : Type u} [Field F] {E : Type u_1} [Field E] [Algebra F E] [Algebra.IsQuadraticExtension F E] (α : Fˣ →* ℂˣ) (x : Eˣ) : (GL2Linear F α).character ((GL2NonSplitTorusHom F E) x) = ↑(α ((Algebra.normUnits F) x))

The linear character at a non-split-torus element is the character applied to its field norm.

The Steinberg twists

noncomputable def TauCeti.GL2SteinbergTwist (F : Type u) [Field F] [Fintype F] (α : Fˣ →* ℂˣ) : FDRep ℂ (GL (Fin 2) F)

The Steinberg representation twisted by α ∘ det. These are the degree-q boundary constituents of the principal series. Their dimension and character values are proved below; TauCeti.nonempty_iso_GL2PrincipalSeries_self identifies them as constituents.

Equations

• TauCeti.GL2SteinbergTwist F α = CategoryTheory.MonoidalCategoryStruct.tensorObj (TauCeti.GL2Linear F α) (TauCeti.GL2Steinberg F)

theorem TauCeti.GL2SteinbergTwist_def {F : Type u} [Field F] [Fintype F] (α : Fˣ →* ℂˣ) : GL2SteinbergTwist F α = CategoryTheory.MonoidalCategoryStruct.tensorObj (GL2Linear F α) (GL2Steinberg F)

A Steinberg twist is the tensor product of the determinant character with the untwisted Steinberg representation.

@[simp]

theorem TauCeti.finrank_GL2SteinbergTwist {F : Type u} [Field F] [Fintype F] (α : Fˣ →* ℂˣ) : Module.finrank ℂ ↑(GL2SteinbergTwist F α).V = Fintype.card F

The Steinberg twist has dimension q, being the tensor product of a line with the Steinberg representation.

@[simp]

theorem TauCeti.character_GL2SteinbergTwist {F : Type u} [Field F] [Fintype F] (α : Fˣ →* ℂˣ) (g : GL (Fin 2) F) : (GL2SteinbergTwist F α).character g = ↑(α (Matrix.GeneralLinearGroup.det g)) * (GL2Steinberg F).character g

The character of a Steinberg twist is the determinant character times the Steinberg character.

theorem TauCeti.character_GL2SteinbergTwist_scalar {F : Type u} [Field F] [Fintype F] (α : Fˣ →* ℂˣ) (a : Fˣ) : (GL2SteinbergTwist F α).character ((Matrix.GeneralLinearGroup.scalar (Fin 2)) a) = ↑(Fintype.card F) * ↑(α (a ^ 2))

The Steinberg twist at a scalar matrix is q α(a²).

theorem TauCeti.character_GL2SteinbergTwist_diagGL {F : Type u} [Field F] [Fintype F] (α : Fˣ →* ℂˣ) {a b : Fˣ} (hab : a ≠ b) : (GL2SteinbergTwist F α).character (diagGL ![a, b]) = ↑(α (a * b))

The Steinberg twist at a split semisimple representative is α(ab).

theorem TauCeti.GL2SteinbergTwist_character_injective {F : Type u} [Field F] [Fintype F] : Function.Injective fun (α : Fˣ →* ℂˣ) => (GL2SteinbergTwist F α).character

Distinct parameters give distinct Steinberg-twist character rows. At diag(a, 1) the Steinberg character is 1 whenever a ≠ 1, so the row recovers α(a); every character has value 1 at the remaining element.

theorem TauCeti.character_GL2SteinbergTwist_jordanGL {F : Type u} [Field F] [Fintype F] (α : Fˣ →* ℂˣ) (a : Fˣ) {b : F} (hb : b ≠ 0) : (GL2SteinbergTwist F α).character (jordanGL a b) = 0

The Steinberg twist vanishes at a non-semisimple representative.

theorem TauCeti.character_GL2SteinbergTwist_gl2NonSplitTorusHom {F : Type u} [Field F] [Fintype F] {E : Type u_1} [Field E] [Algebra F E] [Algebra.IsQuadraticExtension F E] (α : Fˣ →* ℂˣ) {x : Eˣ} (hx : ↑x ∉ Set.range ⇑(algebraMap F E)) : (GL2SteinbergTwist F α).character ((GL2NonSplitTorusHom F E) x) = -↑(α ((Algebra.normUnits F) x))

The Steinberg twist at an elliptic element is the negative of α at its field norm.