The cosets of the Borel subgroup of GL₂ are the projective line #
The coset space GL₂(F) ⧸ B of the Borel subgroup of invertible upper-triangular matrices is the
projective line over F: a coset g B remembers exactly the line spanned by the first column
of g, because right multiplication by an upper-triangular matrix rescales that column. Mathlib
already models the projective line as OnePoint F, with the Möbius action of GL (Fin 2) F on it
(OnePoint.instGLAction), and this file supplies the missing bridge: the Borel subgroup is the
stabilizer of the point at infinity (TauCeti.GL2Borel.stabilizer_infty), and the action is
transitive, so translating ∞ identifies the two
(TauCeti.GL2Borel.quotientEquivOnePoint), equivariantly.
The point of the identification is the fixed-coset count, which the bridge turns into a
fixed-point count on OnePoint F, where Mathlib's OnePoint.smul_infty_eq_self_iff and
Matrix.GeneralLinearGroup.fixpointPolynomial_aeval_eq_zero_iff compute it. For an element
!![a, b; 0, d] of the Borel subgroup itself, ∞ is fixed and the fixed affine points are the
roots of the linear equation (d - a) t = b; so there are two fixed points when a ≠ d, and one
when a = d and b ≠ 0. A scalar matrix is central, so it fixes every coset, and an element with
no upper-triangular conjugate fixes none.
Those four statements are read off for the four families of conjugacy classes of GL₂(𝔽_q): a
scalar matrix fixes all q + 1 cosets, a diagonal matrix with distinct entries 2, a Jordan block
1, and an element of the non-split torus that does not come from F fixes 0. Those four
numbers, less one, are the character values of the Steinberg representation.
Only the scalar count needs F to be finite, and only because it is the one whose value is the
number of points; the other three are the same over any field, and the two general Borel counts
hold there too.
Main definitions #
TauCeti.GL2Borel.quotientEquivOnePoint: the identificationGL₂(F) ⧸ B ≃ OnePoint Fof the coset space with Mathlib's model of the projective line, by translating the point at infinity.
Main results #
TauCeti.GL2Borel.stabilizer_infty: the Borel subgroup is the stabilizer of∞for the Möbius action ofGL₂(F)onOnePoint F.TauCeti.GL2Borel.quotientEquivOnePoint_smul: that identification is equivariant, whenceTauCeti.GL2Borel.natCard_fixedCosets_eq_ncard, the fixed cosets ofgare counted by its fixed points onOnePoint F.TauCeti.GL2Borel.natCard_fixedCosets_of_mem_of_diagonal_neandTauCeti.GL2Borel.natCard_fixedCosets_of_mem_of_diagonal_eq_of_upperRight_ne_zero: an upper-triangular element fixes exactly2cosets when its diagonal entries differ, and exactly1when they agree and it is not diagonal.TauCeti.GL2Borel.scalar_smul_quotient_eq_selfandTauCeti.GL2Borel.natCard_fixedCosets_eq_zero: a scalar matrix fixes every coset, and an element with no upper-triangular conjugate fixes none.TauCeti.GL2Borel.natCard_fixedCosets_scalar,TauCeti.GL2Borel.natCard_fixedCosets_diagGL,TauCeti.GL2Borel.natCard_fixedCosets_jordanGLandTauCeti.GL2Borel.natCard_fixedCosets_gl2NonSplitTorusHom: the countsq + 1,2,1and0for the four families of conjugacy classes ofGL₂(𝔽_q).
References #
This supplies the fixed-point counts on the projective line that the character-value formulas of
Layer 9 ("the representation theory of GL₂(𝔽_q)") of
TauCetiRoadmap/RepresentationTheory/CharacterTheory/README.md need. See also W. Fulton and
J. Harris, Representation Theory: A First Course, GTM 129, §5.2, and C. Bonnafé,
Representations of SL₂(𝔽_q) (2011), Chapter 1.
An element with no upper-triangular conjugate fixes no coset at all. A fixed coset would exhibit such a conjugate. Over a field this is the elliptic case: the matrix has no eigenline.
The Borel subgroup is the stabilizer of the point at infinity for the Möbius action of
GL₂(F) on Mathlib's model OnePoint F of the projective line: the coset B is the line spanned
by the first basis vector.
The cosets of the Borel subgroup are the points of the projective line: translating the
point at infinity identifies GL₂(F) ⧸ B with Mathlib's model OnePoint F. It is a bijection
because TauCeti.GL2Borel.stabilizer_infty identifies the stabilizer of ∞ with B, and because
the action is transitive.
Equations
Instances For
The point of the projective line attached to the coset of g is g • ∞, the line spanned by
the first column of g.
The identification is equivariant, so it matches fixed cosets with fixed points.
The coset carried to ∞ is the Borel subgroup itself.
The coset carried to the affine point t is that of !![t, 1; 1, 0], whose first column spans
the line through (t, 1).
The fixed-coset count is a fixed-point count on the projective line, by the equivariant
identification TauCeti.GL2Borel.quotientEquivOnePoint.
An upper-triangular element with distinct diagonal entries fixes exactly two cosets: the Borel subgroup itself, and the line spanned by the second eigenvector.
An upper-triangular element with equal diagonal entries but a nonzero upper-right entry fixes exactly one coset: the Borel subgroup itself, the line of its single eigenvector.
An element of the non-split torus outside F fixes no coset at all. A fixed coset would
exhibit an upper-triangular conjugate, which is exactly what
TauCeti.GL2NonSplitTorus.conj_notMem_gl2Borel forbids. This is the elliptic case: no eigenvalue of
such a matrix lies in F, so it has no eigenline over F.
A scalar matrix fixes every coset, so it fixes all q + 1 points of the projective line.
Unlike its three companions this is deliberately not a simp lemma: over a finite field the fixed
cosets form a Fintype, so simp rewrites the left-hand side by Nat.card_eq_fintype_card and it
is not in simp-normal form.