Centralizers of the regular elements of GL₂ #
A 2 × 2 matrix over a field is regular as soon as it is not scalar: it is then cyclic
(nonderogatory), and the matrices commuting with it are exactly the polynomials in it, the
two-dimensional algebra F[M]. That is TauCeti.commute_fin_two_iff, from
TauCeti.LinearAlgebra.Matrix.Commute, and it is what organizes this file.
Two consequences organize the conjugacy classes of GL₂(F). First, the commutant of a non-scalar
matrix is commutative, so the centralizer of a non-central element of GL₂(F) is an abelian
subgroup (TauCeti.isMulCommutative_centralizer_of_notMem_range_scalar). Second, when a regular
element generates a maximal commutative subalgebra of Matrix (Fin 2) (Fin 2) F — a split one,
F × F, or a quadratic field extension E/F — its centralizer is that subalgebra's unit group:
- the split case, an invertible diagonal matrix with distinct diagonal entries: its centralizer
is the split torus
TauCeti.diagonalTorus F 2of all invertible diagonal matrices (TauCeti.centralizer_diagGL), of order(q - 1)², so its conjugacy class hasq (q + 1)elements; - the non-split case, an element of
TauCeti.GL2NonSplitTorus— the unit group of a quadratic field extensionE/F— that does not come fromF: its centralizer is that whole group (TauCeti.GL2NonSplitTorus.centralizer_gl2NonSplitTorusHom), of orderq² - 1, so its conjugacy class hasq (q - 1)elements.
The split computation needs no commutant: a matrix commuting with a diagonal matrix of distinct
entries is diagonal (TauCeti.isDiag_of_commute_diagonal), and the torus is commutative. The same
is true of the non-semisimple case below, where two entry equations do the work. It is the
non-split case, and the abelianness of a general non-central centralizer, that consume
TauCeti.commute_fin_two_iff.
Over a finite field — more generally whenever E/F is separable — both elements are regular
semisimple and both centralizers are the maximal torus containing the element, split in the
first case and elliptic in the second. Those words are used only under that hypothesis: over an
imperfect field of characteristic two a purely inseparable quadratic extension E/F satisfies the
hypotheses of TauCeti.GL2NonSplitTorus.centralizer_gl2NonSplitTorusHom, and there multiplication
by an element of E ∖ F is not semisimple and Eˣ is not a torus; the general statement is proved
and read as a centralizer computation for a quadratic extension, with no semisimplicity claimed.
The counting results all assume F finite, where the torus language is unconditionally correct.
Both computations are stated for a normal form — a diagonal matrix, and an element of the non-split
torus in the basis TauCeti.nonSplitTorusBasis — rather than for an arbitrary regular semisimple
element. TauCeti.exists_isConj_normalForm of
TauCeti/LinearAlgebra/Matrix/GeneralLinearGroup/NormalForm.lean exhausts GL₂(𝔽_q) by four
named normal forms, of which these two are the regular semisimple ones — the central scalar
family is semisimple too, but not regular. That a regular semisimple element falls into one of
those two rather than into the scalar or the Jordan family, and that a centralizer transports
along a conjugation, are not proved here.
The third regular family is also here. A non-semisimple element is a Jordan block
TauCeti.jordanGL a b = !![a, b; 0, a] with b ≠ 0; it is again regular
(TauCeti.notMem_range_scalar_jordanGL), and its centralizer is
the scalar-unipotent subgroup TauCeti.GL2ScalarUnipotent F of all !![x, y; 0, x]
(TauCeti.centralizer_jordanGL), of order q (q - 1), so its conjugacy class has q² - 1
elements. That subgroup is the product Z U of the centre with the unipotent radical of the Borel
subgroup, so it is Gₘ × Gₐ and not a torus — which is precisely what distinguishes this family
from the two semisimple ones.
The fourth family, the central one, is the non-regular case this file's title excludes: a
scalar matrix is central in GL n R for any index type and any commutative semiring, so its
centralizer is everything and its class is a single point. The centralizer half is proved at that
generality in TauCeti.LinearAlgebra.Matrix.GeneralLinearGroup.Diagonal.Basic
(TauCeti.centralizer_scalar); the class size, TauCeti.ncard_carrier_mk_scalar, is here with the
other three.
Together the four families give the class sizes 1, q (q + 1), q (q - 1) and q² - 1. These
are the sizes of the individual classes, not the numbers of classes in each family: the
non-semisimple family, for instance, has one class for each of the q - 1 possible eigenvalues.
That every element of GL₂(𝔽_q) is conjugate to one of the four normal forms, and with it any
enumeration of the classes themselves, is not proved here.
The class sizes are read off the centralizer orders by orbit-stabilizer
(ConjClasses.ncard_carrier_mk), together with TauCeti.natCard_GL_fin_two, which gives
|GL₂(𝔽_q)| = (q - 1)² q (q + 1).
Main results #
TauCeti.isMulCommutative_centralizer_of_notMem_range_scalar: the centralizer of a non-central element ofGL (Fin 2) Fis abelian.TauCeti.centralizer_diagGL,TauCeti.natCard_centralizer_diagGL,TauCeti.ncard_carrier_mk_diagGL: the centralizer of an invertible diagonal matrix with distinct entries is the split torus, of order(q - 1)², and its conjugacy class hasq (q + 1)elements.TauCeti.GL2NonSplitTorus.centralizer_gl2NonSplitTorusHom,TauCeti.GL2NonSplitTorus.natCard_centralizer_gl2NonSplitTorusHom,TauCeti.GL2NonSplitTorus.ncard_carrier_mk_gl2NonSplitTorusHom: the centralizer of an element of the non-split torus not coming fromF— an elliptic element, over a finite field — is that whole torus, of orderq² - 1, and its conjugacy class hasq (q - 1)elements.TauCeti.centralizer_jordanGL,TauCeti.natCard_centralizer_jordanGL,TauCeti.ncard_carrier_mk_jordanGL: the centralizer of a Jordan block!![a, b; 0, a]withb ≠ 0— a non-semisimple element — is the scalar-unipotent subgroup, of orderq (q - 1), and its conjugacy class hasq² - 1elements.TauCeti.ncard_carrier_mk_scalar: the conjugacy class of a scalar matrix is a single point.
References #
- Character theory roadmap, Layer 9, "The conjugacy classes (a build target)".
- C. Bonnafé, Representations of
SL₂(𝔽_q)(2011), Chapter 1. - W. Fulton and J. Harris, Representation Theory: A First Course (1991), Lecture 5.2.
A non-central element of GL (Fin 2) F is one whose matrix is not scalar; the matrices
commuting with it then form a commutative algebra, so its centralizer is an abelian subgroup.
This is the prerequisite for the centralizers computed below being tori: an abelian overgroup of
the torus can be no larger than it.
The centralizer of an invertible diagonal matrix with distinct entries. Over a commutative
semiring in which every nonzero element cancels, such a matrix has, as its centralizer, exactly the
diagonal torus TauCeti.diagonalTorus k 2 of all invertible diagonal matrices.
Both inclusions come from the diagonal API: a matrix commuting with a diagonal matrix of distinct
entries is diagonal (TauCeti.isDiag_of_commute_diagonal), and conversely the torus is
commutative, so it centralizes each of its own elements. Only the first of these needs anything of
k, and only that its two distinct diagonal entries be separated by cancellation, so neither
subtraction nor inverses are used; a field is needed just for the counting below.
Over a field — where IsCancelMulZero is automatic — this is the centralizer of a split regular
semisimple element of GL₂: a diagonal matrix with distinct entries is then regular semisimple,
TauCeti.diagonalTorus k 2 is the split maximal torus, and the theorem says that the centralizer
of the element is the maximal torus containing it.
The order of the centralizer of a split regular semisimple element: over a field with q
elements the split torus has (q - 1)² elements, one invertible scalar per diagonal entry. No
finiteness is assumed: over an infinite field both sides vanish.
The centralizer of an element of GL₂ coming from a quadratic field extension. An element
of TauCeti.GL2NonSplitTorus F E, the unit group of a quadratic extension E/F acting on E
by multiplication, that does not come from F has that whole group as its centralizer.
When E/F is separable — always so over a finite field — such an element is elliptic regular
semisimple and TauCeti.GL2NonSplitTorus F E is the maximal torus containing it. Together with
TauCeti.centralizer_diagGL this computes the centralizer of each of the two standard regular
semisimple normal forms of GL₂, split and elliptic; that every regular semisimple element is
conjugate to one of them, and that a centralizer transports along such a conjugation, are not
proved here. Separability is not needed below: for a purely inseparable E/F in characteristic
two the statement computes the centralizer of an element that is not semisimple, and Eˣ is then
not a torus.
The order of the centralizer of an element of GL₂ coming from a quadratic extension: the
centralizer is TauCeti.GL2NonSplitTorus F E, a copy of Eˣ, so over a field with q elements
it has q² - 1 elements. As for TauCeti.GL2NonSplitTorus.natCard_eq, no finiteness is assumed:
over an infinite F both sides are 0. When E/F is separable — always so over a finite field —
this is the order of the elliptic maximal torus containing the element; nothing here needs that
hypothesis.
The size of an elliptic conjugacy class of GL₂(𝔽_q): it is q (q - 1) = [GL₂(𝔽_q) : T]
for the non-split torus T.
The centralizer of a Jordan block with regular off-diagonal entry. Over any commutative
ring, the centralizer of TauCeti.jordanGL a b = !![a, b; 0, a] with b left-regular — over a
field, any b ≠ 0 — is the scalar-unipotent subgroup TauCeti.GL2ScalarUnipotent R of the matrices
!![x, y; 0, x].
Like the split case this needs no commutant, and for the same reason: only the two entry equations
b · g₁₀ = b · 0 and b · g₁₁ = b · g₀₀ of M g = g M are used, and cancelling b from them is
what solves them — no division and no hypothesis on the other elements of R, so left-regularity of
b alone is enough, and a field is asked for only by the counting below. That the diagonal entry so
obtained is a unit is read off the determinant g₀₀². The reverse inclusion is the commutativity of
TauCeti.GL2ScalarUnipotent R.
Over a field this is the centralizer of a non-semisimple element, and unlike the split and
elliptic cases it is not a torus: it is the product Z U of the centre with the unipotent
radical of the Borel subgroup, Gₘ × Gₐ rather than Gₘ × Gₘ, which is exactly the failure of M
to be semisimple. As with the two semisimple normal forms, that every non-semisimple element of
GL₂(𝔽_q) is conjugate to a Jordan block, and that a centralizer transports along such a
conjugation, are not proved here.
The order of the centralizer of a regular non-semisimple element of GL₂: the centralizer
is TauCeti.GL2ScalarUnipotent F, a copy of Fˣ × (F, +), so over a field with q elements it has
(q - 1) q elements. As in the two semisimple cases no finiteness is assumed: over an infinite
field both sides are 0.
The size of a non-semisimple conjugacy class of GL₂(𝔽_q): it is
q² - 1 = [GL₂(𝔽_q) : Z U].
This is the last of the four class sizes: a central class has 1 element, a split semisimple class
q (q + 1), an elliptic class q (q - 1), and a non-semisimple class q² - 1.
The size of a central conjugacy class: the conjugacy class of a scalar matrix is a single
point. For GL₂(𝔽_q) these are the q - 1 central classes, the first of the four families of
conjugacy classes gathered in this file; nothing here is special to Fin 2 or to a field, so the
statement is made for an arbitrary finite index type over a commutative semiring.
The centralizer half of the statement, TauCeti.centralizer_scalar, is in
TauCeti.LinearAlgebra.Matrix.GeneralLinearGroup.Diagonal.Basic with the rest of the general-index
material; only the class size is here, so that the foundational diagonal module does not have to
import conjugacy theory for it.