The principal series of GL₂(𝔽_q)

A pair of characters α, β : Fˣ →* ℂˣ of the multiplicative group of a field inflates through the split torus to a one-dimensional character of the Borel subgroup B = T U of upper-triangular matrices, on which the unipotent radical acts trivially. Inducing that character up to GL₂ is parabolic induction, and the resulting representation

GL2PrincipalSeries F α β = Ind_B^{GL₂} (α ⊗ β)

is the principal series. Over a finite field with q elements the Borel subgroup has index q + 1, so the principal series has dimension q + 1.

This file builds the characters of B, the one-dimensional representations carrying them, the principal series itself, and its dimension. The irreducibility criterion α ≠ β is proved in TauCeti/RepresentationTheory/CharacterTable/GL2/PrincipalSeries/Irreducible.lean; the decomposition of the boundary case α = β into a linear character and the Steinberg representation is not proved here.

Main definitions

• TauCeti.GL2Borel.linearChar: the character b ↦ α b₁₁ · β b₂₂ of the Borel subgroup obtained by inflating a pair of characters through the split torus.
• TauCeti.GL2Borel.linearRep: the one-dimensional representation carrying that character.
• TauCeti.GL2BorelRep: the same representation as an object of FDRep ℂ B.
• TauCeti.GL2PrincipalSeries: the principal series Ind_B^{GL₂}(α ⊗ β).

Main statements

• TauCeti.GL2Borel.linearChar_unipotentHom: the character is trivial on the unipotent radical, so it is genuinely inflated from the split torus (TauCeti.GL2Borel.linearChar_torusHom).
• TauCeti.GL2Borel.linearChar_inj: the pair (α, β) is recovered from the character it inflates to, so distinct pairs give distinct one-dimensional representations of B.
• TauCeti.GL2Borel.linearChar_self: for α = β the Borel character is the determinant twisted by α; this is the boundary case whose principal series is reducible.
• TauCeti.GL2Borel.character_linearRep: the character of a one-dimensional representation is the scalar it acts by.
• TauCeti.GL2Borel.linearRep_def: the representation is the generic one-dimensional representation associated to TauCeti.GL2Borel.linearChar.
• TauCeti.GL2BorelRep_def: the bundled Borel representation is TauCeti.GL2Borel.linearRep, the form to reason from when the action itself, and not only its character, is needed.
• TauCeti.GL2Borel.nonempty_iso_borelRep_iff: two inducing Borel lines are isomorphic exactly when their ordered parameter pairs agree.
• TauCeti.finrank_GL2PrincipalSeries and TauCeti.character_one_GL2PrincipalSeries: the principal series has dimension q + 1.

Implementation notes

TauCeti.GL2Borel.linearChar and TauCeti.GL2Borel.linearRep are stated over an arbitrary commutative ring R for the group — the Borel subgroup itself is defined over any commutative ring — and over the weakest coefficients each needs: the character only multiplies values in kˣ, so it lives over a CommMonoid k, while the representation needs a module structure on the line and so lives over a CommSemiring k. Nothing in the inflation uses finiteness or the complex numbers, and neither does its bundled form TauCeti.GL2BorelRep, which is therefore stated over a CommRing F; the field and finiteness hypotheses enter only with TauCeti.GL2PrincipalSeries, where they supply the finite index that makes induction finite-dimensional.

The construction is universe-polymorphic in F. Although Mathlib's raw induced representation has a carrier in the universe of the group, TauCeti.indFDRep transports it to an equivalent small model whose carrier lies in the universe of the coefficient ring. It therefore produces an object of FDRep ℂ (GL (Fin 2) F) without restricting the universe of F.

TauCetiRoadmap/RepresentationTheory/CharacterTheory/Suggested.lean pins GL2PrincipalSeries with a [DecidableEq F] hypothesis. It is not needed: GL (Fin 2) F needs decidable equality only on the index type Fin 2, and carrying an unused instance argument would be flagged by the unusedArguments linter, so it is dropped here.

References

• Character theory roadmap, Layer 9, "The Borel and the principal series": the targets GL2PrincipalSeries and character_one_GL2PrincipalSeries, whose names are the roadmap's.
• C. Bonnafé, Representations of SL₂(𝔽_q) (2011), Chapter 5.
• W. Fulton and J. Harris, Representation Theory: A First Course (1991), Lecture 5.2.

The linear characters of the Borel subgroup

def TauCeti.GL2Borel.linearChar {R : Type u_1} [CommRing R] {k : Type u_2} [CommMonoid k] (α β : Rˣ →* kˣ) : ↥(GL2Borel R) →* kˣ

The linear character of the Borel subgroup attached to a pair of characters. The two diagonal entries of an upper-triangular matrix are units, and TauCeti.GL2Borel.diag reads them off; the character α ⊗ β sends b to α b₁₁ · β b₂₂. It is inflated from the split torus, being trivial on the unipotent radical.

Equations

• TauCeti.GL2Borel.linearChar α β = (α.comp (MonoidHom.fst Rˣ Rˣ) * β.comp (MonoidHom.snd Rˣ Rˣ)).comp TauCeti.GL2Borel.diag

@[simp]

theorem TauCeti.GL2Borel.linearChar_apply {R : Type u_1} [CommRing R] {k : Type u_2} [CommMonoid k] (α β : Rˣ →* kˣ) (g : ↥(GL2Borel R)) : (linearChar α β) g = α (diag g).1 * β (diag g).2

theorem TauCeti.GL2Borel.linearChar_torusHom {R : Type u_1} [CommRing R] {k : Type u_2} [CommMonoid k] (α β : Rˣ →* kˣ) (p : Rˣ × Rˣ) : (linearChar α β) (torusHom p) = α p.1 * β p.2

On the split torus the character is literally α ⊗ β.

theorem TauCeti.GL2Borel.linearChar_unipotentHom {R : Type u_1} [CommRing R] {k : Type u_2} [CommMonoid k] (α β : Rˣ →* kˣ) (b : R) : (linearChar α β) (unipotentHom b) = 1

The character is trivial on the unipotent radical, which is what makes it an inflation from the split torus rather than a general character of the Borel subgroup.

theorem TauCeti.GL2Borel.linearChar_inj {R : Type u_1} [CommRing R] {k : Type u_2} [CommMonoid k] {α β α' β' : Rˣ →* kˣ} : linearChar α β = linearChar α' β' ↔ α = α' ∧ β = β'

The pair of characters is recovered from the character it inflates to. Restricting along the two coordinate embeddings of the split torus returns α and β, so distinct pairs inflate to distinct characters of B, hence to non-isomorphic one-dimensional representations.

theorem TauCeti.GL2Borel.linearChar_self {R : Type u_1} [CommRing R] {k : Type u_2} [CommMonoid k] (α : Rˣ →* kˣ) (g : ↥(GL2Borel R)) : (linearChar α α) g = α (Matrix.GeneralLinearGroup.det ↑g)

The equal-character case is a determinant twist. When the two characters agree, the Borel character is the restriction of α ∘ det, the linear character of GL₂ whose principal series is the reducible one.

The one-dimensional representation carrying a linear character

def TauCeti.GL2Borel.linearRep {R : Type u_1} [CommRing R] {k : Type u_2} [CommSemiring k] (α β : Rˣ →* kˣ) : Representation k (↥(GL2Borel R)) k

The one-dimensional representation of the Borel subgroup on which b acts by the scalar TauCeti.GL2Borel.linearChar α β b. This is the representation α ⊗ β that parabolic induction consumes.

Equations

• TauCeti.GL2Borel.linearRep α β = Representation.ofLinearCharacter (TauCeti.GL2Borel.linearChar α β)

theorem TauCeti.GL2Borel.linearRep_def {R : Type u_1} [CommRing R] {k : Type u_2} [CommSemiring k] (α β : Rˣ →* kˣ) : linearRep α β = Representation.ofLinearCharacter (linearChar α β)

The Borel representation is the one-dimensional representation associated to TauCeti.GL2Borel.linearChar.

@[simp]

theorem TauCeti.GL2Borel.linearRep_apply {R : Type u_1} [CommRing R] {k : Type u_2} [CommSemiring k] (α β : Rˣ →* kˣ) (g : ↥(GL2Borel R)) (x : k) : ((linearRep α β) g) x = ↑((linearChar α β) g) * x

@[simp]

theorem TauCeti.GL2Borel.character_linearRep {R : Type u_1} [CommRing R] {k : Type u_2} [Field k] (α β : Rˣ →* kˣ) (g : ↥(GL2Borel R)) : (linearRep α β).character g = ↑((linearChar α β) g)

The character of a one-dimensional representation is the scalar it acts by: the trace of multiplication by c on the line k is c.

The one-dimensional representation of the Borel subgroup over ℂ

noncomputable def TauCeti.GL2BorelRep (F : Type u_1) [CommRing F] (α β : Fˣ →* ℂˣ) : FDRep ℂ ↥(GL2Borel F)

The one-dimensional representation α ⊗ β of the Borel subgroup, bundled as an object of FDRep ℂ B, which is the shape parabolic induction consumes.

Equations

• TauCeti.GL2BorelRep F α β = FDRep.of (TauCeti.GL2Borel.linearRep α β)

@[simp]

theorem TauCeti.finrank_GL2BorelRep (F : Type u_1) [CommRing F] (α β : Fˣ →* ℂˣ) : Module.finrank ℂ ↑(GL2BorelRep F α β).V = 1

The representation α ⊗ β of the Borel subgroup is one-dimensional.

theorem TauCeti.GL2BorelRep_def (F : Type u_1) [CommRing F] (α β : Fˣ →* ℂˣ) : GL2BorelRep F α β = FDRep.of (GL2Borel.linearRep α β)

TauCeti.GL2BorelRep is TauCeti.GL2Borel.linearRep bundled into FDRep ℂ B. Bundling changes the packaging, not the representation. This is the characterization downstream results that need the action itself — rather than its character — reason from, so none of them unfolds the definition.

@[simp]

theorem TauCeti.character_GL2BorelRep (F : Type u_1) [CommRing F] (α β : Fˣ →* ℂˣ) (g : ↥(GL2Borel F)) : (GL2BorelRep F α β).character g = ↑((GL2Borel.linearChar α β) g)

The character of TauCeti.GL2BorelRep is TauCeti.GL2Borel.linearChar.

@[simp]

theorem TauCeti.GL2Borel.nonempty_iso_borelRep_iff {F : Type u_1} [CommRing F] (α β γ δ : Fˣ →* ℂˣ) : Nonempty (GL2BorelRep F α β ≅ GL2BorelRep F γ δ) ↔ α = γ ∧ β = δ

The inducing Borel lines remember their ordered parameter pair. Two representations α ⊗ β and γ ⊗ δ of the Borel subgroup are isomorphic exactly when α = γ and β = δ.

The principal series

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

The principal series Ind_B^{GL₂}(α ⊗ β): the representation of GL₂(𝔽_q) induced from the one-dimensional character α ⊗ β of the Borel subgroup. This is parabolic induction in rank one.

Equations

• TauCeti.GL2PrincipalSeries F α β = TauCeti.indFDRep (TauCeti.GL2BorelRep F α β)

theorem TauCeti.GL2PrincipalSeries_def (F : Type u_1) [Field F] [Fintype F] (α β : Fˣ →* ℂˣ) : GL2PrincipalSeries F α β = indFDRep (GL2BorelRep F α β)

The principal series is the induction of TauCeti.GL2BorelRep. This is the characterization downstream results reason from, so none of them unfolds the definition.

@[simp]

theorem TauCeti.finrank_GL2PrincipalSeries (F : Type u_1) [Field F] [Fintype F] (α β : Fˣ →* ℂˣ) : Module.finrank ℂ ↑(GL2PrincipalSeries F α β).V = Fintype.card F + 1

The principal series has dimension q + 1, the index of the Borel subgroup, because it is induced from a one-dimensional representation.

theorem TauCeti.character_one_GL2PrincipalSeries (F : Type u_1) [Field F] [Fintype F] (α β : Fˣ →* ℂˣ) : (GL2PrincipalSeries F α β).character 1 = ↑(Fintype.card F) + 1

The principal series has dimension q + 1, read off the character at the identity.