The weight-k slash action of GL(2, ℚ)

Mathlib defines the slash action of GL(2, ℝ) on ℍ → ℂ and specialises it to SL(2, ℤ) through monoidHomSlashAction. The Hecke operators need the group in between: their coset representatives are rational matrices of positive determinant — Δ₀(N) is a submonoid of GL(2, ℚ) — and they are slashed against functions invariant under an integral congruence subgroup.

This file supplies that action, by the same mechanism Mathlib uses for SL(2, ℤ): transport along the entrywise map GL(2, ℚ) →* GL(2, ℝ). It is a scoped instance, so a module that does not want f ∣[k] g to elaborate at rational g simply does not open the scope.

f ∣[k] g is the real slash at the mapped matrix definitionally, so every GL(2, ℝ) lemma applies after rewriting with rat_slash; the point of the instance is that consumers need not insert the coercion by hand.

The SLnZ 2 / 𝒮ℒ bridge

SlashInvariantForm and friends are indexed by subgroups of GL(2, ℝ), while the Hecke development works at SLnZ 2 ≤ GL(2, ℚ) under the rational action defined here. Both SLnZ 2 and 𝒮ℒ are ranges of mapGL out of the same SL₂(ℤ), so mathlib's Matrix.SpecialLinearGroup.map_mapGL relates them directly and the two membership directions are corollaries of it. slash_eq_of_mem_SLnZ is the form consumers want: real invariance under 𝒮ℒ gives rational invariance under SLnZ 2.

The file also carries the rational forms of mathlib's two behaviour-at-i∞ slash lemmas, in the UpperHalfPlane namespace: they belong beside rat_slash, which is the bridge their proofs cross, rather than in any module about particular matrices.

Main results

• ModularForm.rat_slash: the rational action is the real one at the mapped matrix.
• SlashInvariantFormClass.slash_eq_of_mem_SLnZ: a form invariant under 𝒮ℒ is fixed by the rational slash action of every element of SLnZ 2.
• ModularForm.rat_slash_def_of_det_pos, ModularForm.rat_slash_apply_of_det_pos: the expanded formula at positive determinant, free of the σ twist.
• ModularForm.det_map_ratCast_pos: positivity of the determinant survives the embedding.
• ModularForm.rat_smul_slash_of_det_pos: scalars pass through the slash of a positive-determinant rational matrix, with no σ twist.
• ModularForm.map_ratCast_mem_SL, ModularForm.exists_mem_SLnZ_of_mem_SL: the two directions of the SLnZ 2 / 𝒮ℒ correspondence.
• ModularForm.rat_slash_mapGL: the rational slash at mapGL ℚ σ is the real slash at mapGL ℝ σ, and ModularForm.slash_eq_of_mem_map_mapGL, ModularForm.slash_eq_of_mem_map_mapGL_real: the two directions of slash-invariance under the images of a subgroup G ≤ SL₂(ℤ) in GL(2, ℚ) and in GL(2, ℝ), together with ModularForm.map_mapGL_le_glpos.
• ModularForm.slash_eq_of_mem_SLnZ: real slash-invariance under 𝒮ℒ gives rational slash-invariance under SLnZ 2.
• UpperHalfPlane.IsBoundedAtImInfty.rat_slash, UpperHalfPlane.IsZeroAtImInfty.rat_slash: the rational forms of mathlib's .slash lemmas — boundedness and vanishing at i∞ survive a rational slash whose matrix has vanishing (1, 0) entry.

Provenance

Ported from the AINTLIB LeanModularForms project (LeanModularForms/HeckeRIngs/GL2/HeckeAction.lean, commit 2baa76f742bdb4fb8ee323fabba41203bd390e08, Apache-2.0, Chris Birkbeck): the SlashAction ℤ (GL (Fin 2) ℚ) (ℍ → ℂ) instance built by monoidHomSlashAction, and the scalar-pull-through step inside its heckeSlash_smul. AINTLIB names the embedding glMap; here it is spelled out as Matrix.GeneralLinearGroup.map (algebraMap ℚ ℝ) at each use rather than abbreviated, so there is no corresponding declaration. The scalar lemma is stated here at the SMul/IsScalarTower generality of Mathlib's ModularForm.SL_smul_slash rather than AINTLIB's c : ℂ.

The SLnZ 2 / 𝒮ℒ bridge corresponds to AINTLIB's glMap_mem_SL and mem_SL_exists_H (same file). AINTLIB's glMap_mapGL_eq has no counterpart: mathlib's Matrix.SpecialLinearGroup.map_mapGL already states it for an arbitrary scalar tower.

References

• G. Shimura, Introduction to the arithmetic theory of automorphic functions, Chapter 3.

@[instance_reducible]

noncomputable def ModularForm.ratSlashAction : SlashAction ℤ (GL (Fin 2) ℚ) (UpperHalfPlane → ℂ)

The weight-k slash action of GL(2, ℚ), induced from GL(2, ℝ) along ℚ ↪ ℝ. Scoped, so it is opted into rather than imposed.

Equations

• ModularForm.ratSlashAction = monoidHomSlashAction (Matrix.GeneralLinearGroup.map (algebraMap ℚ ℝ))

theorem ModularForm.rat_slash (k : ℤ) (g : GL (Fin 2) ℚ) (f : UpperHalfPlane → ℂ) : SlashAction.map k g f = SlashAction.map k ((Matrix.GeneralLinearGroup.map (algebraMap ℚ ℝ)) g) f

The rational slash action is the real one at the mapped matrix. Definitional, but named: it is how every GL(2, ℝ) lemma is brought to bear on a rational slash.

The three lemmas here mirror Mathlib's integral trio exactly, including the absence of a _def suffix on this one: ModularForm.SL_slash is the transport (Mathlib/NumberTheory/ModularForms/SlashActions.lean:155), ModularForm.SL_slash_def the expanded formula (:158) and ModularForm.SL_slash_apply the pointwise one (:162). _def marks the expanded statement in this family, not the transport, so it belongs to rat_slash_def_of_det_pos below.

theorem ModularForm.det_map_ratCast_pos {g : GL (Fin 2) ℚ} (hg : 0 < (↑g).det) : 0 < (↑((Matrix.GeneralLinearGroup.map (algebraMap ℚ ℝ)) g)).det

A rational matrix of positive determinant maps to a real one of positive determinant. Stated with Matrix.det, the form UpperHalfPlane.σ_eq_refl_of_det_pos consumes.

theorem ModularForm.rat_slash_def_of_det_pos (k : ℤ) {g : GL (Fin 2) ℚ} (hg : 0 < (↑g).det) (f : UpperHalfPlane → ℂ) : SlashAction.map k g f = fun (τ : UpperHalfPlane) => f ((Matrix.GeneralLinearGroup.map (algebraMap ℚ ℝ)) g • τ) * ↑|↑(Matrix.GeneralLinearGroup.det ((Matrix.GeneralLinearGroup.map (algebraMap ℚ ℝ)) g))| ^ (k - 1) * UpperHalfPlane.denom ((Matrix.GeneralLinearGroup.map (algebraMap ℚ ℝ)) g) ↑τ ^ (-k)

The expanded formula for a positive-determinant rational slash, with no σ twist:

f ∣[k] g = fun τ ↦ f (ĝ • τ) * |det ĝ| ^ (k - 1) * denom ĝ τ ^ (-k),

where ĝ abbreviates Matrix.GeneralLinearGroup.map (algebraMap ℚ ℝ) g, the real image of g. The distinction is not cosmetic: g : GL (Fin 2) ℚ does not act on ℍ at all, and denom is likewise only defined at the real matrix, so every occurrence in the statement below is at ĝ.

Mathlib's ModularForm.slash_def carries σ g around the value of f, which is complex conjugation on the negative-determinant branch. This is the analogue of ModularForm.SL_slash_def, which drops the twist because det = 1; here positivity is the hypothesis that does it.

theorem ModularForm.rat_slash_apply_of_det_pos (k : ℤ) {g : GL (Fin 2) ℚ} (hg : 0 < (↑g).det) (f : UpperHalfPlane → ℂ) (τ : UpperHalfPlane) : SlashAction.map k g f τ = f ((Matrix.GeneralLinearGroup.map (algebraMap ℚ ℝ)) g • τ) * ↑|↑(Matrix.GeneralLinearGroup.det ((Matrix.GeneralLinearGroup.map (algebraMap ℚ ℝ)) g))| ^ (k - 1) * UpperHalfPlane.denom ((Matrix.GeneralLinearGroup.map (algebraMap ℚ ℝ)) g) ↑τ ^ (-k)

The pointwise form of rat_slash_def_of_det_pos, matching ModularForm.SL_slash_apply.

@[simp]

theorem ModularForm.rat_smul_slash_of_det_pos {α : Type u_1} [SMul α ℂ] [IsScalarTower α ℂ ℂ] (k : ℤ) {g : GL (Fin 2) ℚ} (hg : 0 < (↑g).det) (f : UpperHalfPlane → ℂ) (c : α) : SlashAction.map k g (c • f) = c • SlashAction.map k g f

Scalars pass through the slash of a positive-determinant rational matrix. Mathlib's ModularForm.smul_slash carries the twist σ A c, which is complex conjugation when the determinant is negative; on the positive branch σ is the identity (UpperHalfPlane.σ_eq_refl_of_det_pos) and the scalar simply commutes.

This is what makes a Hecke operator ℂ-linear: it is a sum of slashes by representatives of positive determinant. The scalar generality matches ModularForm.SL_smul_slash, the same statement for the integral action.

theorem ModularForm.map_ratCast_mem_SL {δ : GL (Fin 2) ℚ} (hδ : δ ∈ HeckeRing.GLn.SLnZ 2) : (Matrix.GeneralLinearGroup.map (algebraMap ℚ ℝ)) δ ∈ (Matrix.SpecialLinearGroup.mapGL ℝ).range

An element of SL₂(ℤ) ≤ GL(2, ℚ) maps into 𝒮ℒ.

theorem ModularForm.exists_mem_SLnZ_of_mem_SL {γ : GL (Fin 2) ℝ} (hγ : γ ∈ (Matrix.SpecialLinearGroup.mapGL ℝ).range) : ∃ δ ∈ HeckeRing.GLn.SLnZ 2, (Matrix.GeneralLinearGroup.map (algebraMap ℚ ℝ)) δ = γ

Every element of 𝒮ℒ is the image of one of SLnZ 2.

theorem ModularForm.slash_eq_of_mem_SLnZ (k : ℤ) {f : UpperHalfPlane → ℂ} (hf : ∀ γ ∈ (Matrix.SpecialLinearGroup.mapGL ℝ).range, SlashAction.map k γ f = f) {δ : GL (Fin 2) ℚ} (hδ : δ ∈ HeckeRing.GLn.SLnZ 2) : SlashAction.map k δ f = f

Real slash-invariance under 𝒮ℒ gives rational slash-invariance under SLnZ 2.

theorem ModularForm.rat_slash_mapGL (k : ℤ) (f : UpperHalfPlane → ℂ) (σ : Matrix.SpecialLinearGroup (Fin 2) ℤ) : SlashAction.map k ((Matrix.SpecialLinearGroup.mapGL ℚ) σ) f = SlashAction.map k ((Matrix.SpecialLinearGroup.mapGL ℝ) σ) f

The ℚ/ℝ bridge for the slash by an integral matrix: the rational action at mapGL ℚ σ is the real action at mapGL ℝ σ. Both are ranges of mapGL out of the same SL(2, ℤ), and mathlib's Matrix.SpecialLinearGroup.map_mapGL relates them along ℤ → ℚ → ℝ.

This is the one lemma needed to state a hypothesis rationally and consume it at a level G.map (mapGL ℝ), or the other way about.

theorem ModularForm.slash_eq_of_mem_map_mapGL {k : ℤ} {G : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {f : UpperHalfPlane → ℂ} (hf : ∀ γ ∈ Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) G, SlashAction.map k γ f = f) {δ : GL (Fin 2) ℚ} (hδ : δ ∈ Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) G) : SlashAction.map k δ f = f

Real slash-invariance under the image of G ≤ SL₂(ℤ) in GL(2, ℝ) — the way a level is spelled for SlashInvariantForm — gives rational slash-invariance under its image in GL(2, ℚ), which is the way the Hecke triples of HeckeRing/GL2/ are spelled. slash_eq_of_mem_SLnZ is the case G = ⊤, written with the ranges SLnZ 2 and 𝒮ℒ that the level-one development uses.

theorem ModularForm.slash_eq_of_mem_map_mapGL_real {k : ℤ} {G : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {f : UpperHalfPlane → ℂ} (hf : ∀ δ ∈ Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) G, SlashAction.map k δ f = f) {γ : GL (Fin 2) ℝ} (hγ : γ ∈ Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) G) : SlashAction.map k γ f = f

The converse of slash_eq_of_mem_map_mapGL: rational slash-invariance under the image of G ≤ SL₂(ℤ) in GL(2, ℚ) gives real slash-invariance under its image in GL(2, ℝ). This is the direction that discharges the slash_action_eq' field of a SlashInvariantForm.

theorem ModularForm.map_mapGL_le_glpos (G : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) : Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) G ≤ Matrix.GLPos (Fin 2) ℚ

The image of G ≤ SL₂(ℤ) in GL(2, ℚ) consists of matrices of determinant 1, so it lies in GLPos. This is the hypothesis det_rightCosetRep_pos asks of the flanking group.

theorem SlashInvariantFormClass.slash_eq_of_mem_map_mapGL {F : Type u_1} {k : ℤ} {G : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} [FunLike F UpperHalfPlane ℂ] [SlashInvariantFormClass F (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) G) k] (f : F) {δ : GL (Fin 2) ℚ} (hδ : δ ∈ Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) G) : SlashAction.map k δ ⇑f = ⇑f

A slash-invariant form is invariant under the rational image of its level. This is ModularForm.slash_eq_of_mem_map_mapGL with the real-invariance hypothesis discharged from the SlashInvariantFormClass instance — the common case of a bundled form. The class is indexed by a subgroup of GL(2, ℝ), so a form of integral level G carries invariance at G.map (mapGL ℝ); this transports it to G.map (mapGL ℚ), the way the Hecke triples of HeckeRing/GL2/ are spelled. Consumers carrying an arbitrary invariance hypothesis instead use ModularForm.slash_eq_of_mem_map_mapGL directly.

theorem UpperHalfPlane.IsBoundedAtImInfty.rat_slash (k : ℤ) {g : GL (Fin 2) ℚ} (hg : ↑g 1 0 = 0) {f : UpperHalfPlane → ℂ} (hf : IsBoundedAtImInfty f) : IsBoundedAtImInfty (SlashAction.map k g f)

The rational form of IsBoundedAtImInfty.slash. Mathlib's lemma is stated for the real slash; the matrix and its hypothesis are given here over ℚ, since Matrix.GeneralLinearGroup.map acts entrywise and so carries g 1 0 = 0 along algebraMap ℚ ℝ.

theorem UpperHalfPlane.IsZeroAtImInfty.rat_slash (k : ℤ) {g : GL (Fin 2) ℚ} (hg : ↑g 1 0 = 0) {f : UpperHalfPlane → ℂ} (hf : IsZeroAtImInfty f) : IsZeroAtImInfty (SlashAction.map k g f)

The rational form of IsZeroAtImInfty.slash.

theorem SlashInvariantFormClass.slash_eq_of_mem_SLnZ {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {k : ℤ} [SlashInvariantFormClass F (Matrix.SpecialLinearGroup.mapGL ℝ).range k] (f : F) (γ : GL (Fin 2) ℚ) (hγ : γ ∈ HeckeRing.GLn.SLnZ 2) : SlashAction.map k γ ⇑f = ⇑f

A form invariant under 𝒮ℒ is fixed by the rational slash action of every element of SLnZ 2.