Documentation

TauCeti.RepresentationTheory.CharacterTable.GL2.Steinberg

The Steinberg representation of GL₂(𝔽_q) #

The Borel subgroup B of GL₂(𝔽_q) has index q + 1, and GL₂ permutes the cosets GL₂ ⧸ B — the points of the projective line. The resulting permutation representation ℂ[GL₂ ⧸ B] has the same character as the principal series Ind_B^{GL₂}(1 ⊗ 1) of TauCeti/RepresentationTheory/CharacterTable/GL2/PrincipalSeries/Basic.lean at the boundary value α = β = 1, where it is reducible: it contains the line spanned by the sum of the cosets, on which GL₂ acts trivially. The complement of that line is the Steinberg representation TauCeti.GL2Steinberg, of dimension q.

This file builds it as the augmentation subrepresentation of ℂ[GL₂ ⧸ B] — the elements whose coefficients sum to zero, of TauCeti/RepresentationTheory/Augmentation.lean — and computes its dimension and its character. The character values are the fixed-coset counts less one, and the Bruhat decomposition then gives the character-theoretic form of irreducibility: the Steinberg character has norm 1 for the character pairing of TauCeti/RepresentationTheory/CharacterTable/Pairing.lean. Everything proved here is an identity between characters; irreducibility itself is not proved here. The splitting of the boundary principal series as a representation is TauCeti.nonempty_iso_GL2PrincipalSeries_self in TauCeti/RepresentationTheory/CharacterTable/GL2/Boundary.lean.

Main definitions #

Main statements #

Implementation notes #

An object of FDRep ℂ G carries a ℂ-module in Type, while the coset space GL₂(F) ⧸ B lies in the universe of F; TauCeti.GL2Steinberg therefore transports the carrier down with FDRep.ofShrink, exactly as TauCeti.indFDRep does for induced representations, so that the construction stays universe-polymorphic in F. The transport itself is never reasoned about here: the dimension and the character below go through the generic transfer lemmas FDRep.finrank_ofShrink and FDRep.character_ofShrink, and TauCeti.GL2SteinbergEquiv — the comparison equivalence that FDRep.ofShrinkEquiv supplies — is public so that consumers can read off anything else the same way. It is not a restatement they could do without: the body of TauCeti.GL2Steinberg is not exposed, so FDRep.ofShrinkEquiv does not elaborate at that type outside this file.

TauCeti.characterPairing_GL2Steinberg_self carries a [DecidableEq F] hypothesis, which the other statements do not. It is used, not decorative: TauCeti.ClassFunction.characterPairing averages over a Fintype of the group, and a Fintype (GL (Fin 2) F) instance needs decidable equality on the matrix entries.

The irreducibility of the Steinberg representation is packaged downstream as TauCeti.simple_GL2Steinberg, using the norm computed here and Mathlib's FDRep.simple_iff_char_is_norm_one. That criterion is stated for a coefficient field and a group in the same universe, so the downstream theorem necessarily pins F : Type; keeping it out of this file preserves the universe polymorphism of the construction and character computation. It also keeps the fundamental theorem of algebra, needed for the IsAlgClosed ℂ instance, out of this foundational module.

References #

The definition and the dimension #

source
noncomputable def TauCeti.GL2Steinberg (F : Type u) [Field F] [Fintype F] :
FDRep ℂ (GL (Fin 2) F)

The Steinberg representation of GL₂(𝔽_q): the augmentation subrepresentation of the permutation representation ℂ[GL₂ ⧸ B] on the cosets of the Borel subgroup, that is, the complement of its invariant line. It has dimension q, and ℂ[GL₂ ⧸ B] has the character of the boundary principal series Ind_B^{GL₂}(1 ⊗ 1).

Equations
Instances For
    source
    noncomputable def TauCeti.GL2SteinbergEquiv (F : Type u) [Field F] [Fintype F] :
    Representation.Equiv (GL2Steinberg F).ρ (augmentationSubrepresentation ℂ (GL (Fin 2) F) (GL (Fin 2) F ⧸ GL2Borel F)).toRepresentation

    The Steinberg representation carries the augmentation subrepresentation of ℂ[GL₂ ⧸ B]. Shrinking the carrier to Type is a change of model, not of representation, so everything about TauCeti.GL2Steinberg may be read off the augmentation subrepresentation through this equivalence.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.finrank_GL2Steinberg (F : Type u) [Field F] [Fintype F] :
      Module.finrank ℂ ↑(GL2Steinberg F).V = Fintype.card F

      The Steinberg representation has dimension q, one less than the q + 1 points of the projective line.

      The character #

      source
      @[simp]
      theorem TauCeti.character_GL2Steinberg (F : Type u) [Field F] [Fintype F] (g : GL (Fin 2) F) :
      (GL2Steinberg F).character g = ↑(Nat.card { q : GL (Fin 2) F ⧸ GL2Borel F // g • q = q }) - 1

      The Steinberg character counts fixed points on the projective line, less one. The permutation character of ℂ[GL₂ ⧸ B] is the number of cosets fixed by g, and the invariant line accounts for exactly 1 of it.

      The character of the boundary principal series #

      source
      theorem TauCeti.character_GL2PrincipalSeries_one_one_eq_character_ofMulAction (F : Type u) [Field F] [Fintype F] (g : GL (Fin 2) F) :
      (GL2PrincipalSeries F 1 1).character g = (Representation.ofMulAction ℂ (GL (Fin 2) F) (GL (Fin 2) F ⧸ GL2Borel F)).character g

      The boundary principal series has the character of the permutation representation on the projective line. At α = β = 1 the character of Ind_B^{GL₂}(1 ⊗ 1) is the character of ℂ[GL₂ ⧸ B], because inducing the trivial character of B is inducing the trivial representation. The two representations are only shown to have the same character here, not identified.

      source
      @[simp]
      theorem TauCeti.character_GL2PrincipalSeries_one_one_eq_one_add (F : Type u) [Field F] [Fintype F] (g : GL (Fin 2) F) :
      (GL2PrincipalSeries F 1 1).character g = 1 + (GL2Steinberg F).character g

      The character of the boundary principal series is 1 plus the Steinberg character. The 1 is the trivial character, carried by the invariant line of ℂ[GL₂ ⧸ B]. This is the character-theoretic form of the two-constituent splitting; the corresponding isomorphism of representations is TauCeti.nonempty_iso_GL2PrincipalSeries_self.

      The norm of the Steinberg character #

      source
      @[simp]
      theorem TauCeti.characterPairing_GL2Steinberg_self (F : Type u) [Field F] [Fintype F] [DecidableEq F] :
      (ClassFunction.characterPairing (ClassFunction.ofFDRep (GL2Steinberg F))) (ClassFunction.ofFDRep (GL2Steinberg F)) = 1

      The Steinberg character has norm 1. This is the character-theoretic form of the irreducibility of the Steinberg representation; TauCeti.simple_GL2Steinberg in TauCeti/RepresentationTheory/CharacterTable/GL2/Boundary.lean packages it as CategoryTheory.Simple.