Twisting the principal series of GL₂(𝔽_q) by a determinant character

Multiplying both parameters of the principal series by a character γ : Fˣ →* ℂˣ multiplies its character by the determinant character γ ∘ det:

χ(Ind_B^{GL₂}(γα ⊗ γβ)) = (γ ∘ det) · χ(Ind_B^{GL₂}(α ⊗ β)).

This is the projection formula for induced class functions, because the Borel character γα ⊗ γβ is the pointwise product of α ⊗ β with the restriction of γ ∘ det to the Borel subgroup (TauCeti.GL2LinearChar_comp_gl2BorelSubtype).

At α = β = 1 the identity turns the character of the permutation representation on the projective line into the character of the principal series at the repeated parameter (γ, γ), which is how TauCeti/RepresentationTheory/CharacterTable/GL2/Boundary.lean splits that principal series.

Main statements

• TauCeti.character_GL2PrincipalSeries_mul_eq_mul: twisting both principal-series parameters by γ multiplies the induced character by the determinant character of γ.

References

• J.-P. Serre, Linear Representations of Finite Groups, GTM 42, Chapter 7 — the projection formula for induced characters.

@[simp]

theorem TauCeti.character_GL2PrincipalSeries_mul_eq_mul (F : Type u) [Field F] [Fintype F] (γ α β : Fˣ →* ℂˣ) : (GL2PrincipalSeries F (γ * α) (γ * β)).character = (GL2Linear F γ).character * (GL2PrincipalSeries F α β).character

Twisting both principal-series parameters multiplies the character by a determinant character. For γ α β : Fˣ → ℂˣ, the equality χ(Ind_B^GL₂(γα ⊗ γβ)) = (γ ∘ det) · χ(Ind_B^GL₂(α ⊗ β)). At α = β = 1, this identifies the repeated-parameter principal-series character as a determinant twist of the untwisted boundary character.