Determinant-indexed projective matrix modules

For a positive integer n, the Eichler--Selberg trace formula uses integral two-by-two matrices of determinant n, modulo simultaneous sign. This file supplies that carrier and its left, inverse right, and conjugation actions of PSL(2, ℤ). The corresponding SL(2, ℤ) maps on representatives provide the descent to the projective group. These are the input for the group-ring calculations in the Popa--Zagier construction of the trace formula.

Inverse right multiplication is written as a left action. Its representative formula is A ↦ A * g⁻¹, so applying h and then g gives the action of g * h; in GL(2, ℚ), through FixedDetMatrices.toGL, it is right multiplication by g⁻¹ (TauCeti.toGL_traceFormulaMatrixRight). On the upper-triangular representatives FixedDetMatrices.reps n, n ≠ 0, of SL(2, ℤ) \ ℳₙ, it is read as TauCeti.repsRightMul, the representative of the coset of A g⁻¹; this is injective on the representatives (TauCeti.repsRightMul_injOn), so it permutes the cosets. It preserves the primitive representatives FixedDetMatrices.primitiveReps n and permutes them (TauCeti.image_repsRightMul_primitiveReps).

The right and conjugation actions are also MulAction instances, of PSL(2, ℤ)ᵐᵒᵖ and of ConjAct PSL(2, ℤ). With open scoped RightActions, x <• g, that is MulOpposite.op g • x, is Popa--Zagier's product M · g, right multiplication by g itself; it equals x.rightPSL g⁻¹. Conjugation ConjAct.toConjAct g • x equals g • x <• g⁻¹.

For n ≠ 0 the left action of PSL(2, ℤ) is free (TauCeti.TraceFormulaMatrixModule.isCancelSMul): a matrix of nonzero determinant is cancellable, so g A = ±A forces g = ±1 (TauCeti.TraceFormulaMatrixModule.eq_one_or_eq_neg_one_of_smul_eq). Likewise A g = ±A forces g = ±1 (TauCeti.TraceFormulaMatrixModule.eq_one_or_eq_neg_one_of_op_smul_eq), so the right action is free (TauCeti.TraceFormulaMatrixModule.isCancelSMul_mulOpposite).

Elements of the group ring k[ℳₙ] are given by weights on integral matrices: TauCeti.TraceFormulaMatrixModule.ofWeight n w B hw, over any semiring k, gives the class of A the coefficient w A + w (-A) (TauCeti.TraceFormulaMatrixModule.coeff_ofWeight_mk), a bound B on the entries of the determinant-n matrices of nonzero weight making the support finite. Its right coset sums are the sums of w over the matrices in the coset (TauCeti.TraceFormulaMatrixModule.mapDomain_orbitRel_mk_coeff_ofWeight). Conversely, a sign-invariant function f of determinant-n matrices extends linearly to k[ℳₙ] (TauCeti.TraceFormulaMatrixModule.linearLift), sending ∑ c_M M to ∑ c_M f 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, Section 1.

The projective determinant fibre

@[reducible, inline]

abbrev TauCeti.TraceFormulaMatrix (n : ℤ) : Type

Integral two-by-two matrices of determinant n.

def TauCeti.TraceFormulaMatrix.diagonal {n : ℤ} (d₀ d₁ : ℤ) (h : d₀ * d₁ = n) : TraceFormulaMatrix n

The diagonal matrix diag(d₀, d₁), as a matrix of determinant n = d₀ d₁.

@[simp]

theorem TauCeti.TraceFormulaMatrix.val_diagonal {n : ℤ} (d₀ d₁ : ℤ) (h : d₀ * d₁ = n) : ↑(diagonal d₀ d₁ h) = !![d₀, 0; 0, d₁]

The underlying matrix of TraceFormulaMatrix.diagonal d₀ d₁ h is diag(d₀, d₁).

@[instance_reducible]

instance TauCeti.instNegTraceFormulaMatrix (n : ℤ) : Neg (TraceFormulaMatrix n)

@[simp]

theorem TauCeti.TraceFormulaMatrix.val_neg {n : ℤ} (A : TraceFormulaMatrix n) : ↑(-A) = -↑A

Negation of a determinant fibre is computed on its underlying matrix.

@[instance_reducible]

instance TauCeti.instInvolutiveNegTraceFormulaMatrix (n : ℤ) : InvolutiveNeg (TraceFormulaMatrix n)

@[instance_reducible]

instance TauCeti.instSetoidTraceFormulaMatrix (n : ℤ) : Setoid (TraceFormulaMatrix n)

Two determinant-n matrices define the same projective matrix when they differ by sign.

@[reducible, inline]

abbrev TauCeti.TraceFormulaMatrixModule (n : ℤ) : Type

The projective determinant-n matrix module ℳₙ: matrices modulo simultaneous sign.

def TauCeti.TraceFormulaMatrixModule.mk {n : ℤ} (A : TraceFormulaMatrix n) : TraceFormulaMatrixModule n

The projective class of a determinant-n matrix.

@[simp]

theorem TauCeti.TraceFormulaMatrixModule.mk_neg {n : ℤ} (A : TraceFormulaMatrix n) : mk (-A) = mk A

Passing to the projective matrix module identifies a matrix with its negative.

@[simp]

theorem TauCeti.TraceFormulaMatrixModule.lift_mk {n : ℤ} {β : Sort u_1} (f : TraceFormulaMatrix n → β) (h : ∀ (A B : TraceFormulaMatrix n), A ≈ B → f A = f B) (A : TraceFormulaMatrix n) : Quotient.lift f h (mk A) = f A

A sign-invariant function of determinant-n matrices, descended to ℳₙ, takes the class of A to its value at A.

@[simp]

theorem TauCeti.TraceFormulaMatrixModule.mk_eq_iff {n : ℤ} {A B : TraceFormulaMatrix n} : mk A = mk B ↔ A = B ∨ A = -B

Two representatives of ℳₙ agree exactly when they are equal up to simultaneous sign.

theorem TauCeti.TraceFormulaMatrixModule.induction {n : ℤ} {p : TraceFormulaMatrixModule n → Prop} (h : ∀ (A : TraceFormulaMatrix n), p (mk A)) (x : TraceFormulaMatrixModule n) : p x

To prove a property of every projective determinant matrix, it suffices to prove it on representatives.

theorem TauCeti.TraceFormulaMatrixModule.mk_surjective {n : ℤ} : Function.Surjective mk

Every projective determinant matrix has a determinant-fibre representative.

The three modular-group actions

def TauCeti.traceFormulaMatrixRight {n : ℤ} (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) (A : TraceFormulaMatrix n) : TraceFormulaMatrix n

Right multiplication by the inverse of an integral determinant-one matrix.

@[simp]

theorem TauCeti.val_traceFormulaMatrixRight {n : ℤ} (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) (A : TraceFormulaMatrix n) : ↑(traceFormulaMatrixRight g A) = ↑A * ↑g⁻¹

Inverse right multiplication is computed on the underlying matrix.

theorem TauCeti.toGL_traceFormulaMatrixRight {n : ℤ} (hn : n ≠ 0) (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) (A : TraceFormulaMatrix n) : FixedDetMatrices.toGL hn (traceFormulaMatrixRight g A) = FixedDetMatrices.toGL hn A * (Matrix.SpecialLinearGroup.mapGL ℚ) g⁻¹

For n ≠ 0, inverse right multiplication becomes right multiplication by the image of g⁻¹ in GL(2, ℚ).

theorem TauCeti.toGLReal_traceFormulaMatrixRight {n : ℤ} (hn : n ≠ 0) (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) (A : TraceFormulaMatrix n) : FixedDetMatrices.toGLReal hn (traceFormulaMatrixRight g A) = FixedDetMatrices.toGLReal hn A * (Matrix.SpecialLinearGroup.mapGL ℝ) g⁻¹

For n ≠ 0, inverse right multiplication becomes right multiplication by the image of g⁻¹ in GL(2, ℝ).

theorem TauCeti.isPrimitive_traceFormulaMatrixRight_iff {n : ℤ} (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) (A : TraceFormulaMatrix n) : IsPrimitive ↑(traceFormulaMatrixRight g A) ↔ IsPrimitive ↑A

Inverse right multiplication preserves and reflects primitivity.

Right multiplication on the upper-triangular representatives

noncomputable def TauCeti.repsRightMulFactor {n : ℤ} (hn : n ≠ 0) (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) (A : TraceFormulaMatrix n) : Matrix.SpecialLinearGroup (Fin 2) ℤ

A matrix of SL(2, ℤ) moving the right translate A g⁻¹ back into FixedDetMatrices.reps n.

noncomputable def TauCeti.repsRightMul {n : ℤ} (hn : n ≠ 0) (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) (A : TraceFormulaMatrix n) : TraceFormulaMatrix n

Right multiplication by g⁻¹ on SL(2, ℤ) \ ℳₙ, read on the representatives FixedDetMatrices.reps n: the representative of the coset SL(2, ℤ) A g⁻¹.

theorem TauCeti.repsRightMul_def {n : ℤ} (hn : n ≠ 0) (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) (A : TraceFormulaMatrix n) : repsRightMul hn g A = repsRightMulFactor hn g A • traceFormulaMatrixRight g A

The defining equation of repsRightMul: the right translate A g⁻¹ moved by repsRightMulFactor.

theorem TauCeti.repsRightMul_mem_reps {n : ℤ} (hn : n ≠ 0) (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) (A : TraceFormulaMatrix n) : repsRightMul hn g A ∈ FixedDetMatrices.reps n

The right translate repsRightMul hn g A is a representative.

theorem TauCeti.toGL_repsRightMul {n : ℤ} (hn : n ≠ 0) (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) (A : TraceFormulaMatrix n) : FixedDetMatrices.toGL hn (repsRightMul hn g A) = (Matrix.SpecialLinearGroup.mapGL ℚ) (repsRightMulFactor hn g A) * (FixedDetMatrices.toGL hn A * (Matrix.SpecialLinearGroup.mapGL ℚ) g⁻¹)

In GL(2, ℚ), repsRightMul hn g A is A g⁻¹ moved on the left by repsRightMulFactor hn g A.

theorem TauCeti.toGLReal_repsRightMul {n : ℤ} (hn : n ≠ 0) (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) (A : TraceFormulaMatrix n) : FixedDetMatrices.toGLReal hn (repsRightMul hn g A) = (Matrix.SpecialLinearGroup.mapGL ℝ) (repsRightMulFactor hn g A) * (FixedDetMatrices.toGLReal hn A * (Matrix.SpecialLinearGroup.mapGL ℝ) g⁻¹)

In GL(2, ℝ), repsRightMul hn g A is A g⁻¹ moved on the left by repsRightMulFactor hn g A.

theorem TauCeti.repsRightMul_injOn {n : ℤ} (hn : n ≠ 0) (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) : Set.InjOn (repsRightMul hn g) (FixedDetMatrices.reps n)

Right multiplication by g⁻¹ permutes SL(2, ℤ) \ ℳₙ: distinct cosets have distinct right translates.

theorem TauCeti.repsRightMul_mem_primitiveReps {n : ℤ} (hn : n ≠ 0) (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) {A : TraceFormulaMatrix n} (hA : A ∈ FixedDetMatrices.primitiveReps n) : repsRightMul hn g A ∈ FixedDetMatrices.primitiveReps n

Right multiplication by g⁻¹ preserves the primitive representatives.

theorem TauCeti.repsRightMul_injOn_primitiveReps {n : ℤ} (hn : n ≠ 0) (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) : Set.InjOn (repsRightMul hn g) ↑(FixedDetMatrices.primitiveReps n)

Right multiplication by g⁻¹ is injective on the primitive representatives.

theorem TauCeti.image_repsRightMul_primitiveReps {n : ℤ} (hn : n ≠ 0) (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) : Finset.image (repsRightMul hn g) (FixedDetMatrices.primitiveReps n) = FixedDetMatrices.primitiveReps n

Right multiplication by g⁻¹ permutes the SL(2, ℤ)-orbits of primitive matrices: the representatives of the right translates of FixedDetMatrices.primitiveReps n are again all of FixedDetMatrices.primitiveReps n.

theorem TauCeti.toGL_neg_smul {n : ℤ} (hn : n ≠ 0) (A : TraceFormulaMatrix n) (α : OnePoint ℚ) : FixedDetMatrices.toGL hn (-A) • α = FixedDetMatrices.toGL hn A • α

For n ≠ 0, a determinant-n matrix and its negative act in the same way on the cusps ℙ¹(ℚ).

@[instance_reducible]

instance TauCeti.instSMulSpecialLinearGroupFinOfNatNatIntTraceFormulaMatrixModule (n : ℤ) : SMul (Matrix.SpecialLinearGroup (Fin 2) ℤ) (TraceFormulaMatrixModule n)

Left multiplication makes ℳₙ an SL(2, ℤ)-set.

@[instance_reducible]

instance TauCeti.instMulActionSpecialLinearGroupFinOfNatNatIntTraceFormulaMatrixModule (n : ℤ) : MulAction (Matrix.SpecialLinearGroup (Fin 2) ℤ) (TraceFormulaMatrixModule n)

@[simp]

theorem TauCeti.TraceFormulaMatrixModule.smul_mk {n : ℤ} (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) (A : TraceFormulaMatrix n) : g • mk A = mk (g • A)

Left multiplication on a projective class is computed on any representative.

@[simp]

theorem TauCeti.TraceFormulaMatrixModule.neg_one_smul {n : ℤ} (x : TraceFormulaMatrixModule n) : -1 • x = x

The central sign acts trivially on the projective determinant fibre.

@[instance_reducible]

instance TauCeti.instMulActionProjectiveSpecialLinearGroupFinOfNatNatIntTraceFormulaMatrixModule (n : ℤ) : MulAction (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℤ) (TraceFormulaMatrixModule n)

The left action of PSL(2, ℤ) on projective determinant-n matrices.

@[simp]

theorem TauCeti.TraceFormulaMatrixModule.coe_smul {n : ℤ} (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) (x : TraceFormulaMatrixModule n) : ↑g • x = g • x

A projective modular-group element represented by g acts as g.

theorem TauCeti.TraceFormulaMatrixModule.eq_one_or_eq_neg_one_of_smul_eq {n : ℤ} (hn : n ≠ 0) {g : Matrix.SpecialLinearGroup (Fin 2) ℤ} {x : TraceFormulaMatrixModule n} (h : g • x = x) : g = 1 ∨ g = -1

For n ≠ 0, only ±1 in SL(2, ℤ) fixes an element of ℳₙ.

theorem TauCeti.TraceFormulaMatrixModule.isCancelSMul {n : ℤ} (hn : n ≠ 0) : IsCancelSMul (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℤ) (TraceFormulaMatrixModule n)

For n ≠ 0, PSL(2, ℤ) acts freely on ℳₙ.

def TauCeti.TraceFormulaMatrixModule.right {n : ℤ} (x : TraceFormulaMatrixModule n) (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) : TraceFormulaMatrixModule n

The right multiplication action on ℳₙ, expressed as a left action through inversion.

@[simp]

theorem TauCeti.TraceFormulaMatrixModule.right_mk {n : ℤ} (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) (A : TraceFormulaMatrix n) : (mk A).right g = mk (traceFormulaMatrixRight g A)

Inverse right multiplication on a projective class is computed on any representative.

def TauCeti.TraceFormulaMatrixModule.conj {n : ℤ} (x : TraceFormulaMatrixModule n) (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) : TraceFormulaMatrixModule n

The conjugation action on ℳₙ, expressed as a left action by A ↦ g A g⁻¹.

@[simp]

theorem TauCeti.TraceFormulaMatrixModule.conj_mk {n : ℤ} (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) (A : TraceFormulaMatrix n) : (mk A).conj g = mk (g • traceFormulaMatrixRight g A)

Conjugation on a projective class is computed on any representative.

@[simp]

theorem TauCeti.TraceFormulaMatrixModule.right_one {n : ℤ} (x : TraceFormulaMatrixModule n) : x.right 1 = x

Inverse right multiplication fixes ℳₙ at the identity.

@[simp]

theorem TauCeti.TraceFormulaMatrixModule.right_mul {n : ℤ} (g h : Matrix.SpecialLinearGroup (Fin 2) ℤ) (x : TraceFormulaMatrixModule n) : x.right (g * h) = (x.right h).right g

Inverse right multiplication defines a left action.

@[simp]

theorem TauCeti.TraceFormulaMatrixModule.right_inv_right {n : ℤ} (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) (x : TraceFormulaMatrixModule n) : (x.right g).right g⁻¹ = x

Inverse right multiplication by g is cancelled by its inverse.

@[simp]

theorem TauCeti.TraceFormulaMatrixModule.right_right_inv {n : ℤ} (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) (x : TraceFormulaMatrixModule n) : (x.right g⁻¹).right g = x

Inverse right multiplication by the inverse of g is cancelled by g.

@[simp]

theorem TauCeti.TraceFormulaMatrixModule.right_neg_one {n : ℤ} (x : TraceFormulaMatrixModule n) : x.right (-1) = x

The central sign also acts trivially by inverse right multiplication.

def TauCeti.TraceFormulaMatrixModule.rightPSLHom (n : ℤ) : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℤ →* Equiv.Perm (TraceFormulaMatrixModule n)

Inverse right multiplication descends through the central quotient.

def TauCeti.TraceFormulaMatrixModule.rightPSL {n : ℤ} (x : TraceFormulaMatrixModule n) (g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℤ) : TraceFormulaMatrixModule n

Inverse right multiplication by a projective modular-group element.

@[simp]

theorem TauCeti.TraceFormulaMatrixModule.rightPSLHom_apply {n : ℤ} (g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℤ) (x : TraceFormulaMatrixModule n) : ((rightPSLHom n) g) x = x.rightPSL g

The packaged permutation action agrees with inverse right multiplication.

@[simp]

theorem TauCeti.TraceFormulaMatrixModule.rightPSL_coe {n : ℤ} (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) (x : TraceFormulaMatrixModule n) : x.rightPSL ↑g = x.right g

A representative acts by inverse right multiplication.

@[simp]

theorem TauCeti.TraceFormulaMatrixModule.rightPSL_one {n : ℤ} (x : TraceFormulaMatrixModule n) : x.rightPSL 1 = x

The identity acts trivially by inverse right multiplication.

@[simp]

theorem TauCeti.TraceFormulaMatrixModule.rightPSL_mul {n : ℤ} (g h : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℤ) (x : TraceFormulaMatrixModule n) : x.rightPSL (g * h) = (x.rightPSL h).rightPSL g

Inverse right multiplication gives a left action of PSL(2, ℤ).

@[simp]

theorem TauCeti.TraceFormulaMatrixModule.rightPSL_inv_rightPSL {n : ℤ} (g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℤ) (x : TraceFormulaMatrixModule n) : (x.rightPSL g).rightPSL g⁻¹ = x

Projective inverse right multiplication by g is cancelled by its inverse.

@[simp]

theorem TauCeti.TraceFormulaMatrixModule.rightPSL_rightPSL_inv {n : ℤ} (g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℤ) (x : TraceFormulaMatrixModule n) : (x.rightPSL g⁻¹).rightPSL g = x

Projective inverse right multiplication by the inverse of g is cancelled by g.

@[simp]

theorem TauCeti.TraceFormulaMatrixModule.right_smul {n : ℤ} (g h : Matrix.SpecialLinearGroup (Fin 2) ℤ) (x : TraceFormulaMatrixModule n) : (g • x).right h = g • x.right h

Left multiplication commutes with the right modular-group action on ℳₙ.

@[simp]

theorem TauCeti.TraceFormulaMatrixModule.rightPSL_smul {n : ℤ} (g h : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℤ) (x : TraceFormulaMatrixModule n) : (g • x).rightPSL h = g • x.rightPSL h

Left multiplication commutes with inverse right multiplication on projective classes.

def TauCeti.TraceFormulaMatrixModule.conjPSL {n : ℤ} (x : TraceFormulaMatrixModule n) (g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℤ) : TraceFormulaMatrixModule n

Conjugation of projective determinant-n matrices by PSL(2, ℤ).

@[simp]

theorem TauCeti.TraceFormulaMatrixModule.conjPSL_coe {n : ℤ} (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) (x : TraceFormulaMatrixModule n) : x.conjPSL ↑g = x.conj g

A representative conjugates by A ↦ g A g⁻¹.

@[simp]

theorem TauCeti.TraceFormulaMatrixModule.conjPSL_one {n : ℤ} (x : TraceFormulaMatrixModule n) : x.conjPSL 1 = x

Conjugation fixes every class at the identity.

@[simp]

theorem TauCeti.TraceFormulaMatrixModule.conjPSL_mul {n : ℤ} (g h : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℤ) (x : TraceFormulaMatrixModule n) : x.conjPSL (g * h) = (x.conjPSL h).conjPSL g

Conjugation by a product composes in left-action order.

@[simp]

theorem TauCeti.TraceFormulaMatrixModule.conjPSL_inv_conjPSL {n : ℤ} (g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℤ) (x : TraceFormulaMatrixModule n) : (x.conjPSL g).conjPSL g⁻¹ = x

Projective conjugation by g is cancelled by conjugation by its inverse.

@[simp]

theorem TauCeti.TraceFormulaMatrixModule.conjPSL_conjPSL_inv {n : ℤ} (g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℤ) (x : TraceFormulaMatrixModule n) : (x.conjPSL g⁻¹).conjPSL g = x

Projective conjugation by the inverse of g is cancelled by conjugation by g.

@[simp]

theorem TauCeti.TraceFormulaMatrixModule.conj_one {n : ℤ} (x : TraceFormulaMatrixModule n) : x.conj 1 = x

Conjugation fixes ℳₙ at the identity.

@[simp]

theorem TauCeti.TraceFormulaMatrixModule.conj_mul {n : ℤ} (g h : Matrix.SpecialLinearGroup (Fin 2) ℤ) (x : TraceFormulaMatrixModule n) : x.conj (g * h) = (x.conj h).conj g

Conjugation by a product composes in the usual left-action order.

@[simp]

theorem TauCeti.TraceFormulaMatrixModule.conj_inv_conj {n : ℤ} (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) (x : TraceFormulaMatrixModule n) : (x.conj g).conj g⁻¹ = x

Conjugation by g is cancelled by conjugation by its inverse.

@[simp]

theorem TauCeti.TraceFormulaMatrixModule.conj_conj_inv {n : ℤ} (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) (x : TraceFormulaMatrixModule n) : (x.conj g⁻¹).conj g = x

Conjugation by the inverse of g is cancelled by conjugation by g.

def TauCeti.TraceFormulaMatrixModule.conjPSLHom (n : ℤ) : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℤ →* Equiv.Perm (TraceFormulaMatrixModule n)

Conjugation of ℳₙ by projective modular-group elements, packaged as permutations.

@[simp]

theorem TauCeti.TraceFormulaMatrixModule.conjPSLHom_apply {n : ℤ} (g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℤ) (x : TraceFormulaMatrixModule n) : ((conjPSLHom n) g) x = x.conjPSL g

The packaged conjugation permutation acts by conjPSL.

The right and conjugation actions as MulActions

@[instance_reducible]

instance TauCeti.TraceFormulaMatrixModule.instMulActionMulOppositePSL (n : ℤ) : MulAction (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℤ)ᵐᵒᵖ (TraceFormulaMatrixModule n)

Right multiplication makes ℳₙ a right PSL(2, ℤ)-set. With open scoped RightActions, x <• g, that is MulOpposite.op g • x, is Popa--Zagier's product M · g: the class of A * g for a representative A of x. It is inverse right multiplication by g⁻¹, that is x.rightPSL g⁻¹.

theorem TauCeti.TraceFormulaMatrixModule.op_smul_eq_rightPSL_inv {n : ℤ} (g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℤ) (x : TraceFormulaMatrixModule n) : MulOpposite.op g • x = x.rightPSL g⁻¹

Right multiplication by g is inverse right multiplication by g⁻¹.

@[simp]

theorem TauCeti.TraceFormulaMatrixModule.op_smul_mk {n : ℤ} (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) (A : TraceFormulaMatrix n) : MulOpposite.op ↑g • mk A = mk (traceFormulaMatrixRight g⁻¹ A)

Right multiplication by a projective class is computed on any representatives: the class of A times the class of g is the class of A * g.

@[simp]

theorem TauCeti.TraceFormulaMatrixModule.inv_op_smul_mk {n : ℤ} (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) (A : TraceFormulaMatrix n) : (MulOpposite.op ↑g)⁻¹ • mk A = mk (traceFormulaMatrixRight g A)

Right multiplication by the inverse of a projective class is computed on any representatives: the class of A times the inverse of the class of g is the class of A * g⁻¹. This is the form in which simp leaves x <• g⁻¹, via MulOpposite.op_inv.

@[simp]

theorem TauCeti.TraceFormulaMatrixModule.mk_mem_orbit_op_mk_iff {n : ℤ} {A B : TraceFormulaMatrix n} : mk A ∈ MulAction.orbit (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℤ)ᵐᵒᵖ (mk B) ↔ ∃ (g : Matrix.SpecialLinearGroup (Fin 2) ℤ), ↑A = ↑B * ↑g

The class of A lies in the right coset of the class of B exactly when A = B g for some g ∈ SL(2, ℤ); the sign ambiguity of the classes is absorbed into g.

theorem TauCeti.TraceFormulaMatrixModule.eq_one_or_eq_neg_one_of_op_smul_eq {n : ℤ} (hn : n ≠ 0) {g : Matrix.SpecialLinearGroup (Fin 2) ℤ} {x : TraceFormulaMatrixModule n} (h : MulOpposite.op ↑g • x = x) : g = 1 ∨ g = -1

For n ≠ 0, only ±1 in SL(2, ℤ) fixes an element of ℳₙ under right multiplication.

theorem TauCeti.TraceFormulaMatrixModule.isCancelSMul_mulOpposite {n : ℤ} (hn : n ≠ 0) : IsCancelSMul (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℤ)ᵐᵒᵖ (TraceFormulaMatrixModule n)

For n ≠ 0, PSL(2, ℤ) acts freely on ℳₙ by right multiplication.

instance TauCeti.TraceFormulaMatrixModule.instSMulCommClassPSL (n : ℤ) : SMulCommClass (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℤ) (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℤ)ᵐᵒᵖ (TraceFormulaMatrixModule n)

Left and right multiplication on ℳₙ commute.

instance TauCeti.TraceFormulaMatrixModule.instSMulCommClassSL (n : ℤ) : SMulCommClass (Matrix.SpecialLinearGroup (Fin 2) ℤ) (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℤ)ᵐᵒᵖ (TraceFormulaMatrixModule n)

Left multiplication by a determinant-one matrix commutes with right multiplication on ℳₙ.

@[instance_reducible]

instance TauCeti.TraceFormulaMatrixModule.instMulActionConjActPSL (n : ℤ) : MulAction (ConjAct (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℤ)) (TraceFormulaMatrixModule n)

Conjugation makes ℳₙ a ConjAct PSL(2, ℤ)-set: ConjAct.toConjAct g sends the class of A to the class of g * A * g⁻¹, that is x to g • x <• g⁻¹.

theorem TauCeti.TraceFormulaMatrixModule.toConjAct_smul_eq_conjPSL {n : ℤ} (g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℤ) (x : TraceFormulaMatrixModule n) : ConjAct.toConjAct g • x = x.conjPSL g

The conjugation action of ConjAct PSL(2, ℤ) is conjPSL.

@[simp]

theorem TauCeti.TraceFormulaMatrixModule.toConjAct_smul {n : ℤ} (g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℤ) (x : TraceFormulaMatrixModule n) : ConjAct.toConjAct g • x = g • MulOpposite.op g⁻¹ • x

Conjugation by g is left multiplication by g and right multiplication by g⁻¹.

Elements given by weights

noncomputable def TauCeti.TraceFormulaMatrixModule.ofWeight {k : Type u_1} [Semiring k] (n : ℤ) (w : Matrix (Fin 2) (Fin 2) ℤ → k) (B : ℤ) (hw : ∀ (A : TraceFormulaMatrix n), w ↑A ≠ 0 → ∀ (i j : Fin 2), |↑A i j| ≤ B) : MonoidAlgebra k (TraceFormulaMatrixModule n)

The element of k[ℳₙ] in which the class of A has coefficient w A + w (-A), for a weight w on integral matrices that vanishes on every determinant-n matrix with an entry larger than B in absolute value. Its coefficients are given by coeff_ofWeight_mk.

@[simp]

theorem TauCeti.TraceFormulaMatrixModule.coeff_ofWeight_mk {k : Type u_1} [Semiring k] {n : ℤ} (w : Matrix (Fin 2) (Fin 2) ℤ → k) (B : ℤ) (hw : ∀ (A : TraceFormulaMatrix n), w ↑A ≠ 0 → ∀ (i j : Fin 2), |↑A i j| ≤ B) (A : TraceFormulaMatrix n) : (ofWeight n w B hw).coeff (mk A) = w ↑A + w (-↑A)

The coefficient of the class of A in ofWeight n w B hw is w A + w (-A).

theorem TauCeti.TraceFormulaMatrixModule.ofWeight_eq_sum {k : Type u_1} [Semiring k] {n : ℤ} (hn : n ≠ 0) (w : Matrix (Fin 2) (Fin 2) ℤ → k) (B : ℤ) (hw : ∀ (A : TraceFormulaMatrix n), w ↑A ≠ 0 → ∀ (i j : Fin 2), |↑A i j| ≤ B) (s : Finset (TraceFormulaMatrix n)) (hs : ∀ (A : TraceFormulaMatrix n), w ↑A ≠ 0 → A ∈ s) : ofWeight n w B hw = ∑ A ∈ s, MonoidAlgebra.single (mk A) (w ↑A)

An element given by a weight is the sum of the weighted projective classes over any finite set containing every determinant-n matrix of nonzero weight. The weights of the two representatives of a projective class add, with no factor of two.

theorem TauCeti.TraceFormulaMatrixModule.mapDomain_orbitRel_mk_coeff_ofWeight {k : Type u_1} [Semiring k] {n : ℤ} (hn : n ≠ 0) (w : Matrix (Fin 2) (Fin 2) ℤ → k) (B : ℤ) (hw : ∀ (A : TraceFormulaMatrix n), w ↑A ≠ 0 → ∀ (i j : Fin 2), |↑A i j| ≤ B) (x : TraceFormulaMatrixModule n) : (Finsupp.mapDomain (Quotient.mk (MulAction.orbitRel (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℤ)ᵐᵒᵖ (TraceFormulaMatrixModule n))) (ofWeight n w B hw).coeff) ⟦x⟧ = ∑ᶠ (A : TraceFormulaMatrix n) (_ : A ∈ mk ⁻¹' MulAction.orbit (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℤ)ᵐᵒᵖ x), w ↑A

The right coset sums of an element given by a weight: for n ≠ 0, the sum of the coefficients of ofWeight n w B hw over the right coset x Γ is the sum of w over the determinant-n matrices whose class lies in x Γ. Each class ±A contributes w A + w (-A), so both representatives of a class are counted.

Linear extension of sign-invariant functions

noncomputable def TauCeti.TraceFormulaMatrixModule.linearLift {k : Type u_1} [Semiring k] {n : ℤ} {M : Type u_2} [AddCommMonoid M] [Module k M] (f : TraceFormulaMatrix n → M) (hf : ∀ (A : TraceFormulaMatrix n), f (-A) = f A) : MonoidAlgebra k (TraceFormulaMatrixModule n) →ₗ[k] M

The linear extension ∑ c_M M ↦ ∑ c_M f M to k[ℳₙ] of a function f of determinant-n matrices that takes the same value on A and -A.

@[simp]

theorem TauCeti.TraceFormulaMatrixModule.linearLift_single {k : Type u_1} [Semiring k] {n : ℤ} {M : Type u_2} [AddCommMonoid M] [Module k M] (f : TraceFormulaMatrix n → M) (hf : ∀ (A : TraceFormulaMatrix n), f (-A) = f A) (A : TraceFormulaMatrix n) (c : k) : (linearLift f hf) (MonoidAlgebra.single (mk A) c) = c • f A

A basis element c • [A] is sent to c • f A.