Documentation

TauCeti.NumberTheory.ModularForms.Petersson.Unitary

The Petersson product is unitary under a normalising slash #

The Petersson product CuspForm.peterssonInnerCosets on S_k(Γ) is a sum over the cosets of Γ·{±I} in SL₂(ℤ) of level-one-domain pairings of slashed forms. Slashing both arguments by an α ∈ SL₂(ℤ) that normalises Γ·{±I} permutes those cosets — right multiplication by α⁻¹ is a well-defined permutation of SL₂(ℤ)/Γ·{±I} exactly because α normalises the group — so it leaves the whole sum unchanged: such a slash is unitary for the Petersson product.

The main case is Γ = Γ₁(N) and α ∈ Γ₀(N), that is, the diamond operators ⟨d⟩ of TauCeti/NumberTheory/ModularForms/DiamondOperators.lean: ⟪⟨d⟩f, ⟨d⟩g⟫ = ⟪f, g⟫.

The normaliser in SL₂(ℤ) is not the whole story: the Fricke matrix !![0, -1; N, 0] and the Atkin–Lehner matrices normalise Γ₁(N) or Γ₀(N) from inside GL₂(ℝ), with determinant D > 0, in general different from 1. For such an α the coset-sum argument is unavailable — α does not act on SL₂(ℤ)/Γ·{±I} — and the pairing is instead read as one integral over a fundamental domain, which α carries to another fundamental domain; what survives of the slash is the factor D ^ (k - 2) of UpperHalfPlane.peterssonInner_slash_slash_of_det_pos. The same argument needs no normalising hypothesis: an α conjugating Γ onto Γ' carries a fundamental domain for Γ to one for Γ', and so compares the Petersson products at the two levels.

Two consequences of the diamond case carry the newform theory forward. First, the Petersson-orthogonal complement of a diamond-stable subspace is again diamond-stable — the diamonds form a group of unitaries, so a stable subspace is mapped onto itself, which is what an orthogonal complement needs. Second, cusp forms with distinct nebentypus characters are Petersson-orthogonal, since the diamond eigenvalues χ(d) are roots of unity: unitarity turns ⟪f, g⟫ into conj (χ d) * ψ d * ⟪f, g⟫, and the scalar differs from 1 at some d.

Main results #

References #

Slashing by a normalising element #

source
theorem TauCeti.CuspForm.peterssonInnerCosets_slash {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} [Γ.FiniteIndex] {k : ℤ} {α : Matrix.SpecialLinearGroup (Fin 2) ℤ} (hα : α ∈ Subgroup.normalizer ↑Γ.withCenter) {f g F G : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k} (hF : ⇑F = SlashAction.map k α ⇑f) (hG : ⇑G = SlashAction.map k α ⇑g) :
F.peterssonInnerCosets G = f.peterssonInnerCosets g

The Petersson product is unitary under a normalising slash. If α ∈ SL₂(ℤ) normalises Γ·{±I} and the slashes f ∣[k] α, g ∣[k] α are again cusp forms F, G for Γ, then ⟪F, G⟫ = ⟪f, g⟫: right multiplication by α⁻¹ permutes the cosets of Γ·{±I} indexing the defining sum, and the summands match up term by term.

It is Γ·{±I}, not Γ, that the hypothesis constrains, that being the group whose cosets the sum runs over; an α normalising Γ normalises Γ·{±I} too, by Subgroup.normalizer_le_normalizer_sup_normal.

The forms F and G are taken as data with their defining equations, rather than built here, because the operators that arise this way — the diamond operators of Layer 0, the Atkin–Lehner involutions later — each package the slashed function as a cusp form in their own way.

source
theorem TauCeti.CuspForm.peterssonInnerCosets_slash_of_inv_conjAct_eq {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} [Γ.FiniteIndex] {k : ℤ} {Γ' : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} [Γ'.FiniteIndex] {α : GL (Fin 2) ℝ} (hdet : 0 < (↑α).det) (hα : ConjAct.toConjAct α⁻¹ • Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ' = Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) {f g : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ') k} {F G : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k} (hF : ⇑F = SlashAction.map k α ⇑f) (hG : ⇑G = SlashAction.map k α ⇑g) :
F.peterssonInnerCosets G = ↑(↑α).det ^ (k - 2) * f.peterssonInnerCosets g

Slashing by a conjugating element of GL₂(ℝ) rescales the Petersson product. If α ∈ GL₂(ℝ) has positive determinant and conjugates the image of Γ in GL₂(ℝ) onto that of Γ' — α⁻¹ Γ' α = Γ — and F, G are the cusp forms for Γ obtained by slashing cusp forms f, g for Γ' by α, then

⟪F, G⟫_Γ = (det α) ^ (k - 2) · ⟪f, g⟫_Γ'.

The pairing is one integral over the fundamental domain ⋃_q q⁻¹ • 𝒟ᵒ (CuspForm.peterssonInnerCosets_eq_peterssonInner); the slash moves it to the translate by α at the cost of (det α) ^ (k - 2) (UpperHalfPlane.peterssonInner_slash_slash_of_det_pos), and that translate is a fundamental domain for Γ' (ModularGroup.isFundamentalDomain_smul_of_inv_conjAct_eq), over which the pairing is the same as over any other (UpperHalfPlane.peterssonInner_eq_of_isFundamentalDomain).

With Γ' = Γ this is the case of a normaliser, such as the Fricke and Atkin–Lehner matrices; with Γ' ≠ Γ it is the conjugation step of the adjoint theory of the double coset operators (CuspForm.peterssonInnerCosets_trace_translate). As in peterssonInnerCosets_slash, the forms F and G are taken as data with their defining equations, since the operators that arise this way each package the slashed function as a cusp form in their own way.

The diamond operators are unitary #

source
@[simp]
theorem TauCeti.CuspForm.peterssonInnerCosets_diamondOpCusp {N : ℕ} [NeZero N] (k : ℤ) (d : (ZMod N)ˣ) (f g : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k) :
((diamondOpCusp k d) f).peterssonInnerCosets ((diamondOpCusp k d) g) = f.peterssonInnerCosets g

The diamond operators are Petersson-unitary: ⟪⟨d⟩f, ⟨d⟩g⟫ = ⟪f, g⟫. The operator ⟨d⟩ is slashing by a representative of d in Γ₀(N), and Γ₀(N) normalises Γ₁(N), hence also Γ₁(N)·{±I}.

source
theorem TauCeti.CuspForm.diamondOpCusp_mem_peterssonOrthogonal {N : ℕ} [NeZero N] {k : ℤ} {V : Submodule ℂ (CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k)} (hV : ∀ (u : (ZMod N)ˣ), ∀ f ∈ V, (diamondOpCusp k u) f ∈ V) (d : (ZMod N)ˣ) {f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k} (hf : f ∈ peterssonOrthogonal V) :
(diamondOpCusp k d) f ∈ peterssonOrthogonal V

The Petersson-orthogonal complement of a diamond-stable subspace is diamond-stable. Unitarity alone would not suffice: what is used is that the diamonds form a group, so a stable subspace V is carried onto itself by ⟨d⟩, and every g ∈ V is ⟨d⟩ of the element ⟨d⁻¹⟩ g of V.

Distinct nebentypus characters are orthogonal #

source
theorem TauCeti.CuspForm.peterssonInnerCosets_eq_zero_of_mem_cuspFormCharSpace_of_ne {N : ℕ} [NeZero N] {k : ℤ} {χ ψ : (ZMod N)ˣ →* ℂˣ} (hne : χ ≠ ψ) {f g : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k} (hf : f ∈ cuspFormCharSpace k χ) (hg : g ∈ cuspFormCharSpace k ψ) :
f.peterssonInnerCosets g = 0

Cusp forms with distinct nebentypus characters are Petersson-orthogonal. The diamond operators are unitary and act on the two forms by the scalars χ(d) and ψ(d), so the pairing is multiplied by conj (χ d) * ψ d; at a d where the characters differ this scalar is not 1, the values being unimodular. Hence the nebentypus decomposition of S_k(Γ₁(N)) is an orthogonal decomposition.

source
theorem TauCeti.CuspForm.cuspFormCharSpace_le_peterssonOrthogonal_of_ne {N : ℕ} [NeZero N] {k : ℤ} {χ ψ : (ZMod N)ˣ →* ℂˣ} (hne : χ ≠ ψ) :
cuspFormCharSpace k ψ ≤ peterssonOrthogonal (cuspFormCharSpace k χ)

The nebentypus decomposition of S_k(Γ₁(N)) is orthogonal: distinct nebentypus spaces are Petersson-orthogonal, the submodule form of peterssonInnerCosets_eq_zero_of_mem_cuspFormCharSpace_of_ne.