The Fricke operator preserves the old subspace

Let N = d * e * M. The Fricke matrix W_N = !![0, -1; N, 0] moves past the level-raising matrix diag(d, 1) at the cost of exchanging d for the complementary factor e:

diag(d, 1) · W_N = d · (W_M · diag(e, 1)),

both sides being !![0, -d; N, 0]. Since the scalar matrix d · I slashes as multiplication by d ^ (k - 2), the Fricke operator carries a level-raise V_d f of a form f of level M to a multiple of the level-raise V_e (W_M f), where W_M is the Fricke operator of the lower level:

W_N (V_d f) = d⁻¹ · e ^ (k - 1) · V_e (W_M f).

As e * M divides N and M is still a proper divisor of N, the right-hand side is again old. So W_N maps the old subspace S_k(Γ₁(N))ᵒˡᵈ into itself, and, being invertible, onto itself; the same holds for the normalized operator 𝒲_N, a nonzero multiple of W_N. This is the Fricke transport of the degeneracy maps and of the old subspace (Diamond–Shurman §5.6, Miyake §4.6): combined with the Petersson unitarity of 𝒲_N, it makes the new subspace, the Petersson complement of the old one, stable under 𝒲_N.

Main results

• TauCeti.scaleGL_mul_frickeGL: the matrix identity diag(d, 1) · W_N = d · W_M · diag(e, 1).
• TauCeti.slash_scaleGL_slash_frickeGL: its slash form, for an arbitrary function.
• TauCeti.frickeOperator_levelRaise, TauCeti.frickeOperatorCusp_levelRaise, TauCeti.normalizedFrickeOperator_levelRaise, TauCeti.normalizedFrickeOperatorCusp_levelRaise: the Fricke operator, raw and normalized, on modular and on cusp forms, intertwines V_d at level N with V_e at level M.
• TauCeti.frickeOperatorCusp_mem_cuspFormsOld, TauCeti.normalizedFrickeOperatorCusp_mem_cuspFormsOld: the old subspace is stable.
• TauCeti.cuspFormsOld_map_frickeOperatorCusp, TauCeti.cuspFormsOld_map_normalizedFrickeOperatorCusp: the old subspace is carried onto itself.

References

• F. Diamond and J. Shurman, A First Course in Modular Forms, §5.6 and §5.10.
• Miyake, Modular forms, Section 4.6.
• A. O. L. Atkin and J. Lehner, Hecke operators on Γ₀(m), Math. Ann. 185 (1970), 134–160.

Moving the Fricke matrix past a level-raise

theorem TauCeti.scaleGL_mul_frickeGL {M d e N : ℕ} [NeZero M] [NeZero d] [NeZero e] [NeZero N] (h : d * e * M = N) : scaleGL d * frickeGL ℝ N = (Matrix.GeneralLinearGroup.scalar (Fin 2)) (Units.mk0 ↑d ⋯) * (frickeGL ℝ M * scaleGL e)

The Fricke matrix moves past diag(d, 1): for N = d * e * M, diag(d, 1) · W_N = d · (W_M · diag(e, 1)), both sides being !![0, -d; N, 0].

theorem TauCeti.slash_scaleGL_slash_frickeGL {M d e N : ℕ} [NeZero M] [NeZero d] [NeZero e] [NeZero N] (h : d * e * M = N) (k : ℤ) (f : UpperHalfPlane → ℂ) : SlashAction.map k (frickeGL ℝ N) (SlashAction.map k (scaleGL d) f) = ↑d ^ (k - 2) • SlashAction.map k (scaleGL e) (SlashAction.map k (frickeGL ℝ M) f)

Slashing by diag(d, 1) and then by W_N is d ^ (k - 2) times slashing by W_M and then by diag(e, 1), whenever N = d * e * M. This is scaleGL_mul_frickeGL read through the weight-k slash action, for a function not assumed to be a form.

The Fricke operator on a level-raise

theorem TauCeti.frickeOperator_levelRaise {M d e N : ℕ} {k : ℤ} [NeZero M] [NeZero d] [NeZero e] [NeZero N] (h : d * e * M = N) (hd : Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N) ≤ ConjAct.toConjAct (scaleGL d)⁻¹ • Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 M)) (he : Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N) ≤ ConjAct.toConjAct (scaleGL e)⁻¹ • Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 M)) (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 M)) k) : (frickeOperator k) (ModularForm.levelRaise d hd f) = ((↑d)⁻¹ * ↑e ^ (k - 1)) • ModularForm.levelRaise e he ((frickeOperator k) f)

The Fricke operator intertwines the level-raises on modular forms: for N = d * e * M and a modular form f of level M, W_N (V_d f) = d⁻¹ · e ^ (k - 1) · V_e (W_M f), where W_N and W_M are the Fricke operators of levels N and M.

theorem TauCeti.frickeOperatorCusp_levelRaise {M d e N : ℕ} {k : ℤ} [NeZero M] [NeZero d] [NeZero e] [NeZero N] (h : d * e * M = N) (hd : Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N) ≤ ConjAct.toConjAct (scaleGL d)⁻¹ • Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 M)) (he : Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N) ≤ ConjAct.toConjAct (scaleGL e)⁻¹ • Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 M)) (f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 M)) k) : (frickeOperatorCusp k) (CuspForm.levelRaise d hd f) = ((↑d)⁻¹ * ↑e ^ (k - 1)) • CuspForm.levelRaise e he ((frickeOperatorCusp k) f)

The Fricke operator intertwines the level-raises: for N = d * e * M and a cusp form f of level M, W_N (V_d f) = d⁻¹ · e ^ (k - 1) · V_e (W_M f), where W_N and W_M are the Fricke operators of levels N and M.

theorem TauCeti.normalizedFrickeOperator_levelRaise {M d e N : ℕ} {k : ℤ} [NeZero M] [NeZero d] [NeZero e] [NeZero N] (h : d * e * M = N) (hd : Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N) ≤ ConjAct.toConjAct (scaleGL d)⁻¹ • Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 M)) (he : Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N) ≤ ConjAct.toConjAct (scaleGL e)⁻¹ • Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 M)) (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 M)) k) : (normalizedFrickeOperator k) (ModularForm.levelRaise d hd f) = (atkinLehnerNormalizer (d * e) k * (↑d)⁻¹ * ↑e ^ (k - 1)) • ModularForm.levelRaise e he ((normalizedFrickeOperator k) f)

The normalized Fricke operator intertwines the level-raises on modular forms: for N = d * e * M, 𝒲_N (V_d f) = (√(d e)) ^ (2 - k) · d⁻¹ · e ^ (k - 1) · V_e (𝒲_M f).

theorem TauCeti.normalizedFrickeOperatorCusp_levelRaise {M d e N : ℕ} {k : ℤ} [NeZero M] [NeZero d] [NeZero e] [NeZero N] (h : d * e * M = N) (hd : Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N) ≤ ConjAct.toConjAct (scaleGL d)⁻¹ • Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 M)) (he : Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N) ≤ ConjAct.toConjAct (scaleGL e)⁻¹ • Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 M)) (f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 M)) k) : (normalizedFrickeOperatorCusp k) (CuspForm.levelRaise d hd f) = (atkinLehnerNormalizer (d * e) k * (↑d)⁻¹ * ↑e ^ (k - 1)) • CuspForm.levelRaise e he ((normalizedFrickeOperatorCusp k) f)

The normalized Fricke operator intertwines the level-raises: for N = d * e * M, 𝒲_N (V_d f) = (√(d e)) ^ (2 - k) · d⁻¹ · e ^ (k - 1) · V_e (𝒲_M f). The scalar is (e / d) ^ (k / 2); it is written through atkinLehnerNormalizer (d * e) k, the ratio of the normalizers of 𝒲_N and 𝒲_M.

Stability of the old subspace

theorem TauCeti.frickeOperatorCusp_mem_cuspFormsOld {N : ℕ} {k : ℤ} [NeZero N] {f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k} (hf : f ∈ cuspFormsOld N k) : (frickeOperatorCusp k) f ∈ cuspFormsOld N k

The Fricke operator preserves the old subspace: W_N maps S_k(Γ₁(N))ᵒˡᵈ into itself. A level-raise V_d f from a proper divisor level M, with d * M ∣ N, goes to a multiple of V_e (W_M f) for the complementary e = N / (d * M) (frickeOperatorCusp_levelRaise), which is again old.

theorem TauCeti.normalizedFrickeOperatorCusp_mem_cuspFormsOld {N : ℕ} {k : ℤ} [NeZero N] {f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k} (hf : f ∈ cuspFormsOld N k) : (normalizedFrickeOperatorCusp k) f ∈ cuspFormsOld N k

The normalized Fricke operator preserves the old subspace: 𝒲_N maps S_k(Γ₁(N))ᵒˡᵈ into itself, being a scalar multiple of W_N.

theorem TauCeti.cuspFormsOld_map_frickeOperatorCusp (N : ℕ) [NeZero N] (k : ℤ) : Submodule.map (frickeOperatorCusp k) (cuspFormsOld N k) = cuspFormsOld N k

The Fricke operator carries the old subspace onto itself. It maps the old subspace into itself (frickeOperatorCusp_mem_cuspFormsOld), and every old form is (frickeScalar N k)⁻¹ times the image of the old form W_N f, since W_N ∘ W_N = frickeScalar N k • id.

theorem TauCeti.cuspFormsOld_map_normalizedFrickeOperatorCusp (N : ℕ) [NeZero N] (k : ℤ) : Submodule.map (normalizedFrickeOperatorCusp k) (cuspFormsOld N k) = cuspFormsOld N k

The normalized Fricke operator carries the old subspace onto itself: 𝒲_N maps it into itself (normalizedFrickeOperatorCusp_mem_cuspFormsOld), and squares to the unit (-1) ^ k.