Rational matrices carry cusps to cusps

IsCusp.smul moves a cusp of Γ to a cusp of the conjugate ConjAct.toConjAct g • Γ, and for a rational g that conjugate is again arithmetic (Subgroup.IsArithmetic.conj). Since every arithmetic subgroup has the same cusps as 𝒮ℒ (Subgroup.IsArithmetic.isCusp_iff_isCusp_SL2Z), the cusp transports straight back to Γ.

This is what the Hecke operators need. A rational representative need not lie in Γ at all, so IsCusp.smul_of_mem does not apply to it, and the general IsCusp.smul only places the image cusp in a conjugate subgroup. What repairs that is arithmeticity of the conjugate, as above; nothing is asked of the determinant beyond invertibility.

Main results

• IsCusp.smul_map_ratCast: if c is a cusp of an arithmetic Γ then so is g • c, for any g : GL (Fin 2) ℚ pushed forward to ℝ.

Provenance

The need for this lemma, and its role as the cusp-stability step under a Hecke representative, come from the AINTLIB LeanModularForms project (Chris Birkbeck, Apache-2.0), LeanModularForms/HeckeRIngs/GL2/AdjointTheory.lean at commit 2baa76f742bdb4fb8ee323fabba41203bd390e08, where it is packaged as glMap_smul_isCusp_Gamma1.

The proof is not ported: that declaration is specific to Γ₁(N), whereas this one is stated for an arbitrary arithmetic subgroup and is a three-line composition of mathlib's IsCusp.smul, Subgroup.IsArithmetic.conj and Subgroup.IsArithmetic.isCusp_iff_isCusp_SL2Z, none of which the source uses.

theorem IsCusp.smul_map_ratCast {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.IsArithmetic] {c : OnePoint ℝ} (hc : IsCusp c Γ) (g : GL (Fin 2) ℚ) : IsCusp ((Matrix.GeneralLinearGroup.map (algebraMap ℚ ℝ)) g • c) Γ

Rational matrices carry cusps to cusps: a g : GL (Fin 2) ℚ, pushed forward to ℝ, sends a cusp of an arithmetic Γ to a cusp of Γ.