Documentation

TauCeti.NumberTheory.ModularForms.Petersson.AtkinLehner

The Fricke and Atkin–Lehner operators are Petersson-unitary #

The Fricke matrix W_N = !![0, -1; N, 0] normalises Γ₁(N), and an Atkin–Lehner matrix W_Q for an exact divisor Q ∥ N normalises Γ₀(N). Their determinants are N, respectively Q, so for N ≠ 1, respectively Q ≠ 1, they do not lie in SL₂(ℤ). Slashing both arguments of the Petersson product by such a matrix of determinant D multiplies the product by D ^ (k - 2) (TauCeti.CuspForm.peterssonInnerCosets_slash_of_inv_conjAct_eq), and the arithmetic normalization 𝒲_Q = (√Q) ^ (2 - k) • (· ∣[k] W_Q) is exactly the one that cancels this factor: the normalizer is real and its square is Q ^ (2 - k). So the normalized operators are unitary for the Petersson product,

⟪𝒲_N f, 𝒲_N g⟫ = ⟪f, g⟫   on S_k(Γ₁(N)),        ⟪𝒲_Q f, 𝒲_Q g⟫ = ⟪f, g⟫   on S_k(Γ₀(N)).

Combined with the square laws 𝒲_N² = (-1) ^ k and 𝒲_Q² = 1, unitarity gives the adjoints: 𝒲_Q is self-adjoint on S_k(Γ₀(N)), and 𝒲_N is self-adjoint up to the sign (-1) ^ k on S_k(Γ₁(N)). Consequently the Petersson-orthogonal complement of a subspace stable under one of these operators is again stable under it. That is the form in which the Fricke and Atkin–Lehner operators reach the newforms: the new subspace is the Petersson-orthogonal complement of the old subspace, so an operator preserving the old subspace preserves the new one, and on a newform of trivial nebentypus multiplicity one then turns 𝒲_Q f into a multiple ± f — the Atkin–Lehner sign.

Main results #

References #

The Fricke operator #

source
theorem TauCeti.peterssonInnerCosets_frickeOperatorCusp {N : ℕ} [NeZero N] (k : ℤ) (f g : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k) :
((frickeOperatorCusp k) f).peterssonInnerCosets ((frickeOperatorCusp k) g) = ↑N ^ (k - 2) * f.peterssonInnerCosets g

The raw Fricke operator scales the Petersson product by N ^ (k - 2): ⟪f ∣[k] W_N, g ∣[k] W_N⟫ = N ^ (k - 2) · ⟪f, g⟫ on S_k(Γ₁(N)), the determinant of W_N = !![0, -1; N, 0] being N.

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

The normalized Fricke operator is Petersson-unitary: ⟪𝒲_N f, 𝒲_N g⟫ = ⟪f, g⟫ on S_k(Γ₁(N)), in every weight. The normalizer (√N) ^ (2 - k) is real, so it contributes its square N ^ (2 - k), cancelling the factor N ^ (k - 2) of the raw operator.

source
theorem TauCeti.peterssonInnerCosets_normalizedFrickeOperatorCusp_left {N : ℕ} [NeZero N] (k : ℤ) (f g : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k) :
((normalizedFrickeOperatorCusp k) f).peterssonInnerCosets g = (-1) ^ k * f.peterssonInnerCosets ((normalizedFrickeOperatorCusp k) g)

The Petersson adjoint of the normalized Fricke operator is (-1) ^ k • 𝒲_N: ⟪𝒲_N f, g⟫ = (-1) ^ k · ⟪f, 𝒲_N g⟫ on S_k(Γ₁(N)). Unitarity and the square law 𝒲_N² = (-1) ^ k combine to this; in even weight 𝒲_N is self-adjoint.

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

The Petersson-orthogonal complement of a 𝒲_N-stable subspace is 𝒲_N-stable. The adjoint of 𝒲_N is a scalar multiple of 𝒲_N itself (peterssonInnerCosets_normalizedFrickeOperatorCusp_left), so it preserves V whenever 𝒲_N does.

The Atkin–Lehner operators #

source
theorem TauCeti.Nat.IsExactDivisor.peterssonInnerCosets_atkinLehnerOperatorCusp {N Q : ℕ} [NeZero N] (h : IsExactDivisor Q N) (k : ℤ) (f g : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma0 N)) k) :
((h.atkinLehnerOperatorCusp k) f).peterssonInnerCosets ((h.atkinLehnerOperatorCusp k) g) = ↑Q ^ (k - 2) * f.peterssonInnerCosets g

The raw Atkin–Lehner operator scales the Petersson product by Q ^ (k - 2): ⟪f ∣[k] W_Q, g ∣[k] W_Q⟫ = Q ^ (k - 2) · ⟪f, g⟫ on S_k(Γ₀(N)), the determinant of an Atkin–Lehner matrix for Q being Q.

source
@[simp]
theorem TauCeti.Nat.IsExactDivisor.peterssonInnerCosets_normalizedAtkinLehnerOperatorCusp {N Q : ℕ} [NeZero N] (h : IsExactDivisor Q N) (k : ℤ) (f g : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma0 N)) k) :
((h.normalizedAtkinLehnerOperatorCusp k) f).peterssonInnerCosets ((h.normalizedAtkinLehnerOperatorCusp k) g) = f.peterssonInnerCosets g

The normalized Atkin–Lehner operator is Petersson-unitary: ⟪𝒲_Q f, 𝒲_Q g⟫ = ⟪f, g⟫ on S_k(Γ₀(N)). The real normalizer (√Q) ^ (2 - k) cancels the factor Q ^ (k - 2) of the raw operator.

source
theorem TauCeti.Nat.IsExactDivisor.peterssonInnerCosets_normalizedAtkinLehnerOperatorCusp_left {N Q : ℕ} [NeZero N] (h : IsExactDivisor Q N) (k : ℤ) (f g : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma0 N)) k) :
((h.normalizedAtkinLehnerOperatorCusp k) f).peterssonInnerCosets g = f.peterssonInnerCosets ((h.normalizedAtkinLehnerOperatorCusp k) g)

The normalized Atkin–Lehner operator is Petersson self-adjoint: ⟪𝒲_Q f, g⟫ = ⟪f, 𝒲_Q g⟫ on S_k(Γ₀(N)), a unitary involution being its own adjoint.

source
theorem TauCeti.Nat.IsExactDivisor.normalizedAtkinLehnerOperatorCusp_mem_peterssonOrthogonal {N Q : ℕ} [NeZero N] (h : IsExactDivisor Q N) {k : ℤ} {V : Submodule ℂ (CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma0 N)) k)} (hV : ∀ f ∈ V, (h.normalizedAtkinLehnerOperatorCusp k) f ∈ V) {f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma0 N)) k} (hf : f ∈ CuspForm.peterssonOrthogonal V) :
(h.normalizedAtkinLehnerOperatorCusp k) f ∈ CuspForm.peterssonOrthogonal V

The Petersson-orthogonal complement of a 𝒲_Q-stable subspace is 𝒲_Q-stable, 𝒲_Q being self-adjoint.