The normalized Atkin–Lehner operators 𝒲_Q

The raw Atkin–Lehner slash W_Q of TauCeti/NumberTheory/ModularForms/AtkinLehner/Operator.lean squares to Q ^ (k - 2), so it is not an involution. Multiplying it by atkinLehnerNormalizer Q k = (√Q) ^ (2 - k) removes that scalar exactly, and the resulting normalized operator

𝒲_Q f = (√Q) ^ (2 - k) • (f ∣[k] W)

is an involution of M_k(Γ₀(N)) and of S_k(Γ₀(N)) — at every weight, with no parity hypothesis, because -I lies in Γ₀(N) and absorbs the sign that the Fricke operator on the Γ₁(N) carrier is left with.

Every later Atkin–Lehner statement — the signs 𝒲_Q f = ε_Q f on a newform, and the sign i ^ k · ε_N of the functional equation of L(s, f) — is a statement about 𝒲_Q, not about the raw slash, with which they would all acquire a stray power of Q.

The composition law

The exact divisors of N form a Boolean group under symmetric difference of the corresponding subsets of N.primeFactors, and the normalized operators act through it: for exact divisors Q and R,

𝒲_Q ∘ 𝒲_R = 𝒲_{Q R / gcd (Q, R) ²},

the divisor on the right being the symmetric difference of Q and R (TauCeti.Nat.IsExactDivisor.mul_div_gcd_sq). It is proved from two special cases: at coprime Q and R the product of an Atkin–Lehner matrix for Q and one for R is one for Q * R (TauCeti.IsAtkinLehnerMatrix.mul) and the normalizers multiply (TauCeti.atkinLehnerNormalizer_mul), so 𝒲_Q ∘ 𝒲_R = 𝒲_{Q R}; and at Q = R the operator is an involution. Writing g = gcd (Q, R), Q = g · q and R = g · r with g, q, r pairwise coprime exact divisors, the two cases give

𝒲_Q 𝒲_R = 𝒲_g 𝒲_q 𝒲_g 𝒲_r = 𝒲_g 𝒲_g 𝒲_q 𝒲_r = 𝒲_q 𝒲_r = 𝒲_{q r}.

In particular all of them commute. Bundling an exact divisor as TauCeti.Nat.ExactDivisor N gives this Boolean group explicitly, and normalizedAtkinLehnerRepresentation and its cusp-form counterpart are its representations on the two form spaces. The group is abstractly (ℤ/2) ^ ω(N): TauCeti.Nat.ExactDivisor.primeFactorsEquiv identifies it with the subsets of N.primeFactors, on which multiplication is symmetric difference and every element is its own inverse, and TauCeti.Nat.IsExactDivisor.prodPrimePow_primeFactors recovers an exact divisor as the product of the maximal prime powers p ^ v_p(N) it contains — the prime-power generators. The action may have a kernel: nothing here claims it is injective.

Main definitions

• TauCeti.Nat.IsExactDivisor.normalizedAtkinLehnerOperator, TauCeti.Nat.IsExactDivisor.normalizedAtkinLehnerOperatorCusp: 𝒲_Q on M_k(Γ₀(N)) and on S_k(Γ₀(N)).
• TauCeti.Nat.IsExactDivisor.normalizedAtkinLehnerOperatorEquiv, TauCeti.Nat.IsExactDivisor.normalizedAtkinLehnerOperatorCuspEquiv: 𝒲_Q bundled as a linear automorphism, its own inverse.
• TauCeti.Nat.ExactDivisor.normalizedAtkinLehnerRepresentation, TauCeti.Nat.ExactDivisor.normalizedAtkinLehnerCuspRepresentation: the action of the exact-divisor group on modular and cusp forms.

Main results

• TauCeti.Nat.IsExactDivisor.normalizedAtkinLehnerOperator_involutive and its cusp-form counterpart: 𝒲_Q is an involution, at every weight.
• TauCeti.Nat.IsExactDivisor.normalizedAtkinLehnerOperator_normalizedAtkinLehnerOperator and its cusp-form counterpart: the composition law 𝒲_Q ∘ 𝒲_R = 𝒲_{Q R / gcd (Q, R) ²}.
• TauCeti.Nat.IsExactDivisor.normalizedAtkinLehnerOperator_comm and its cusp-form counterpart: consequently the family is commutative.
• TauCeti.Nat.IsExactDivisor.normalizedAtkinLehnerOperator_one: 𝒲_1 is the identity, and TauCeti.Nat.IsExactDivisor.coe_normalizedAtkinLehnerOperator_self: 𝒲_N is the normalized Fricke slash, so the two endpoints of the family are the expected ones.
• TauCeti.Nat.IsExactDivisor.isCompl_eigenspace_normalizedAtkinLehnerOperator and its cusp-form counterpart: the ±1 eigenspaces of 𝒲_Q are complementary — the Atkin–Lehner sign decomposition of the space, whose labels are the Atkin–Lehner signs ε_Q. For a general exact divisor Q that label is the Atkin–Lehner eigenvalue and nothing more; it is only at the Fricke member Q = N, and only on a newform, that it becomes a sign of the functional equation of L(s, f).

References

• F. Diamond and J. Shurman, A First Course in Modular Forms, §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.

The operator

noncomputable def TauCeti.Nat.IsExactDivisor.normalizedAtkinLehnerOperator {N Q : ℕ} (h : IsExactDivisor Q N) (k : ℤ) : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma0 N)) k →ₗ[ℂ] ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma0 N)) k

The normalized Atkin–Lehner operator 𝒲_Q on M_k(Γ₀(N)), for an exact divisor Q of N: the raw slash W_Q scaled by atkinLehnerNormalizer Q k. Unlike W_Q it is an involution.

Equations

• h.normalizedAtkinLehnerOperator k = TauCeti.atkinLehnerNormalizer Q k • h.atkinLehnerOperator k

theorem TauCeti.Nat.IsExactDivisor.normalizedAtkinLehnerOperator_def {N Q : ℕ} (h : IsExactDivisor Q N) (k : ℤ) : h.normalizedAtkinLehnerOperator k = atkinLehnerNormalizer Q k • h.atkinLehnerOperator k

Defining equation for normalizedAtkinLehnerOperator: it is the raw operator W_Q scaled by atkinLehnerNormalizer Q k.

@[simp]

theorem TauCeti.Nat.IsExactDivisor.coe_normalizedAtkinLehnerOperator {N Q : ℕ} (h : IsExactDivisor Q N) (k : ℤ) (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma0 N)) k) : ⇑((h.normalizedAtkinLehnerOperator k) f) = atkinLehnerNormalizer Q k • SlashAction.map k (atkinLehnerGL ⋯ ⋯) ⇑f

On underlying functions 𝒲_Q is (√Q) ^ (2 - k) • (⇑f ∣[k] W).

noncomputable def TauCeti.Nat.IsExactDivisor.normalizedAtkinLehnerOperatorCusp {N Q : ℕ} (h : IsExactDivisor Q N) (k : ℤ) : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma0 N)) k →ₗ[ℂ] CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma0 N)) k

The normalized Atkin–Lehner operator on cusp forms S_k(Γ₀(N)).

Equations

• h.normalizedAtkinLehnerOperatorCusp k = TauCeti.atkinLehnerNormalizer Q k • h.atkinLehnerOperatorCusp k

theorem TauCeti.Nat.IsExactDivisor.normalizedAtkinLehnerOperatorCusp_def {N Q : ℕ} (h : IsExactDivisor Q N) (k : ℤ) : h.normalizedAtkinLehnerOperatorCusp k = atkinLehnerNormalizer Q k • h.atkinLehnerOperatorCusp k

Defining equation for normalizedAtkinLehnerOperatorCusp: it is the raw cusp-form operator W_Q scaled by atkinLehnerNormalizer Q k.

@[simp]

theorem TauCeti.Nat.IsExactDivisor.coe_normalizedAtkinLehnerOperatorCusp {N Q : ℕ} (h : IsExactDivisor Q N) (k : ℤ) (f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma0 N)) k) : ⇑((h.normalizedAtkinLehnerOperatorCusp k) f) = atkinLehnerNormalizer Q k • SlashAction.map k (atkinLehnerGL ⋯ ⋯) ⇑f

On underlying functions the cusp-form 𝒲_Q is (√Q) ^ (2 - k) • (⇑f ∣[k] W).

@[simp]

theorem TauCeti.Nat.IsExactDivisor.normalizedAtkinLehnerOperator_coe_cuspForm {N Q : ℕ} (h : IsExactDivisor Q N) (k : ℤ) (f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma0 N)) k) : (h.normalizedAtkinLehnerOperator k) (ModularFormClass.modularForm f) = ModularFormClass.modularForm ((h.normalizedAtkinLehnerOperatorCusp k) f)

The two normalized operators agree under the coercion S_k(Γ₀(N)) → M_k(Γ₀(N)), since the raw ones do and the scalar is the same.

theorem TauCeti.Nat.IsExactDivisor.normalizedAtkinLehnerOperator_congr {N Q Q' : ℕ} (h : IsExactDivisor Q N) (h' : IsExactDivisor Q' N) (hQQ' : Q = Q') (k : ℤ) (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma0 N)) k) : (h.normalizedAtkinLehnerOperator k) f = (h'.normalizedAtkinLehnerOperator k) f

The operator depends on the divisor only through its value. Two proofs that the same natural number is an exact divisor give the same operator, so an identity between divisors transports the operators along it.

theorem TauCeti.Nat.IsExactDivisor.normalizedAtkinLehnerOperatorCusp_congr {N Q Q' : ℕ} (h : IsExactDivisor Q N) (h' : IsExactDivisor Q' N) (hQQ' : Q = Q') (k : ℤ) (f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma0 N)) k) : (h.normalizedAtkinLehnerOperatorCusp k) f = (h'.normalizedAtkinLehnerOperatorCusp k) f

The cusp-form operator depends on the divisor only through its value.

The involution

@[simp]

theorem TauCeti.Nat.IsExactDivisor.normalizedAtkinLehnerOperator_normalizedAtkinLehnerOperator_self {N Q : ℕ} (h : IsExactDivisor Q N) (k : ℤ) (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma0 N)) k) : (h.normalizedAtkinLehnerOperator k) ((h.normalizedAtkinLehnerOperator k) f) = f

𝒲_Q (𝒲_Q f) = f on M_k(Γ₀(N)). The raw operator squares to Q ^ (k - 2) and the square of the normalizer is Q ^ (2 - k); no parity hypothesis on the weight is needed, since on the Γ₀(N) carrier the matrix -I acts trivially.

@[simp]

theorem TauCeti.Nat.IsExactDivisor.normalizedAtkinLehnerOperatorCusp_normalizedAtkinLehnerOperatorCusp_self {N Q : ℕ} (h : IsExactDivisor Q N) (k : ℤ) (f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma0 N)) k) : (h.normalizedAtkinLehnerOperatorCusp k) ((h.normalizedAtkinLehnerOperatorCusp k) f) = f

𝒲_Q (𝒲_Q f) = f on S_k(Γ₀(N)).

theorem TauCeti.Nat.IsExactDivisor.normalizedAtkinLehnerOperator_involutive {N Q : ℕ} (h : IsExactDivisor Q N) (k : ℤ) : Function.Involutive ⇑(h.normalizedAtkinLehnerOperator k)

𝒲_Q is an involution of M_k(Γ₀(N)) — the property the raw slash lacks and the whole normalization exists to supply.

theorem TauCeti.Nat.IsExactDivisor.normalizedAtkinLehnerOperatorCusp_involutive {N Q : ℕ} (h : IsExactDivisor Q N) (k : ℤ) : Function.Involutive ⇑(h.normalizedAtkinLehnerOperatorCusp k)

𝒲_Q is an involution of S_k(Γ₀(N)).

The bundled automorphism

noncomputable def TauCeti.Nat.IsExactDivisor.normalizedAtkinLehnerOperatorEquiv {N Q : ℕ} (h : IsExactDivisor Q N) (k : ℤ) : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma0 N)) k ≃ₗ[ℂ] ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma0 N)) k

𝒲_Q as a linear automorphism of M_k(Γ₀(N)), its own inverse.

Equations

• h.normalizedAtkinLehnerOperatorEquiv k = LinearEquiv.ofInvolutive (h.normalizedAtkinLehnerOperator k) ⋯

@[simp]

theorem TauCeti.Nat.IsExactDivisor.normalizedAtkinLehnerOperatorEquiv_apply {N Q : ℕ} (h : IsExactDivisor Q N) (k : ℤ) (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma0 N)) k) : (h.normalizedAtkinLehnerOperatorEquiv k) f = (h.normalizedAtkinLehnerOperator k) f

The bundled automorphism acts as 𝒲_Q.

@[simp]

theorem TauCeti.Nat.IsExactDivisor.normalizedAtkinLehnerOperatorEquiv_symm_apply {N Q : ℕ} (h : IsExactDivisor Q N) (k : ℤ) (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma0 N)) k) : (h.normalizedAtkinLehnerOperatorEquiv k).symm f = (h.normalizedAtkinLehnerOperator k) f

The bundled automorphism is its own inverse.

noncomputable def TauCeti.Nat.IsExactDivisor.normalizedAtkinLehnerOperatorCuspEquiv {N Q : ℕ} (h : IsExactDivisor Q N) (k : ℤ) : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma0 N)) k ≃ₗ[ℂ] CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma0 N)) k

𝒲_Q as a linear automorphism of S_k(Γ₀(N)), its own inverse.

Equations

• h.normalizedAtkinLehnerOperatorCuspEquiv k = LinearEquiv.ofInvolutive (h.normalizedAtkinLehnerOperatorCusp k) ⋯

@[simp]

theorem TauCeti.Nat.IsExactDivisor.normalizedAtkinLehnerOperatorCuspEquiv_apply {N Q : ℕ} (h : IsExactDivisor Q N) (k : ℤ) (f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma0 N)) k) : (h.normalizedAtkinLehnerOperatorCuspEquiv k) f = (h.normalizedAtkinLehnerOperatorCusp k) f

The bundled cusp-form automorphism acts as 𝒲_Q.

@[simp]

theorem TauCeti.Nat.IsExactDivisor.normalizedAtkinLehnerOperatorCuspEquiv_symm_apply {N Q : ℕ} (h : IsExactDivisor Q N) (k : ℤ) (f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma0 N)) k) : (h.normalizedAtkinLehnerOperatorCuspEquiv k).symm f = (h.normalizedAtkinLehnerOperatorCusp k) f

The bundled cusp-form automorphism is its own inverse.

The endpoints Q = 1 and Q = N

@[simp]

theorem TauCeti.Nat.IsExactDivisor.normalizedAtkinLehnerOperator_one {N : ℕ} (h : IsExactDivisor 1 N) (k : ℤ) (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma0 N)) k) : (h.normalizedAtkinLehnerOperator k) f = f

𝒲_1 is the identity on M_k(Γ₀(N)): the raw operator is, and the normalizer at Q = 1 is 1.

@[simp]

theorem TauCeti.Nat.IsExactDivisor.normalizedAtkinLehnerOperatorCusp_one {N : ℕ} (h : IsExactDivisor 1 N) (k : ℤ) (f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma0 N)) k) : (h.normalizedAtkinLehnerOperatorCusp k) f = f

𝒲_1 is the identity on S_k(Γ₀(N)).

theorem TauCeti.Nat.IsExactDivisor.coe_normalizedAtkinLehnerOperator_self {N : ℕ} (h : IsExactDivisor N N) (k : ℤ) (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma0 N)) k) : ⇑((h.normalizedAtkinLehnerOperator k) f) = atkinLehnerNormalizer N k • SlashAction.map k (frickeGL ℝ N) ⇑f

𝒲_N is the normalized Fricke slash on M_k(Γ₀(N)): on underlying functions it is (√N) ^ (2 - k) • (⇑f ∣[k] W) for the Fricke matrix W, which is what TauCeti.normalizedFrickeOperator performs on the Γ₁(N) carrier. The two operators have different carriers, so this function-level identity is the comparison between them.

theorem TauCeti.Nat.IsExactDivisor.coe_normalizedAtkinLehnerOperatorCusp_self {N : ℕ} (h : IsExactDivisor N N) (k : ℤ) (f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma0 N)) k) : ⇑((h.normalizedAtkinLehnerOperatorCusp k) f) = atkinLehnerNormalizer N k • SlashAction.map k (frickeGL ℝ N) ⇑f

𝒲_N is the normalized Fricke slash on S_k(Γ₀(N)).

The composition law

theorem TauCeti.Nat.IsExactDivisor.normalizedAtkinLehnerOperator_normalizedAtkinLehnerOperator_of_coprime {N Q R : ℕ} (hQ : IsExactDivisor Q N) (hR : IsExactDivisor R N) (hQR : Q.Coprime R) (k : ℤ) (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma0 N)) k) : (hR.normalizedAtkinLehnerOperator k) ((hQ.normalizedAtkinLehnerOperator k) f) = (⋯.normalizedAtkinLehnerOperator k) f

𝒲_R ∘ 𝒲_Q = 𝒲_{Q R} at coprime exact divisors, on M_k(Γ₀(N)). The raw operators compose this way because the matrices multiply, and the normalizers multiply as well.

theorem TauCeti.Nat.IsExactDivisor.normalizedAtkinLehnerOperatorCusp_normalizedAtkinLehnerOperatorCusp_of_coprime {N Q R : ℕ} (hQ : IsExactDivisor Q N) (hR : IsExactDivisor R N) (hQR : Q.Coprime R) (k : ℤ) (f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma0 N)) k) : (hR.normalizedAtkinLehnerOperatorCusp k) ((hQ.normalizedAtkinLehnerOperatorCusp k) f) = (⋯.normalizedAtkinLehnerOperatorCusp k) f

𝒲_R ∘ 𝒲_Q = 𝒲_{Q R} at coprime exact divisors, on S_k(Γ₀(N)).

@[simp]

theorem TauCeti.Nat.IsExactDivisor.normalizedAtkinLehnerOperator_normalizedAtkinLehnerOperator {N Q R : ℕ} (hQ : IsExactDivisor Q N) (hR : IsExactDivisor R N) (k : ℤ) (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma0 N)) k) : (hQ.normalizedAtkinLehnerOperator k) ((hR.normalizedAtkinLehnerOperator k) f) = (⋯.normalizedAtkinLehnerOperator k) f

The composition law 𝒲_Q ∘ 𝒲_R = 𝒲_{Q R / gcd (Q, R) ²} on M_k(Γ₀(N)), for arbitrary exact divisors Q and R of N. The divisor on the right is the symmetric difference of Q and R under the identification of exact divisors with subsets of N.primeFactors.

@[simp]

theorem TauCeti.Nat.IsExactDivisor.normalizedAtkinLehnerOperatorCusp_normalizedAtkinLehnerOperatorCusp {N Q R : ℕ} (hQ : IsExactDivisor Q N) (hR : IsExactDivisor R N) (k : ℤ) (f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma0 N)) k) : (hQ.normalizedAtkinLehnerOperatorCusp k) ((hR.normalizedAtkinLehnerOperatorCusp k) f) = (⋯.normalizedAtkinLehnerOperatorCusp k) f

The composition law 𝒲_Q ∘ 𝒲_R = 𝒲_{Q R / gcd (Q, R) ²} on S_k(Γ₀(N)).

The exact-divisor group action

noncomputable def TauCeti.Nat.ExactDivisor.normalizedAtkinLehnerRepresentation (N : ℕ) (k : ℤ) : ExactDivisor N →* ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma0 N)) k ≃ₗ[ℂ] ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma0 N)) k

The representation of the exact-divisor group on M_k(Γ₀(N)). An exact divisor acts by its normalized Atkin–Lehner automorphism. Multiplicativity is precisely the symmetric-difference composition law.

Equations

• TauCeti.Nat.ExactDivisor.normalizedAtkinLehnerRepresentation N k = { toFun := fun (Q : TauCeti.Nat.ExactDivisor N) => ⋯.normalizedAtkinLehnerOperatorEquiv k, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem TauCeti.Nat.ExactDivisor.normalizedAtkinLehnerRepresentation_apply (N : ℕ) (k : ℤ) (Q : ExactDivisor N) (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma0 N)) k) : ((normalizedAtkinLehnerRepresentation N k) Q) f = (⋯.normalizedAtkinLehnerOperator k) f

The exact-divisor representation acts by the normalized Atkin–Lehner operator.

noncomputable def TauCeti.Nat.ExactDivisor.normalizedAtkinLehnerCuspRepresentation (N : ℕ) (k : ℤ) : ExactDivisor N →* CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma0 N)) k ≃ₗ[ℂ] CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma0 N)) k

The representation of the exact-divisor group on S_k(Γ₀(N)). An exact divisor acts by its normalized Atkin–Lehner automorphism on cusp forms.

Equations

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

@[simp]

theorem TauCeti.Nat.ExactDivisor.normalizedAtkinLehnerCuspRepresentation_apply (N : ℕ) (k : ℤ) (Q : ExactDivisor N) (f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma0 N)) k) : ((normalizedAtkinLehnerCuspRepresentation N k) Q) f = (⋯.normalizedAtkinLehnerOperatorCusp k) f

The cusp-form exact-divisor representation acts by the normalized Atkin–Lehner operator.

theorem TauCeti.Nat.IsExactDivisor.normalizedAtkinLehnerOperator_comm {N Q R : ℕ} (hQ : IsExactDivisor Q N) (hR : IsExactDivisor R N) (k : ℤ) (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma0 N)) k) : (hQ.normalizedAtkinLehnerOperator k) ((hR.normalizedAtkinLehnerOperator k) f) = (hR.normalizedAtkinLehnerOperator k) ((hQ.normalizedAtkinLehnerOperator k) f)

The normalized Atkin–Lehner operators commute on M_k(Γ₀(N)): the divisor Q R / gcd (Q, R) ² they compose to is symmetric in Q and R.

theorem TauCeti.Nat.IsExactDivisor.normalizedAtkinLehnerOperatorCusp_comm {N Q R : ℕ} (hQ : IsExactDivisor Q N) (hR : IsExactDivisor R N) (k : ℤ) (f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma0 N)) k) : (hQ.normalizedAtkinLehnerOperatorCusp k) ((hR.normalizedAtkinLehnerOperatorCusp k) f) = (hR.normalizedAtkinLehnerOperatorCusp k) ((hQ.normalizedAtkinLehnerOperatorCusp k) f)

The normalized Atkin–Lehner operators commute on S_k(Γ₀(N)).

The eigenspace splitting

theorem TauCeti.Nat.IsExactDivisor.isCompl_eigenspace_normalizedAtkinLehnerOperator {N Q : ℕ} (h : IsExactDivisor Q N) (k : ℤ) : IsCompl (Module.End.eigenspace (h.normalizedAtkinLehnerOperator k) 1) (Module.End.eigenspace (h.normalizedAtkinLehnerOperator k) (-1))

The ±1 eigenspaces of 𝒲_Q are complementary in M_k(Γ₀(N)). This is the Atkin–Lehner sign decomposition of the space: on the +1 eigenspace 𝒲_Q f = f, on the -1 eigenspace 𝒲_Q f = -f, and every modular form for Γ₀(N) is uniquely a sum of one of each. The label of a newform under this splitting is its Atkin–Lehner sign ε_Q, and for a general exact divisor that is all it is; only at the Fricke member Q = N is it the sign appearing in the functional equation of L(s, f) (as i ^ k · ε_N). Unlike the Fricke statement on the Γ₁(N) carrier, no parity hypothesis on the weight is needed.

theorem TauCeti.Nat.IsExactDivisor.isCompl_eigenspace_normalizedAtkinLehnerOperatorCusp {N Q : ℕ} (h : IsExactDivisor Q N) (k : ℤ) : IsCompl (Module.End.eigenspace (h.normalizedAtkinLehnerOperatorCusp k) 1) (Module.End.eigenspace (h.normalizedAtkinLehnerOperatorCusp k) (-1))

The ±1 eigenspaces of 𝒲_Q are complementary in S_k(Γ₀(N)).