The two spellings of M_k(Γ₀(N))

There are two ways to say "modular form of level N with trivial nebentypus": as a modular form for the bare congruence subgroup Γ₀(N), and as an element of the character space M_k(Γ₁(N), χ) of TauCeti.NumberTheory.ModularForms.DiamondOperators for the trivial character χ = 1. The ModularForms roadmap flags the clash and pins its resolution: prove the two isomorphic, then use M_k(Γ₀(N)) as the default spelling and convert to it. This file is that milestone, for modular forms (TauCeti.modFormCharSpaceOneEquiv) and for cusp forms (TauCeti.cuspFormCharSpaceOneEquiv), both stated for N ≠ 0.

Both directions are instances of the generic subgroup-change API of TauCeti.NumberTheory.ModularForms.Basic. Restricting a Γ₀(N)-form to Γ₁(N) (ModularForm.ofLe) is unconditional, and the resulting form has trivial nebentypus because the diamond operators are slashes by elements of Γ₀(N). Conversely, a Γ₁(N)-form with trivial nebentypus is Γ₀(N)-slash invariant by the nebentypus criterion mem_modFormCharSpace_iff_nebentypus, and it is bounded (resp. zero) at every cusp of Γ₀(N) because for N ≠ 0 the groups Γ₀(N) and Γ₁(N) are arithmetic, hence share the cusps of SL(2, ℤ) (Subgroup.IsArithmetic.isCusp_of_isCusp); this is ModularForm.ofSlashInvariant. Both constructions preserve the underlying function ℍ → ℂ, so the resulting bijections are ℂ-linear and conversion in either direction costs nothing: see the coe_…_apply lemmas below.

The hypothesis N ≠ 0 is therefore needed only for that converse direction: the characterisations of trivial nebentypus and the results about restricting a Γ₀(N)-form hold at every level, while the range equalities and the two equivalences assume [NeZero N].

Note what the isomorphism is not: M_k(Γ₁(N), 1) is a Submodule of M_k(Γ₁(N)), so the statement is that a submodule of the level-Γ₁(N) space is linearly equivalent to another space of forms, not an equality of types.

Main definitions

• TauCeti.modFormCharSpaceOneEquiv, TauCeti.cuspFormCharSpaceOneEquiv: for N ≠ 0, the ℂ-linear equivalences M_k(Γ₁(N), 1) ≃ₗ M_k(Γ₀(N)) and S_k(Γ₁(N), 1) ≃ₗ S_k(Γ₀(N)).
• TauCeti.cuspFormTraceGamma0: for N ≠ 0, Mathlib's trace CuspForm.trace from Γ₁(N) to Γ₀(N), as a ℂ-linear map S_k(Γ₁(N)) →ₗ S_k(Γ₀(N)).

Main results

• TauCeti.mem_modFormCharSpace_one_iff, TauCeti.mem_cuspFormCharSpace_one_iff: trivial nebentypus means Γ₀(N)-slash invariance.
• TauCeti.mem_modFormCharSpace_one_iff_diamondOp, TauCeti.mem_cuspFormCharSpace_one_iff_diamondOpCusp: equivalently, being fixed by every diamond operator.
• TauCeti.modFormCharSpace_one_eq_range, TauCeti.cuspFormCharSpace_one_eq_range: for N ≠ 0, the trivial-nebentypus space is the image of the restriction map from level Γ₀(N).
• TauCeti.coe_trace_eq_sum_diamondOpCusp: the trace from Γ₁(N) to Γ₀(N) is the sum of the diamond operators ∑ᵤ ⟨u⟩.
• TauCeti.sum_diamondOpCusp_mem_cuspFormCharSpace_one: a diamond sum along a surjection has trivial nebentypus.
• TauCeti.cuspFormTraceGamma0_ofLe: tracing a restricted Γ₀(N) form multiplies it by #(ZMod N)ˣ.
• TauCeti.cuspFormTraceGamma0_levelRaise: trace commutes with level raising when the lower-level diamond sum comes from a Γ₀ cusp form.

References

• Diamond–Shurman, A first course in modular forms, §5.1

Trivial nebentypus is Γ₀(N)-invariance

theorem TauCeti.mem_modFormCharSpace_one_iff {N : ℕ} {k : ℤ} (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k) : f ∈ modFormCharSpace k 1 ↔ ∀ γ ∈ Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma0 N), SlashAction.map k γ ⇑f = ⇑f

A modular form for Γ₁(N) has trivial nebentypus exactly when it is Γ₀(N)-slash invariant.

theorem TauCeti.mem_cuspFormCharSpace_one_iff {N : ℕ} {k : ℤ} (f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k) : f ∈ cuspFormCharSpace k 1 ↔ ∀ γ ∈ Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma0 N), SlashAction.map k γ ⇑f = ⇑f

A cusp form for Γ₁(N) has trivial nebentypus exactly when it is Γ₀(N)-slash invariant.

theorem TauCeti.mem_modFormCharSpace_one_iff_diamondOp {N : ℕ} {k : ℤ} (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k) : f ∈ modFormCharSpace k 1 ↔ ∀ (d : (ZMod N)ˣ), (diamondOp k d) f = f

Trivial nebentypus means being fixed by every diamond operator.

theorem TauCeti.mem_cuspFormCharSpace_one_iff_diamondOpCusp {N : ℕ} {k : ℤ} (f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k) : f ∈ cuspFormCharSpace k 1 ↔ ∀ (d : (ZMod N)ˣ), (diamondOpCusp k d) f = f

Trivial nebentypus means being fixed by every diamond operator.

theorem TauCeti.sum_diamondOpCusp_mem_cuspFormCharSpace_one {N : ℕ} {k : ℤ} {M : ℕ} [NeZero N] {φ : (ZMod N)ˣ →* (ZMod M)ˣ} (hφ : Function.Surjective ⇑φ) (g : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 M)) k) : ∑ u : (ZMod N)ˣ, (diamondOpCusp k (φ u)) g ∈ cuspFormCharSpace k 1

Summing the diamond operators of level M along a surjection (ZMod N)ˣ → (ZMod M)ˣ gives a form of trivial nebentypus.

Restricting a Γ₀(N)-form to Γ₁(N)

theorem TauCeti.ofLe_mem_modFormCharSpace_one {N : ℕ} {k : ℤ} (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma0 N)) k) : ModularForm.ofLe ⋯ f ∈ modFormCharSpace k 1

Restricted to Γ₁(N), a modular form for Γ₀(N) has trivial nebentypus.

theorem TauCeti.ofLe_mem_cuspFormCharSpace_one {N : ℕ} {k : ℤ} (f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma0 N)) k) : CuspForm.ofLe ⋯ f ∈ cuspFormCharSpace k 1

Restricted to Γ₁(N), a cusp form for Γ₀(N) has trivial nebentypus.

theorem TauCeti.diamondOp_ofLe {N : ℕ} {k : ℤ} (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma0 N)) k) (d : (ZMod N)ˣ) : (diamondOp k d) (ModularForm.ofLe ⋯ f) = ModularForm.ofLe ⋯ f

The diamond operators fix the restriction of a Γ₀(N)-form: they are slashes by elements of Γ₀(N), under which such a form is already invariant.

theorem TauCeti.diamondOpCusp_ofLe {N : ℕ} {k : ℤ} (f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma0 N)) k) (d : (ZMod N)ˣ) : (diamondOpCusp k d) (CuspForm.ofLe ⋯ f) = CuspForm.ofLe ⋯ f

The diamond operators fix the restriction of a Γ₀(N)-cusp form.

theorem TauCeti.modFormCharSpace_one_eq_range {N : ℕ} {k : ℤ} [NeZero N] : modFormCharSpace k 1 = (ModularForm.ofLeₗ ⋯).range

The trivial-nebentypus space is exactly the image of M_k(Γ₀(N)) under restriction.

theorem TauCeti.cuspFormCharSpace_one_eq_range {N : ℕ} {k : ℤ} [NeZero N] : cuspFormCharSpace k 1 = (CuspForm.ofLeₗ ⋯).range

The trivial-nebentypus space is exactly the image of S_k(Γ₀(N)) under restriction.

The isomorphisms

The two equivalences are deliberately not @[expose], so the coe_… lemmas recording that they preserve the underlying function are written (rfl) rather than rfl: the parentheses opt out of exporting the definitional equality, which those lemmas themselves replace downstream.

noncomputable def TauCeti.modFormCharSpaceOneEquiv (N : ℕ) [NeZero N] (k : ℤ) : ↥(modFormCharSpace k 1) ≃ₗ[ℂ] ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma0 N)) k

The two spellings of M_k(Γ₀(N)) agree: the trivial-nebentypus character space M_k(Γ₁(N), 1) is ℂ-linearly isomorphic to the space M_k(Γ₀(N)) of modular forms for the bare congruence subgroup Γ₀(N), by an isomorphism preserving the underlying function on ℍ (coe_modFormCharSpaceOneEquiv_apply).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.coe_modFormCharSpaceOneEquiv_apply {N : ℕ} {k : ℤ} [NeZero N] (f : ↥(modFormCharSpace k 1)) : ⇑((modFormCharSpaceOneEquiv N k) f) = ⇑↑f

modFormCharSpaceOneEquiv does not change the underlying function on ℍ: a trivial-nebentypus form is converted to a Γ₀(N)-form by re-reading it, not by transporting it.

@[simp]

theorem TauCeti.coe_modFormCharSpaceOneEquiv_symm_apply {N : ℕ} {k : ℤ} [NeZero N] (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma0 N)) k) : ↑((modFormCharSpaceOneEquiv N k).symm f) = ModularForm.ofLe ⋯ f

The inverse of modFormCharSpaceOneEquiv is the restriction ModularForm.ofLe of a Γ₀(N)-form to Γ₁(N); in particular it too preserves the underlying function on ℍ.

noncomputable def TauCeti.cuspFormCharSpaceOneEquiv (N : ℕ) [NeZero N] (k : ℤ) : ↥(cuspFormCharSpace k 1) ≃ₗ[ℂ] CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma0 N)) k

The two spellings of S_k(Γ₀(N)) agree: the cusp-form analogue of modFormCharSpaceOneEquiv.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.coe_cuspFormCharSpaceOneEquiv_apply {N : ℕ} {k : ℤ} [NeZero N] (f : ↥(cuspFormCharSpace k 1)) : ⇑((cuspFormCharSpaceOneEquiv N k) f) = ⇑↑f

cuspFormCharSpaceOneEquiv does not change the underlying function on ℍ: a trivial-nebentypus cusp form is converted to a Γ₀(N)-cusp form by re-reading it, not by transporting it.

@[simp]

theorem TauCeti.coe_cuspFormCharSpaceOneEquiv_symm_apply {N : ℕ} {k : ℤ} [NeZero N] (f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma0 N)) k) : ↑((cuspFormCharSpaceOneEquiv N k).symm f) = CuspForm.ofLe ⋯ f

The inverse of cuspFormCharSpaceOneEquiv is the restriction CuspForm.ofLe of a Γ₀(N)-cusp form to Γ₁(N); in particular it too preserves the underlying function on ℍ.

The trace from Γ₁(N) to Γ₀(N) is the diamond sum

instance TauCeti.instIsFiniteRelIndexGamma1MapGamma0Map (N : ℕ) [NeZero N] : (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)).IsFiniteRelIndex (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma0 N))

For N ≠ 0, Γ₁(N) has finite index in Γ₀(N), so the trace from Γ₁(N) to Γ₀(N) is defined.

theorem TauCeti.coe_trace_eq_sum_diamondOpCusp {N : ℕ} {k : ℤ} [NeZero N] (F : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k) : ⇑(CuspForm.trace (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma0 N)) F) = ⇑(∑ u : (ZMod N)ˣ, (diamondOpCusp k u) F)

Mathlib's cusp-form trace from Γ₁(N) to Γ₀(N) is the diamond sum ∑ᵤ ⟨u⟩ F.

noncomputable def TauCeti.cuspFormTraceGamma0 (N : ℕ) (k : ℤ) [NeZero N] : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k →ₗ[ℂ] CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma0 N)) k

The trace from Γ₁(N) to Γ₀(N), Mathlib's CuspForm.trace, as a ℂ-linear map. By coe_trace_eq_sum_diamondOpCusp it is the diamond sum F ↦ ∑ᵤ ⟨u⟩ F.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.cuspFormTraceGamma0_apply {N : ℕ} {k : ℤ} [NeZero N] (F : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k) : (cuspFormTraceGamma0 N k) F = CuspForm.trace (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma0 N)) F

cuspFormTraceGamma0 is Mathlib's CuspForm.trace.

@[simp]

theorem TauCeti.cuspFormTraceGamma0_ofLe {N : ℕ} {k : ℤ} [NeZero N] (f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma0 N)) k) : (cuspFormTraceGamma0 N k) (CuspForm.ofLe ⋯ f) = ↑(Fintype.card (ZMod N)ˣ) • f

Tracing the restriction of a Γ₀(N) cusp form multiplies it by the index #(ZMod N)ˣ.

theorem TauCeti.cuspFormTraceGamma0_levelRaise {N : ℕ} {k : ℤ} {M d : ℕ} [NeZero N] [NeZero d] (hMN : M ∣ N) (hdvd : d * M ∣ N) (g : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 M)) k) (g₀ : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma0 M)) k) (hsum : CuspForm.ofLe ⋯ g₀ = ∑ u : (ZMod N)ˣ, (diamondOpCusp k ((ZMod.unitsMap hMN) u)) g) : (cuspFormTraceGamma0 N k) (CuspForm.levelRaise d ⋯ g) = CuspForm.levelRaise d ⋯ g₀

Tracing a level-raised cusp form commutes with level raising when the diamond sum at the lower level is the restriction of a Γ₀(M) cusp form.