The principal series of GL₂(𝔽_q) is irreducible exactly off the diagonal

The principal series Ind_B^{GL₂}(α ⊗ β) of GL₂(𝔽_q) is irreducible if and only if the two characters α, β : 𝔽_qˣ → ℂˣ are distinct. Its definition and its dimension q + 1 are in TauCeti/RepresentationTheory/CharacterTable/GL2/PrincipalSeries/Basic.lean.

The proof is the Mackey irreducibility criterion TauCeti.simple_indFDRep_iff run against the Bruhat decomposition. The criterion says that Ind_B^{GL₂} A is irreducible exactly when A is irreducible and, for every s ∉ B, the restrictions of A and of its conjugate {}^s A to B ⊓ sBs⁻¹ share no nonzero intertwiner. The Borel representation α ⊗ β is a line, hence irreducible, and Bruhat collapses the second condition: every s ∉ B is b₁ w b₂ for the Weyl element w = !![0, 1; 1, 0], and Mackey disjointness depends only on the double coset (TauCeti.mackeyDisjoint_mul_left_mul_right_iff), so the whole criterion becomes one condition at w.

At w the two restrictions are again lines, so Schur's lemma (FDRep.finrank_hom_simple_simple) turns disjointness into non-isomorphism. More generally, the restriction attached to (α, β) is isomorphic to the Weyl-conjugated restriction attached to (γ, δ) exactly when α = δ and β = γ: the diagonal matrices diag(a, 1) and diag(1, b) recover both equalities, while conjugation by w swaps the two diagonal coordinates. Specializing to (γ, δ) = (α, β) gives the required criterion α ≠ β.

Main definitions

• TauCeti.GL2Borel.mackeyTorusElt: a diagonal matrix, read as an element of the Mackey subgroup at the Weyl element; this is where the two sides of the Mackey condition are compared.

Main statements

• TauCeti.GL2Borel.inv_weyl_mul_torusHom_mul_weyl: conjugating a diagonal matrix by the Weyl element swaps its two entries.
• TauCeti.GL2Borel.nonempty_iso_mackey_weyl_iff: the two Weyl-cell restrictions are isomorphic exactly when their parameter pairs are swapped.
• TauCeti.GL2Borel.mackeyDisjoint_weyl_iff: the single Mackey condition, at the Weyl element, holds exactly when α ≠ β.
• TauCeti.simple_GL2PrincipalSeries_iff: the principal series Ind_B^{GL₂}(α ⊗ β) is irreducible if and only if α ≠ β.
• TauCeti.character_GL2PrincipalSeries_mem_irreducibleCharacters: for α ≠ β, its character is an irreducible character of GL₂(F).

Implementation notes

The universe of F is pinned to Type in the representation-theoretic statements, unlike in TauCeti/RepresentationTheory/CharacterTable/GL2/PrincipalSeries/Basic.lean, where the principal series is defined for F : Type u. The Mackey criterion TauCeti.simple_indFDRep_iff asks for the coefficient field and the group to lie in the same universe, and the coefficient field here is ℂ : Type; pinning F : Type is what puts GL (Fin 2) F there too. The criterion therefore covers finite fields presented by a Type-valued representative — every finite field has one, up to a ring isomorphism, namely GaloisField p n — but it does not apply directly to a finite field declared in some Type u with u ≠ 0; such a presentation first has to be transported along a ring isomorphism with a small model. The purely group-theoretic lemmas about the Weyl conjugation keep both an arbitrary universe and an arbitrary commutative ring.

That pin is not a choice this file could make differently. The predicate TauCeti.MackeyDisjoint is itself declared for a field and a group in one universe, so the very statement of the Mackey condition at ℂ and GL (Fin 2) F needs F : Type; and the criterion that consumes it ends at Mathlib's FDRep.simple_iff_end_is_rank_one, which is stated for {k : Type u} {G : Type u}. Relaxing the pin therefore means an upstream generalization of that Mathlib lemma, not a change here. TauCeti/RepresentationTheory/CharacterTable/GL2/Steinberg.lean records the same obstruction for the companion criterion FDRep.simple_iff_char_is_norm_one.

Mackey disjointness is unfolded through TauCeti.mackeyDisjoint_iff_finrank_eq_zero and Schur's lemma rather than by exhibiting intertwiners by hand: both sides of the Mackey condition at w are one-dimensional, so FDRep.finrank_hom_simple_simple reduces the condition to the existence of an isomorphism, and for one-dimensional representations an isomorphism is exactly an equality of the characters they carry.

The membership diag(a, 1) ∈ B ⊓ wBw⁻¹ is all that is used of the Mackey subgroup; the file deliberately does not compute B ⊓ wBw⁻¹ to be the split torus, because the reducible direction needs no such description — α ∘ det is conjugation-invariant on all of GL₂, not only on the torus.

References

• J.-P. Serre, Linear Representations of Finite Groups, GTM 42, §7.3, Proposition 23.
• C. Bonnafé, Representations of SL₂(𝔽_q) (2011), Chapter 5.
• W. Fulton and J. Harris, Representation Theory: A First Course, GTM 129, Lecture 5.2.

The Weyl conjugation on the split torus

theorem TauCeti.GL2Borel.inv_weyl_mul_torusHom_mul_weyl {R : Type u_1} [CommRing R] (p : Rˣ × Rˣ) : (GL2WeylElement R)⁻¹ * ↑(torusHom p) * GL2WeylElement R = ↑(torusHom (p.2, p.1))

Conjugating a diagonal matrix by the Weyl element swaps its two entries. This is the whole geometric content of the Mackey condition for the principal series: the w-conjugate of the character α ⊗ β is β ⊗ α.

theorem TauCeti.GL2Borel.torusHom_mem_mackeySubgroup_weyl {R : Type u_1} [CommRing R] (p : Rˣ × Rˣ) : ↑(torusHom p) ∈ mackeySubgroup (GL2WeylElement R) (GL2Borel R) (GL2Borel R)

The diagonal matrices lie in the Mackey subgroup at the Weyl element. They are upper triangular, and so are their w-conjugates, which are again diagonal.

def TauCeti.GL2Borel.mackeyTorusElt {R : Type u_1} [CommRing R] (p : Rˣ × Rˣ) : ↥((mackeySubgroup (GL2WeylElement R) (GL2Borel R) (GL2Borel R)).subgroupOf (GL2Borel R))

The diagonal matrix diag(a, d), read as an element of the Mackey subgroup at the Weyl element viewed inside the Borel subgroup. This is the one element the character computation is performed at.

Equations

• TauCeti.GL2Borel.mackeyTorusElt p = ⟨TauCeti.GL2Borel.torusHom p, ⋯⟩

@[simp]

theorem TauCeti.GL2Borel.coe_mackeyTorusElt {R : Type u_1} [CommRing R] (p : Rˣ × Rˣ) : ↑(mackeyTorusElt p) = torusHom p

@[simp]

theorem TauCeti.GL2Borel.mackeyToH_mackeyTorusElt {R : Type u_1} [CommRing R] (p : Rˣ × Rˣ) : (mackeyToH (GL2WeylElement R) (GL2Borel R) (GL2Borel R)) (mackeyTorusElt p) = torusHom (p.2, p.1)

The Mackey conjugation swaps the two torus coordinates. Together with TauCeti.GL2Borel.linearChar_torusHom this is what makes the two sides of the Mackey condition take the values α a and β a at diag(a, 1).

@[simp]

theorem TauCeti.GL2Borel.diag_mackeyToH {R : Type u_1} [CommRing R] (g : ↥((mackeySubgroup (GL2WeylElement R) (GL2Borel R) (GL2Borel R)).subgroupOf (GL2Borel R))) : diag ((mackeyToH (GL2WeylElement R) (GL2Borel R) (GL2Borel R)) g) = ((diag ↑g).2, (diag ↑g).1)

Mackey conjugation at the Weyl element swaps the diagonal coordinates. This is the coordinate form of the Weyl action on the split torus. It applies to every element of the Mackey subgroup; no diagonal-matrix hypothesis is needed, since conjugation by the Weyl element swaps the two diagonal entries of an arbitrary matrix.

theorem TauCeti.GL2Borel.det_mackeyToH {R : Type u_1} [CommRing R] (g : ↥((mackeySubgroup (GL2WeylElement R) (GL2Borel R) (GL2Borel R)).subgroupOf (GL2Borel R))) : Matrix.GeneralLinearGroup.det ↑((mackeyToH (GL2WeylElement R) (GL2Borel R) (GL2Borel R)) g) = Matrix.GeneralLinearGroup.det ↑↑g

The determinant does not see the Mackey conjugation. Conjugation is inner and the determinant is a homomorphism into a commutative group, so it is unchanged; this is why the boundary character α ∘ det gives a reducible principal series.

The Mackey condition at the Weyl element

@[simp]

theorem TauCeti.GL2Borel.nonempty_iso_mackey_weyl_iff {F : Type u_1} [CommRing F] (α β γ δ : Fˣ →* ℂˣ) : Nonempty (((mackeySubgroup (GL2WeylElement F) (GL2Borel F) (GL2Borel F)).subgroupOf (GL2Borel F)).resFDRep (GL2BorelRep F α β) ≅ (Action.res (FGModuleCat ℂ) (mackeyToH (GL2WeylElement F) (GL2Borel F) (GL2Borel F))).obj (GL2BorelRep F γ δ)) ↔ α = δ ∧ β = γ

The two Weyl-cell restrictions are isomorphic exactly when their parameters are swapped. This characterization supplies the Weyl-cell contribution to the principal-series intertwining number.

@[simp]

theorem TauCeti.GL2Borel.mackeyDisjoint_weyl_iff {F : Type} [CommRing F] (α β : Fˣ →* ℂˣ) : MackeyDisjoint (GL2BorelRep F α β) (GL2WeylElement F) ↔ α ≠ β

The Mackey condition of the principal series, at the Weyl element. The restrictions of α ⊗ β and of its w-conjugate to B ⊓ wBw⁻¹ are disjoint exactly when α ≠ β. Together with the Bruhat decomposition this is the whole content of TauCeti.simple_GL2PrincipalSeries_iff.

The irreducibility criterion

@[simp]

theorem TauCeti.simple_GL2PrincipalSeries_iff (F : Type) [Field F] [Fintype F] (α β : Fˣ →* ℂˣ) : CategoryTheory.Simple (GL2PrincipalSeries F α β) ↔ α ≠ β

The principal series is irreducible exactly off the diagonal. For a finite field F and characters α, β : Fˣ → ℂˣ, the parabolically induced representation Ind_B^{GL₂}(α ⊗ β) of GL₂(F) is irreducible if and only if α ≠ β.

Together with TauCeti.finrank_GL2PrincipalSeries this produces the (q + 1)-dimensional family of the character table of GL₂(𝔽_q); at α = β the induced representation is the reducible one whose two constituents are the linear character α ∘ det and a twist of the Steinberg representation.

theorem TauCeti.character_GL2PrincipalSeries_mem_irreducibleCharacters (F : Type) [Field F] [Fintype F] {α β : Fˣ →* ℂˣ} (hαβ : α ≠ β) : (GL2PrincipalSeries F α β).character ∈ irreducibleCharacters ℂ (GL (Fin 2) F)

The principal series with α ≠ β are irreducible characters of GL₂(F).