The binary quadratic form of a 2 × 2 matrix

To a matrix M = !![a, b; c, d] we attach the binary quadratic form Q_M = c x² + (d - a) x y - b y², whose value at v = (x, y) is the determinant of the matrix with columns v and M v (this is not the Gram form vᵀ M v). Its roots are the fixed points of M acting by Möbius transformations: for invertible M, Q_M(z, 1) is Mathlib's Matrix.GeneralLinearGroup.fixpointPolynomial. The discriminant of Q_M is tr(M)² - 4 det M, Mathlib's Matrix.discr M, and conjugating M by γ ∈ SL(2, R) acts on Q_M by the action γ • f = f ∘ γ⁻¹ of TauCeti.BinaryQuadraticForm.Basic.

Over ℤ, M ↦ Q_M is a bijection between the matrices of trace t and determinant n and the forms of discriminant t² - 4 n: the form determines c, b and d - a, the trace determines a + d, and (d - a)² + 4 b c = t² - 4 n forces d - a ≡ t (mod 2). This is the correspondence through which the Eichler–Selberg trace formula counts the elliptic conjugacy classes of matrices of determinant n by the Hurwitz class numbers H(4 n - t²).

Main definitions

• TauCeti.BinaryQuadraticForm.ofMatrix: the form Q_M = c x² + (d - a) x y - b y².
• TauCeti.BinaryQuadraticForm.ofMatrixEquiv: for t n : ℤ, the bijection M ↦ Q_M from the integer matrices of trace t and determinant n to the forms of discriminant t² - 4 n.

Main results

• TauCeti.BinaryQuadraticForm.discrim_ofMatrix: the discriminant of Q_M is tr(M)² - 4 det M.
• TauCeti.BinaryQuadraticForm.ofMatrix_conj: Q_{γ M γ⁻¹} = γ • Q_M for γ ∈ SL(2, R).
• TauCeti.BinaryQuadraticForm.ofMatrix_inj_of_trace_eq: when 2 is not a zero divisor, a 2 × 2 matrix is determined by its trace and its form Q_M.

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.

def TauCeti.BinaryQuadraticForm.ofMatrix {R : Type u_1} [CommRing R] (M : Matrix (Fin 2) (Fin 2) R) : BinaryQuadraticForm R

The binary quadratic form Q_M = c x² + (d - a) x y - b y² of the matrix M = !![a, b; c, d] (see eval_ofMatrix).

@[simp]

theorem TauCeti.BinaryQuadraticForm.ofMatrix_a {R : Type u_1} [CommRing R] (M : Matrix (Fin 2) (Fin 2) R) : (ofMatrix M).a = M 1 0

The x²-coefficient of Q_M is the lower left entry c of M.

@[simp]

theorem TauCeti.BinaryQuadraticForm.ofMatrix_b {R : Type u_1} [CommRing R] (M : Matrix (Fin 2) (Fin 2) R) : (ofMatrix M).b = M 1 1 - M 0 0

The x y-coefficient of Q_M is the difference d - a of the diagonal entries of M.

@[simp]

theorem TauCeti.BinaryQuadraticForm.ofMatrix_c {R : Type u_1} [CommRing R] (M : Matrix (Fin 2) (Fin 2) R) : (ofMatrix M).c = -M 0 1

The y²-coefficient of Q_M is -b, the negated upper right entry of M.

theorem TauCeti.BinaryQuadraticForm.eval_ofMatrix {R : Type u_1} [CommRing R] (M : Matrix (Fin 2) (Fin 2) R) (x y : R) : (ofMatrix M).eval x y = !![x, M.mulVec ![x, y] 0; y, M.mulVec ![x, y] 1].det

The value of Q_M at (x, y) is the determinant of the matrix with columns (x, y) and M (x, y).

@[simp]

theorem TauCeti.BinaryQuadraticForm.discrim_ofMatrix {R : Type u_1} [CommRing R] (M : Matrix (Fin 2) (Fin 2) R) : (ofMatrix M).discrim = M.trace ^ 2 - 4 * M.det

The discriminant of Q_M is tr(M)² - 4 det M.

theorem TauCeti.BinaryQuadraticForm.discrim_ofMatrix_eq_discr {R : Type u_1} [CommRing R] (M : Matrix (Fin 2) (Fin 2) R) : (ofMatrix M).discrim = M.discr

The discriminant of Q_M is Mathlib's discriminant Matrix.discr M of M.

theorem TauCeti.BinaryQuadraticForm.eval_ofMatrix_eq_eval_fixpointPolynomial {R : Type u_1} [CommRing R] (g : GL (Fin 2) R) (z : R) : (ofMatrix ↑g).eval z 1 = Polynomial.eval z g.fixpointPolynomial

For g ∈ GL(2, R), Q_g(z, 1) is Mathlib's fixed-point polynomial of g evaluated at z, whose roots are the fixed points of g acting by Möbius transformations.

theorem TauCeti.BinaryQuadraticForm.ofMatrix_conj {R : Type u_1} [CommRing R] (γ : Matrix.SpecialLinearGroup (Fin 2) R) (M : Matrix (Fin 2) (Fin 2) R) : ofMatrix (↑γ * M * ↑γ⁻¹) = γ • ofMatrix M

Conjugation by γ ∈ SL(2, R) acts on Q_M as γ acts on forms: Q_{γ M γ⁻¹} = γ • Q_M.

theorem TauCeti.BinaryQuadraticForm.ofMatrix_inj_of_trace_eq {R : Type u_1} [CommRing R] (h2 : IsLeftRegular 2) {M N : Matrix (Fin 2) (Fin 2) R} (h : M.trace = N.trace) : ofMatrix M = ofMatrix N ↔ M = N

When 2 is not a zero divisor in R, for instance over ℤ, ℤ_p or a field of characteristic other than two, a 2 × 2 matrix is determined by its trace and its form Q_M.

theorem TauCeti.BinaryQuadraticForm.two_mul_ediv_two_of_discrim_eq {f : BinaryQuadraticForm ℤ} {t n : ℤ} (hf : f.discrim = t ^ 2 - 4 * n) : 2 * ((t - f.b) / 2) = t - f.b

If an integral form has discriminant t² - 4 n, then t and its middle coefficient have the same parity.

def TauCeti.BinaryQuadraticForm.ofMatrixEquiv (t n : ℤ) : { M : Matrix (Fin 2) (Fin 2) ℤ // M.trace = t ∧ M.det = n } ≃ { f : BinaryQuadraticForm ℤ // f.discrim = t ^ 2 - 4 * n }

For t n : ℤ, M ↦ Q_M is a bijection from the integer matrices of trace t and determinant n to the integral forms of discriminant t² - 4 n. The inverse sends f = ⟨a, b, c⟩ to !![(t - b) / 2, -c; a, t - (t - b) / 2]; as b² - 4 a c = t² - 4 n forces b ≡ t (mod 2), its lower right entry is (t + b) / 2.

@[simp]

theorem TauCeti.BinaryQuadraticForm.coe_ofMatrixEquiv_apply {t n : ℤ} (M : { M : Matrix (Fin 2) (Fin 2) ℤ // M.trace = t ∧ M.det = n }) : ↑((ofMatrixEquiv t n) M) = ofMatrix ↑M

ofMatrixEquiv t n sends a matrix M to its form Q_M.

@[simp]

theorem TauCeti.BinaryQuadraticForm.coe_ofMatrixEquiv_symm_apply {t n : ℤ} (f : { f : BinaryQuadraticForm ℤ // f.discrim = t ^ 2 - 4 * n }) : ↑((ofMatrixEquiv t n).symm f) = !![(t - (↑f).b) / 2, -(↑f).c; (↑f).a, t - (t - (↑f).b) / 2]

The inverse of ofMatrixEquiv t n sends f = ⟨a, b, c⟩ to !![(t - b) / 2, -c; a, t - (t - b) / 2].