The Fricke slash operator on modular and cusp forms

The Fricke matrix W = !![0, -1; N, 0] of TauCeti/NumberTheory/ModularForms/Fricke/Matrix.lean normalizes Γ₁(N), by frickeConjSL_mem_Gamma1 of TauCeti/NumberTheory/ModularForms/Fricke/Conjugation.lean. Read in GL (Fin 2) ℝ that is the subgroup identity Gamma1_map_inv_conjAct_frickeGL_eq, and this file packages f ↦ f ∣[k] W as a ℂ-linear endomorphism frickeOperator of M_k(Γ₁(N)) and frickeOperatorCusp of S_k(Γ₁(N)).

What this operator is, and what it is not

frickeOperator is the raw slash by W: it carries no normalizing scalar, and it is therefore not an involution. With mathlib's weight-k slash and W² = (-N) • 1 (coe_frickeGL_sq) it squares to multiplication by the scalar N ^ (2 * (k - 1)) * (-N) ^ (-k), that is (-1) ^ k * N ^ (k - 2). That scalar is frickeScalar N k and the identity is frickeGL_sq_slash, both in TauCeti/NumberTheory/ModularForms/Fricke/Involution.lean; they are not restated here.

The roadmap's Fricke operator is the normalized 𝒲_N = (√N) ^ (2 - k) • (· ∣[k] W), which brings that scalar down to (-1) ^ k and so is an involution in even weight — the weights the sign theory lives in. It is a later rung, and every downstream statement about signs, eigenvalues and functional equations is about 𝒲_N, not about the map defined here. The name frickeOperator is AINTLIB's own name for the un-normalized map that this file ports, and the roadmap names it as the declaration to migrate, so it is kept; a consumer wanting 𝒲_N must supply the normalization.

Construction

Both operators are mathlib's ModularForm.translate/CuspForm.translate — which slash by an arbitrary g : GL (Fin 2) ℝ and carry holomorphy and the cusp conditions with them — transported back to level Γ₁(N) along Gamma1_map_inv_conjAct_frickeGL_eq with mcast. This is the construction diamondOpAux of TauCeti/NumberTheory/ModularForms/DiamondOperators.lean already uses for conjugation by Γ₀(N). Nothing about the cusps is proved here.

ℂ-linearity

Scalars commute past a slash only on the positive-determinant branch — mathlib's ModularForm.smul_slash otherwise carries the twist σ A c, which is complex conjugation. det W = N > 0, so ModularForm.smul_slash_of_det_pos of TauCeti/NumberTheory/ModularForms/Basic.lean applies and gives map_smul' for both operators.

The diamond shift

W conjugates a representative σ ∈ Γ₀(N) of d : (ZMod N)ˣ into frickeConjGamma0 σ, whose diamond label is d⁻¹ (toHomUnits_gamma0Map_frickeConjGamma0_eq_inv). So W does not commute with the diamond operators; it shifts them, W ∘ ⟨d⟩ = ⟨d⁻¹⟩ ∘ W. Read on a nebentypus space this says W carries M_k(Γ₁(N), χ) into M_k(Γ₁(N), χ⁻¹), which is what the character-space transport of the later Fricke rungs is built from.

Main definitions

• TauCeti.frickeOperator: the un-normalized Fricke slash operator on M_k(Γ₁(N)).
• TauCeti.frickeOperatorCusp: the un-normalized Fricke slash operator on S_k(Γ₁(N)).

Main results

• TauCeti.Gamma1_map_inv_conjAct_frickeGL_eq: W normalizes the image of Γ₁(N) in GL (Fin 2) ℝ. This is the group-level content of the construction, and what the later rungs (the character-space transport, the W_Q family) consume.
• TauCeti.coe_frickeOperator, TauCeti.coe_frickeOperatorCusp: on underlying functions both operators are ⇑f ∣[k] W.
• TauCeti.frickeOperator_coe_cuspForm: the two operators agree under the coercion S_k(Γ₁(N)) → M_k(Γ₁(N)).
• TauCeti.frickeOperator_diamondOp, TauCeti.frickeOperatorCusp_diamondOpCusp: the diamond shift W ∘ ⟨d⟩ = ⟨d⁻¹⟩ ∘ W, on modular and on cusp forms.

Provenance

Ported from the AINTLIB LeanModularForms project (LeanModularForms/HeckeRIngs/GL2/Fricke.lean, commit 340875adfb2, Apache-2.0, Chris Birkbeck), realizing part of Layer 6 of the ModularForms roadmap.

AINTLIB slashes by (frickeGL N : GL (Fin 2) ℚ) and lets the coercion to GL (Fin 2) ℝ do the work, so its frickeSlash_invariant consumes the hand-transported identity glMap_frickeGL_mul_mapGL; here W is read over ℝ directly, as an instance of the field-parameterized frickeGL_mul_mapGL, so no transport lemma appears. For the same reason AINTLIB's frickeGL_det_pos is val_det_frickeGL_pos read at ℝ.

Neither the slash-invariance nor the cusp conditions are ported. AINTLIB builds both operators field by field, deriving invariance from its own frickeSlash_invariant and rebuilding the image cusp by hand out of isCusp_SL2Z_iff before descending along the finite index of Γ₁(N) in SL₂(ℤ). Here the normalizer identity Gamma1_map_inv_conjAct_frickeGL_eq reduces both operators to translate, which mathlib proves for an arbitrary real matrix, so neither argument is needed.

AINTLIB proves ℂ-linearity with its own smul_slash_pos_det; the corresponding TauCeti lemma ModularForm.smul_slash_of_det_pos was already on hand, and is more general (any scalar α acting on ℂ by an IsScalarTower, rather than ℂ itself).

The source states the diamond shift through AINTLIB's Gamma0MapUnits, the unit-valued refinement of mathlib's CongruenceSubgroup.Gamma0Map, which TauCeti does not define. It is ported here over the composite (Gamma0Map N).toHomUnits that this repository already uses for the diamond label — the same substitution by which Gamma0MapUnits_frickeConjSL became toHomUnits_gamma0Map_frickeConjGamma0_eq_inv in Fricke/Conjugation.lean, and the reason no Gamma0MapUnits definition is needed to state it. AINTLIB evaluates ⟨d⟩ on a representative through its private diamondOp_eq_diamondOpAux; the public coe_diamondOp does that here, so no auxiliary is introduced. The cusp-form twin frickeOperatorCusp_diamondOpCusp has no counterpart in the source.

References

• F. Diamond and J. Shurman, A First Course in Modular Forms, §5.

theorem TauCeti.Gamma1_map_inv_conjAct_frickeGL_eq {N : ℕ} [NeZero N] : ConjAct.toConjAct (frickeGL ℝ N)⁻¹ • Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N) = Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)

W normalizes Γ₁(N) in GL (Fin 2) ℝ: conjugating the image of Γ₁(N) by the Fricke matrix returns that same subgroup. This is frickeConjSL_mem_Gamma1 — that W σ W⁻¹ stays in Γ₁(N) — turned into a statement about the subgroup itself, which is the form the operators below and the later Fricke rungs consume.

Both inclusions come from the normalization identities of Fricke/Conjugation.lean: frickeGL_mul_mapGL moves W rightwards past σ and gives ⊇, and mapGL_mul_frickeGL moves it leftwards and gives ⊆. The shape matches Gamma1_map_inv_conjAct_eq, the same statement for conjugation by Γ₀(N).

noncomputable def TauCeti.frickeOperator {N : ℕ} [NeZero N] (k : ℤ) : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k →ₗ[ℂ] ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k

The Fricke slash operator on M_k(Γ₁(N)): f ↦ f ∣[k] W for W = !![0, -1; N, 0], as a ℂ-linear endomorphism.

This is mathlib's ModularForm.translate by W, whose level W⁻¹ Γ₁(N) W is Γ₁(N) again by Gamma1_map_inv_conjAct_frickeGL_eq; mcast transports it back. It carries no normalizing scalar and is not an involution — see the module docstring.

Equations

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

@[simp]

theorem TauCeti.coe_frickeOperator {N : ℕ} [NeZero N] {k : ℤ} (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k) : ⇑((frickeOperator k) f) = SlashAction.map k (frickeGL ℝ N) ⇑f

On underlying functions the Fricke slash operator is ⇑f ∣[k] W.

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

The Fricke slash operator on cusp forms S_k(Γ₁(N)): the cusp-form counterpart of frickeOperator, built the same way from CuspForm.translate, so vanishing at the cusps comes from mathlib exactly as boundedness does.

Equations

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

@[simp]

theorem TauCeti.coe_frickeOperatorCusp {N : ℕ} [NeZero N] {k : ℤ} (f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k) : ⇑((frickeOperatorCusp k) f) = SlashAction.map k (frickeGL ℝ N) ⇑f

On underlying functions the Fricke slash operator on cusp forms is ⇑f ∣[k] W.

@[simp]

theorem TauCeti.frickeOperator_coe_cuspForm {N : ℕ} [NeZero N] (k : ℤ) (f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k) : (frickeOperator k) (ModularFormClass.modularForm f) = ModularFormClass.modularForm ((frickeOperatorCusp k) f)

The two Fricke slash operators agree under the coercion S_k(Γ₁(N)) → M_k(Γ₁(N)): both slash by W, which does not see whether a form vanishes at the cusps. This is the counterpart of diamondOp_coe_cuspForm for the diamond operators.

@[simp]

theorem TauCeti.frickeOperator_diamondOp {N : ℕ} [NeZero N] (k : ℤ) (d : (ZMod N)ˣ) : frickeOperator k ∘ₗ diamondOp k d = diamondOp k d⁻¹ ∘ₗ frickeOperator k

The diamond shift W ∘ ⟨d⟩ = ⟨d⁻¹⟩ ∘ W on M_k(Γ₁(N)): the Fricke operator does not commute with the diamond operators, it inverts their label. Read on a nebentypus space this says W carries M_k(Γ₁(N), χ) into M_k(Γ₁(N), χ⁻¹).

@[simp]

theorem TauCeti.frickeOperatorCusp_diamondOpCusp {N : ℕ} [NeZero N] (k : ℤ) (d : (ZMod N)ˣ) : frickeOperatorCusp k ∘ₗ diamondOpCusp k d = diamondOpCusp k d⁻¹ ∘ₗ frickeOperatorCusp k

The diamond shift on cusp forms: the S_k(Γ₁(N)) counterpart of frickeOperator_diamondOp.