The conjugation action of the special linear group on matrices

The special linear group SL(n, R) acts on the square matrices Matrix n n R by conjugation, g • M = g M g⁻¹. As for any conjugation action, it is recorded as an action of the type synonym ConjAct (SL(n, R)), so that it does not clash with the action of SL(n, R) on column vectors or with the scalar action of R. Mathlib provides the conjugation action ConjAct.unitsScalar of the units Mˣ of a monoid on M, which covers GL(n, R) acting on Matrix n n R, but not the action of SL(n, R), whose orbits are the SL(n, R)-conjugacy classes of matrices.

Conjugation preserves the trace, the determinant and, since adjugate g = g⁻¹ for g ∈ SL(n, R), commutes with taking adjugates.

Conjugation by SL(n, R) is conjugation by its image in GL(n, R), so SL(n, R)-conjugates are GL(n, R)-conjugates. Conversely, a conjugate g X g⁻¹ by g ∈ GL(n, R) is also a conjugate by SL(n, R) exactly when the determinant of g can be corrected inside the centralizer of X: some invertible matrix commuting with X has the same determinant as g.

Main definitions

• ConjAct.specialLinearGroupMulAction: the conjugation action g • M = g M g⁻¹ of ConjAct (SpecialLinearGroup n R) on Matrix n n R, with scalar multiplication ConjAct.specialLinearGroupScalar.
• TauCeti.traceDetFiber n t d: the n × n matrices of trace t and determinant d (TauCeti.mem_traceDetFiber), as a sub-action, whose orbits are the SL(n, R)-conjugacy classes of such matrices.

Main results

• ConjAct.specialLinearGroup_smul_def: g • M = g M g⁻¹.
• ConjAct.trace_specialLinearGroup_smul and ConjAct.det_specialLinearGroup_smul: conjugation preserves the trace and the determinant.
• Matrix.SpecialLinearGroup.trace_mul_mul_inv: the product form trace (P k P⁻¹) = trace k of trace invariance, for P k : SL(n, R).
• ConjAct.adjugate_specialLinearGroup_smul: conjugation commutes with the adjugate.
• ConjAct.toConjAct_toGL_smul: conjugating by s ∈ SL(n, R) is conjugating by its image in GL(n, R).
• Matrix.GeneralLinearGroup.toConjAct_smul_mem_orbit_specialLinearGroup_iff: a GL(n, R)-conjugate is an SL(n, R)-conjugate exactly when the determinant of the conjugator is the determinant of an invertible matrix in the centralizer.
• Matrix.GeneralLinearGroup.orbit_conjAct_specialLinearGroup_subset: an SL(n, R)-conjugate is a GL(n, R)-conjugate.
• TauCeti.adjugate_mem_traceDetFiber: for 2 × 2 matrices, the adjugate has the same trace and determinant.
• TauCeti.traceDetFiberAddScalarEquiv: for 2 × 2 matrices, translation M ↦ M + r by a scalar matrix maps the matrices of trace t and determinant d bijectively to those of trace t + 2 r and determinant d + r t + r².

References

• A. Popa and D. Zagier, An elementary proof of the Eichler–Selberg trace formula, J. Reine Angew. Math. 762 (2020), 105–122, arXiv:1711.00327, §1, equation (2): the sum over the SL(2, ℤ)-conjugacy classes of integer matrices of fixed trace and determinant, whose orbits this action describes.

@[instance_reducible]

instance ConjAct.specialLinearGroupScalar {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] : SMul (ConjAct (Matrix.SpecialLinearGroup n R)) (Matrix n n R)

SL(n, R) acts on Matrix n n R by conjugation, g • M = g M g⁻¹, through the type synonym ConjAct, in the manner of Mathlib's ConjAct.unitsScalar.

theorem ConjAct.specialLinearGroup_smul_def {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] (g : ConjAct (Matrix.SpecialLinearGroup n R)) (M : Matrix n n R) : g • M = ↑(ofConjAct g) * M * ↑(ofConjAct g)⁻¹

The conjugation action of SL(n, R) on matrices is g • M = g M g⁻¹.

@[instance_reducible]

instance ConjAct.specialLinearGroupMulAction {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] : MulAction (ConjAct (Matrix.SpecialLinearGroup n R)) (Matrix n n R)

Conjugation g • M = g M g⁻¹ is an action of SL(n, R) on Matrix n n R.

@[simp]

theorem ConjAct.trace_specialLinearGroup_smul {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] (g : ConjAct (Matrix.SpecialLinearGroup n R)) (M : Matrix n n R) : (g • M).trace = M.trace

Conjugation by SL(n, R) preserves the trace.

@[simp]

theorem ConjAct.det_specialLinearGroup_smul {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] (g : ConjAct (Matrix.SpecialLinearGroup n R)) (M : Matrix n n R) : (g • M).det = M.det

Conjugation by SL(n, R) preserves the determinant.

@[simp]

theorem ConjAct.adjugate_specialLinearGroup_smul {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] (g : ConjAct (Matrix.SpecialLinearGroup n R)) (M : Matrix n n R) : (g • M).adjugate = g • M.adjugate

Conjugation by SL(n, R) commutes with the adjugate: adjugate (g M g⁻¹) = g (adjugate M) g⁻¹.

@[simp]

theorem ConjAct.toConjAct_toGL_smul {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] (s : Matrix.SpecialLinearGroup n R) (M : Matrix n n R) : toConjAct (Matrix.SpecialLinearGroup.toGL s) • M = toConjAct s • M

Conjugating a matrix by the image of s ∈ SL(n, R) in GL(n, R) is conjugating it by s.

theorem Matrix.GeneralLinearGroup.toConjAct_smul_mem_orbit_specialLinearGroup_iff {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] {g : GL n R} {X : Matrix n n R} : ConjAct.toConjAct g • X ∈ MulAction.orbit (ConjAct (SpecialLinearGroup n R)) X ↔ ∃ (c : GL n R), Commute (↑c) X ∧ det c = det g

Determinant correction of conjugators. Over a commutative ring R, the conjugate g X g⁻¹ of a matrix X by g ∈ GL(n, R) is also a conjugate of X by SL(n, R) exactly when some invertible matrix commuting with X has the determinant of g.

theorem Matrix.GeneralLinearGroup.orbit_conjAct_specialLinearGroup_subset {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] (X : Matrix n n R) : MulAction.orbit (ConjAct (SpecialLinearGroup n R)) X ⊆ MulAction.orbit (ConjAct (GL n R)) X

An SL(n, R)-conjugate of a matrix is a GL(n, R)-conjugate.

theorem Matrix.SpecialLinearGroup.trace_mul_mul_inv {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] (P k : SpecialLinearGroup n R) : (↑(P * k * P⁻¹)).trace = (↑k).trace

Conjugation in SL(n, R) preserves the trace: trace (P k P⁻¹) = trace k. This is the product form of ConjAct.trace_specialLinearGroup_smul.

def TauCeti.traceDetFiber (n : Type u_1) {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] (t d : R) : SubMulAction (ConjAct (Matrix.SpecialLinearGroup n R)) (Matrix n n R)

The matrices of trace t and determinant d, as a sub-action of the conjugation action of SL(n, R): its orbits are the SL(n, R)-conjugacy classes of such matrices.

@[simp]

theorem TauCeti.mem_traceDetFiber {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] {t d : R} {M : Matrix n n R} : M ∈ traceDetFiber n t d ↔ M.trace = t ∧ M.det = d

A matrix lies in traceDetFiber n t d exactly when its trace is t and its determinant d.

theorem TauCeti.mem_traceDetFiber_fin_two {R : Type u_2} [CommRing R] {t d : R} {M : Matrix (Fin 2) (Fin 2) R} : M ∈ traceDetFiber (Fin 2) t d ↔ M 0 0 + M 1 1 = t ∧ M 0 0 * M 1 1 - M 0 1 * M 1 0 = d

A 2 × 2 matrix lies in traceDetFiber (Fin 2) t d exactly when its entries satisfy M₀₀ + M₁₁ = t and M₀₀ M₁₁ - M₀₁ M₁₀ = d.

theorem TauCeti.adjugate_mem_traceDetFiber {R : Type u_2} [CommRing R] {t d : R} {M : Matrix (Fin 2) (Fin 2) R} (hM : M ∈ traceDetFiber (Fin 2) t d) : M.adjugate ∈ traceDetFiber (Fin 2) t d

The adjugate of a 2 × 2 matrix M has the trace and the determinant of M: it lies in traceDetFiber (Fin 2) t d whenever M does.

theorem TauCeti.add_scalar_mem_traceDetFiber {R : Type u_2} [CommRing R] {t d : R} {M : Matrix (Fin 2) (Fin 2) R} (hM : M ∈ traceDetFiber (Fin 2) t d) (r : R) : M + (Matrix.scalar (Fin 2)) r ∈ traceDetFiber (Fin 2) (t + 2 * r) (d + r * t + r ^ 2)

Adding the scalar matrix r to a 2 × 2 matrix of trace t and determinant d gives a matrix of trace t + 2 r and determinant d + r t + r².

def TauCeti.traceDetFiberAddScalarEquiv {R : Type u_2} [CommRing R] (t d r : R) : ↥(traceDetFiber (Fin 2) t d) ≃ ↥(traceDetFiber (Fin 2) (t + 2 * r) (d + r * t + r ^ 2))

Translation M ↦ M + r by a scalar matrix, from the 2 × 2 matrices of trace t and determinant d to those of trace t + 2 r and determinant d + r t + r².

@[simp]

theorem TauCeti.traceDetFiberAddScalarEquiv_apply_coe {R : Type u_2} [CommRing R] (t d r : R) (M : ↥(traceDetFiber (Fin 2) t d)) : ↑((traceDetFiberAddScalarEquiv t d r) M) = ↑M + (Matrix.scalar (Fin 2)) r

traceDetFiberAddScalarEquiv t d r adds the scalar matrix r.

@[simp]

theorem TauCeti.traceDetFiberAddScalarEquiv_symm_apply_coe {R : Type u_2} [CommRing R] (t d r : R) (M : ↥(traceDetFiber (Fin 2) (t + 2 * r) (d + r * t + r ^ 2))) : ↑((traceDetFiberAddScalarEquiv t d r).symm M) = ↑M - (Matrix.scalar (Fin 2)) r

The inverse of traceDetFiberAddScalarEquiv t d r subtracts the scalar matrix r.