Popa–Zagier's explicit Hecke element

Popa and Zagier prove the Eichler–Selberg trace formula with an explicit element of ℛₙ = ℚ[ℳₙ] (written Tₙ with a tilde in their paper), given by their eq. (15) as T₁ - T₂ - T₃ - T₄ with

• T₁ = ⟨a - d ≤ -b ≤ c; 0 ≤ c < a⟩,
• T₂ = ⟨-b ≤ a - d ≤ c; b < d ≤ 0⟩,
• T₃ = ⟨0 ≤ a - d ≤ c ≤ -b; a ≤ 0 < c⟩,
• T₄ = ⟨0 ≤ a - d ≤ -b ≤ c; d ≤ 0 < -b⟩.

Here ⟨#⟩ is the sum of the classes of the integral matrices M = (a b; c d) of determinant n satisfying the inequalities #, written in two lines (separated here by ;), each counted with a coefficient c(M) fixed by the inequalities of the first line that are equalities for M: it is 1 if there are none, 1/2 if there is one, and 1/4, 1/3 or 1/6 if there are two and they are independent (A ≤ B, C ≤ D), overlapping (A ≤ B, A ≤ C) or nested (A ≤ B ≤ C). Popa and Zagier represent classes by matrices with c ≥ 0. Every matrix occurring in (15) has c > 0, or c = 0 < a, so at most one of the representatives ±M of a class occurs, and the coefficient of the class of M is the sum of the weights of M and -M.

Main definitions

• TauCeti.PopaZagier.weight M: twelve times the coefficient of M in (15); TauCeti.PopaZagier.weight₁, ..., TauCeti.PopaZagier.weight₄: the same for T₁, ..., T₄.
• TauCeti.TraceFormulaMatrixModule.popaZagierElement k n: Popa–Zagier's element of k[ℳₙ], for a division ring k.

Main results

• TauCeti.PopaZagier.det_pos_of_weight_ne_zero, TauCeti.PopaZagier.abs_le_of_weight_ne_zero: every matrix occurring in (15) has positive determinant n and entries at most 2n in absolute value, so only finitely many occur for each n (Popa–Zagier, Lemma 4(a)).
• TauCeti.PopaZagier.finite_support_weight_traceDetFiber: in particular only finitely many matrices of a given trace and determinant have nonzero weight.
• TauCeti.PopaZagier.abs_le_of_weightᵢ_ne_zero: the same bound for a matrix of nonzero weight in any one of the four sums T₁, ..., T₄.
• TauCeti.PopaZagier.weight_neg_eq_zero: with Popa–Zagier's representatives, c > 0 or c = 0 < a, the matrix -M has weight zero, so simp computes coefficients as weight M / 12.
• TauCeti.PopaZagier.weight₂_eq_weight₁: T₂ = T₁·U, where U = T S = (1 -1; 1 0).
• TauCeti.PopaZagier.weight_smul: the weight of eq. (15) is invariant under positive scaling.
• TauCeti.TraceFormulaMatrixModule.abs_le_of_intCast_ne_zero: the same bound for any integer weight dominated by Popa–Zagier's, cast to an additive group with one, in the shape ofWeight takes.
• TauCeti.TraceFormulaMatrixModule.popaZagierElement_eq_inv_smul_ofWeight: the element is 12⁻¹ times the element with the integer weights.
• TauCeti.TraceFormulaMatrixModule.coeff_popaZagierElement_mk: the coefficient of the class of A is (weight A + weight (-A)) / 12; it is weight A / 12 if c > 0 or c = 0 < a (TauCeti.TraceFormulaMatrixModule.coeff_popaZagierElement_mk_of_pos).

Implementation notes

Popa and Zagier define their element by eq. (14) and prove that it equals (15) (Lemma 4(b)); we define it by (15).

The weights are integers, twelve times Popa–Zagier's coefficients, so that identities between them are statements of integer linear arithmetic. Their definitions are exposed (@[expose]) so that other modules can unfold them in such identities and evaluate them by decide +kernel.

The element popaZagierElement k n is 12⁻¹ times the element TauCeti.TraceFormulaMatrixModule.ofWeight built from the integer weight cast to k; when 12 is invertible in k, for instance for k = ℚ, its coefficients are Popa–Zagier's.

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, §4.

The weights

def TauCeti.PopaZagier.chainWeight₃ (x y z : ℤ) : ℤ

Twelve times Popa–Zagier's coefficient c(M) for a first line x ≤ y ≤ z: 12, 6 or 2 according as none, one or both of the two (nested) inequalities are equalities, and 0 if the line fails.

def TauCeti.PopaZagier.chainWeight₄ (w x y z : ℤ) : ℤ

Twelve times Popa–Zagier's coefficient c(M) for a first line w ≤ x ≤ y ≤ z: 12 or 6 according as none or one of the three inequalities is an equality, 3 if the outer two are (independent), 2 if two adjacent ones are (nested), and 0 if the line fails. The value when all three are equalities is not covered by the rule; it does not occur in (15).

theorem TauCeti.PopaZagier.le_of_chainWeight₃_ne_zero {x y z : ℤ} (h : chainWeight₃ x y z ≠ 0) : x ≤ y ∧ y ≤ z

A first line x ≤ y ≤ z of nonzero weight holds.

theorem TauCeti.PopaZagier.le_of_chainWeight₄_ne_zero {w x y z : ℤ} (h : chainWeight₄ w x y z ≠ 0) : w ≤ x ∧ x ≤ y ∧ y ≤ z

A first line w ≤ x ≤ y ≤ z of nonzero weight holds.

def TauCeti.PopaZagier.weight₁ (a b c d : ℤ) : ℤ

Twelve times the coefficient of (a b; c d) in T₁ = ⟨a - d ≤ -b ≤ c; 0 ≤ c < a⟩.

def TauCeti.PopaZagier.weight₂ (a b c d : ℤ) : ℤ

Twelve times the coefficient of (a b; c d) in T₂ = ⟨-b ≤ a - d ≤ c; b < d ≤ 0⟩.

def TauCeti.PopaZagier.weight₃ (a b c d : ℤ) : ℤ

Twelve times the coefficient of (a b; c d) in T₃ = ⟨0 ≤ a - d ≤ c ≤ -b; a ≤ 0 < c⟩.

def TauCeti.PopaZagier.weight₄ (a b c d : ℤ) : ℤ

Twelve times the coefficient of (a b; c d) in T₄ = ⟨0 ≤ a - d ≤ -b ≤ c; d ≤ 0 < -b⟩.

def TauCeti.PopaZagier.weight (M : Matrix (Fin 2) (Fin 2) ℤ) : ℤ

Twelve times the coefficient of the matrix M in Popa–Zagier's eq. (15), T₁ - T₂ - T₃ - T₄.

theorem TauCeti.PopaZagier.weight₂_eq_weight₁ (a b c d : ℤ) : weight₂ a b c d = weight₁ (-b) (a + b) (-d) (c + d)

T₂ = T₁·U: the weight of M = (a b; c d) in T₂ is the weight of M U⁻¹ = (-b, a + b; -d, c + d) in T₁, where U = T S = (1 -1; 1 0).

Invariance under scaling

theorem TauCeti.PopaZagier.weight₃_mul {r : ℤ} (hr : 0 < r) (a b c d : ℤ) : weight₃ (r * a) (r * b) (r * c) (r * d) = weight₃ a b c d

The weight of a matrix in T₃ is invariant under scaling it by a positive integer.

theorem TauCeti.PopaZagier.weight₄_mul {r : ℤ} (hr : 0 < r) (a b c d : ℤ) : weight₄ (r * a) (r * b) (r * c) (r * d) = weight₄ a b c d

The weight of a matrix in T₄ is invariant under scaling it by a positive integer.

theorem TauCeti.PopaZagier.weight_smul {r : ℤ} (hr : 0 < r) (M : Matrix (Fin 2) (Fin 2) ℤ) : weight (r • M) = weight M

The coefficient c(M) of eq. (15) only depends on which of its linear inequalities hold and which of them are equalities, so it is invariant under scaling M by a positive integer.

Finiteness

theorem TauCeti.PopaZagier.abs_le_of_weightᵢ_ne_zero {M : Matrix (Fin 2) (Fin 2) ℤ} (h : weight₁ (M 0 0) (M 0 1) (M 1 0) (M 1 1) ≠ 0 ∨ weight₂ (M 0 0) (M 0 1) (M 1 0) (M 1 1) ≠ 0 ∨ weight₃ (M 0 0) (M 0 1) (M 1 0) (M 1 1) ≠ 0 ∨ weight₄ (M 0 0) (M 0 1) (M 1 0) (M 1 1) ≠ 0) (i j : Fin 2) : |M i j| ≤ 2 * M.det

Every matrix of nonzero weight in one of the four sums T₁, ..., T₄ of (15) has entries at most twice its determinant in absolute value.

theorem TauCeti.PopaZagier.det_pos_of_weight_ne_zero {M : Matrix (Fin 2) (Fin 2) ℤ} (h : weight M ≠ 0) : 0 < M.det

Popa–Zagier, Lemma 4(a), positivity: every matrix of nonzero weight has positive determinant.

theorem TauCeti.PopaZagier.abs_le_of_weight_ne_zero {M : Matrix (Fin 2) (Fin 2) ℤ} (h : weight M ≠ 0) (i j : Fin 2) : |M i j| ≤ 2 * M.det

Popa–Zagier, Lemma 4(a), finiteness: every matrix of nonzero weight has entries at most twice its determinant in absolute value.

theorem TauCeti.PopaZagier.finite_support_weight_traceDetFiber (t n : ℤ) : (Function.support fun (M : ↥(traceDetFiber (Fin 2) t n)) => weight ↑M).Finite

Only finitely many matrices of trace t and determinant n have nonzero weight: their entries are at most 2 n in absolute value (abs_le_of_weight_ne_zero).

theorem TauCeti.PopaZagier.pos_or_eq_zero_and_pos_of_weight_ne_zero {M : Matrix (Fin 2) (Fin 2) ℤ} (h : weight M ≠ 0) : 0 < M 1 0 ∨ M 1 0 = 0 ∧ 0 < M 0 0

Every matrix M = (a b; c d) of nonzero weight has c > 0, or c = 0 < a.

@[simp]

theorem TauCeti.PopaZagier.weight_neg_eq_zero {M : Matrix (Fin 2) (Fin 2) ℤ} (hM : 0 < M 1 0 ∨ M 1 0 = 0 ∧ 0 < M 0 0) : weight (-M) = 0

With Popa–Zagier's representatives, c > 0 or c = 0 < a, the matrix -M = (-a -b; -c -d) has weight zero: at most one of the representatives ±M of a class occurs in (15).

The element

theorem TauCeti.TraceFormulaMatrixModule.abs_le_of_intCast_ne_zero {k : Type u_1} {n : ℤ} [AddGroupWithOne k] {w : Matrix (Fin 2) (Fin 2) ℤ → ℤ} (hw : ∀ (M : Matrix (Fin 2) (Fin 2) ℤ), w M ≠ 0 → PopaZagier.weight M ≠ 0) (A : TraceFormulaMatrix n) (h : ↑(w ↑A) ≠ 0) (i j : Fin 2) : |↑A i j| ≤ 2 * n

An integer weight w that vanishes wherever Popa–Zagier's weight does, cast to an additive group with one k, satisfies the bound hypothesis of ofWeight with B = 2 n: a determinant-n matrix whose weight is nonzero in k has entries at most 2 n in absolute value (Popa–Zagier, Lemma 4(a)).

noncomputable def TauCeti.TraceFormulaMatrixModule.popaZagierElement (k : Type u_1) [DivisionRing k] (n : ℤ) : MonoidAlgebra k (TraceFormulaMatrixModule n)

Popa–Zagier's explicit Hecke element of k[ℳₙ] (written Tₙ with a tilde in their paper), their eq. (15): T₁ - T₂ - T₃ - T₄ (see TauCeti.PopaZagier.weight), that is, 12⁻¹ times the element with the integer weights. Its coefficients are given by coeff_popaZagierElement_mk. It is Popa–Zagier's element when 12 ≠ 0 in k, that is, when k has characteristic other than 2 and 3; otherwise it is 0.

theorem TauCeti.TraceFormulaMatrixModule.popaZagierElement_eq_inv_smul_ofWeight {k : Type u_1} {n : ℤ} [DivisionRing k] : popaZagierElement k n = 12⁻¹ • ofWeight n (fun (M : Matrix (Fin 2) (Fin 2) ℤ) => ↑(PopaZagier.weight M)) (2 * n) ⋯

Popa–Zagier's element is 12⁻¹ times the element with the integer weights.

@[simp]

theorem TauCeti.TraceFormulaMatrixModule.coeff_popaZagierElement_mk {k : Type u_1} {n : ℤ} [DivisionRing k] (A : TraceFormulaMatrix n) : (popaZagierElement k n).coeff (mk A) = (↑(PopaZagier.weight ↑A) + ↑(PopaZagier.weight (-↑A))) / 12

The coefficient of the class of A in Popa–Zagier's element is (weight A + weight (-A)) / 12.

theorem TauCeti.TraceFormulaMatrixModule.coeff_popaZagierElement_mk_of_pos {k : Type u_1} {n : ℤ} [DivisionRing k] (A : TraceFormulaMatrix n) (hA : 0 < ↑A 1 0 ∨ ↑A 1 0 = 0 ∧ 0 < ↑A 0 0) : (popaZagierElement k n).coeff (mk A) = ↑(PopaZagier.weight ↑A) / 12

With Popa–Zagier's representatives, c > 0 or c = 0 < a, the coefficient of the class of A = (a b; c d) is weight A / 12.