The boundary principal series of GL₂ splits

For a finite field F and a multiplicative character α : Fˣ → ℂˣ, the principal series at the repeated parameter (α, α) is reducible. This file identifies its two constituents:

Ind_B^GL₂(α ⊗ α) ≅ (α ∘ det) ⊕ ((α ∘ det) ⊗ St).

The character identity is the projection formula for induction. The Borel character α ⊗ α is the restriction of the determinant character α ∘ det, so its induction is the product of that character with Ind_B^GL₂(1). The latter is the permutation representation on the projective line and has character 1 + χ_St. Distributing the determinant character gives the characters of TauCeti.GL2Linear F α and TauCeti.GL2SteinbergTwist F α. Character theory over ℂ then promotes this identity to an isomorphism of representations.

This splitting separates the two boundary families in the character table of GL₂(F): the linear representations have dimension 1, while their Steinberg twists have dimension Fintype.card F.

Main results

• TauCeti.character_GL2PrincipalSeries_self_eq_add: its two character constituents are the linear and Steinberg-twist characters.
• TauCeti.simple_GL2Steinberg and TauCeti.simple_GL2SteinbergTwist: the Steinberg representation and all its determinant twists are irreducible (for universe-small finite fields); TauCeti.character_GL2SteinbergTwist_mem_irreducibleCharacters records that the Steinberg twists are irreducible characters of GL₂(F).
• TauCeti.nonempty_iso_GL2PrincipalSeries_self: the boundary principal series is the biproduct of those two representations.

References

• W. Fulton and J. Harris, Representation Theory: A First Course, GTM 129, §5.2.
• J.-P. Serre, Linear Representations of Finite Groups, GTM 42, Chapter 7 — cited only for the projection formula for induced characters, not for the GL₂ decomposition itself, which is Fulton–Harris above.

@[simp]

theorem TauCeti.character_GL2PrincipalSeries_self_eq_add (F : Type u) [Field F] [Fintype F] (α : Fˣ →* ℂˣ) : (GL2PrincipalSeries F α α).character = (GL2Linear F α).character + (GL2SteinbergTwist F α).character

The repeated-parameter principal series has the sum of the linear and Steinberg-twist characters. This is the character-theoretic two-constituent decomposition at the boundary of the principal series.

Irreducibility of the constituents

Mathlib's character-norm criterion currently requires the coefficient field and the group in the same universe. Accordingly the two Steinberg packaging results below use F : Type, as does the existing irreducibility theorem for the non-boundary principal series. The representations, their splitting, and the irreducibility of the linear constituent all remain universe-polymorphic.

theorem TauCeti.simple_GL2Steinberg (F : Type) [Field F] [Fintype F] : CategoryTheory.Simple (GL2Steinberg F)

The Steinberg representation of GL₂(F) is irreducible for a universe-small finite field F.

theorem TauCeti.simple_GL2SteinbergTwist (F : Type) [Field F] [Fintype F] (α : Fˣ →* ℂˣ) : CategoryTheory.Simple (GL2SteinbergTwist F α)

Every determinant twist of the Steinberg representation is irreducible for a universe-small finite field F.

@[simp]

theorem TauCeti.character_GL2SteinbergTwist_mem_irreducibleCharacters (F : Type) [Field F] [Fintype F] (α : Fˣ →* ℂˣ) : (GL2SteinbergTwist F α).character ∈ irreducibleCharacters ℂ (GL (Fin 2) F)

The Steinberg twists are irreducible characters of GL₂(F).

theorem TauCeti.nonempty_iso_GL2PrincipalSeries_self (F : Type u) [Field F] [Fintype F] (α : Fˣ →* ℂˣ) : Nonempty (GL2PrincipalSeries F α α ≅ GL2Linear F α ⊞ GL2SteinbergTwist F α)

The boundary principal series splits into its linear and Steinberg constituents. For a multiplicative character α : Fˣ → ℂˣ, Ind_B^GL₂(α ⊗ α) is isomorphic to the biproduct of the determinant character α ∘ det and its Steinberg twist.