The Fricke operator is an involution up to a scalar

The Fricke matrix squares to the scalar matrix (-N) • 1 (coe_frickeGL_sq of TauCeti/NumberTheory/ModularForms/Fricke/Matrix.lean), and a scalar matrix acts trivially on ℍ. Slashing by W² is therefore multiplication by a constant, and the Fricke operator W_N of TauCeti/NumberTheory/ModularForms/Fricke/Operator.lean satisfies W_N ∘ W_N = c • id for that constant

c = N ^ (2 * (k - 1)) * (-N) ^ (-k).

The constant is nonzero, so W_N is invertible with W_N⁻¹ = c⁻¹ • W_N.

Main definitions

• TauCeti.frickeScalar: the constant c above.
• TauCeti.frickeOperatorEquiv, TauCeti.frickeOperatorCuspEquiv: W_N bundled as a linear automorphism of M_k(Γ₁(N)) and of S_k(Γ₁(N)), with inverse c⁻¹ • W_N.

Main results

• TauCeti.frickeGL_sq_slash: slashing by W² is multiplication by frickeScalar N k.
• TauCeti.frickeOperator_frickeOperator: W_N ∘ W_N = frickeScalar N k • id on M_k(Γ₁(N)).
• TauCeti.frickeOperatorCusp_frickeOperatorCusp: the same on S_k(Γ₁(N)).
• TauCeti.frickeOperator_frickeOperator_apply, TauCeti.frickeOperatorCusp_frickeOperatorCusp_apply: the pointwise forms of those two, which are the simp-normal ones.
• TauCeti.frickeScalar_def: the defining equation of the constant, for clients that cannot unfold it.
• TauCeti.frickeScalar_eq: its evaluated form (-1) ^ k * N ^ (k - 2).
• TauCeti.frickeScalar_ne_zero: the constant is nonzero, which is what makes W_N invertible.
• The two-sided inverse laws W_N ∘ (c⁻¹ • W_N) = id = (c⁻¹ • W_N) ∘ W_N, on modular and on cusp forms, are private: they exist only as the LinearEquiv.ofLinearMap arguments of the two equivalences above, which together with frickeOperator_frickeOperator are the public surface.
• TauCeti.slash_mul_frickeGL: slashing by A * W is frickeScalar N k • slashing by A * W⁻¹. This is the form the character-space transport will consume, where the two Fricke factors of a conjugated operator have to be collapsed onto one representative.

Where the scalar comes from

Weight-k slashing by g carries the factor |det g| ^ (k - 1) * denom g z ^ (-k). For g = W² the two factors are the two halves of frickeScalar: det W = N gives |det W²| = N ^ 2, and W² being the scalar matrix (-N) • 1 gives denom W² z = -N, independently of z. The remaining ingredient is that W² acts trivially on ℍ, so the f (W² • z) in the slash is just f z — mathlib's glScalar_smul.

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 states these over ℚ and pushes to ℝ through a glMap transport at every step; here, as already in Fricke/Operator.lean, frickeGL is read at ℝ directly and no transport appears. That also replaces AINTLIB's hand computation of W² • z and denom (W²) z from the matrix entries: over ℝ the square is literally a Matrix.GeneralLinearGroup.scalar, so mathlib's glScalar_smul and denom_scalar apply, and UpperHalfPlane.σ is discharged from positivity of det W² rather than from a rational-determinant side condition.

References

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

noncomputable def TauCeti.frickeScalar (N : ℕ) (k : ℤ) : ℂ

The scalar c with W_N ∘ W_N = c • id, namely c = N ^ (2 * (k - 1)) * (-N) ^ (-k): the |det| and denom factors of the weight-k slash by W² = (-N) • 1.

Equations

• TauCeti.frickeScalar N k = ↑N ^ (2 * (k - 1)) * (-↑N) ^ (-k)

theorem TauCeti.frickeScalar_def (N : ℕ) (k : ℤ) : frickeScalar N k = ↑N ^ (2 * (k - 1)) * (-↑N) ^ (-k)

Defining equation for frickeScalar. The definition is public but is not marked @[expose], so a downstream module rewrites with this rather than unfolding the body.

Deliberately not @[simp]: frickeScalar N k is the normal form here, not the expanded product. Every statement below is phrased in terms of the named constant, and the two factors only need to be visible inside frickeScalar_eq, which rewrites with this lemma explicitly.

theorem TauCeti.frickeScalar_eq {N : ℕ} [NeZero N] (k : ℤ) : frickeScalar N k = (-1) ^ k * ↑N ^ (k - 2)

The evaluated form of the scalar, (-1) ^ k * N ^ (k - 2), which is how Fricke/Operator.lean describes it and the form the normalized operator 𝒲_N = (√N) ^ (2 - k) • (· ∣[k] W) needs in order to be an involution in even weight.

[NeZero N] is load-bearing rather than ambient: at N = 0, k = 2 the two sides differ.

theorem TauCeti.frickeScalar_ne_zero {N : ℕ} [NeZero N] (k : ℤ) : frickeScalar N k ≠ 0

frickeScalar N k is nonzero. This is what makes the Fricke operator invertible, with inverse (frickeScalar N k)⁻¹ • W_N; see frickeOperatorEquiv.

theorem TauCeti.frickeGL_sq_slash {N : ℕ} [NeZero N] (k : ℤ) (f : UpperHalfPlane → ℂ) : SlashAction.map k (frickeGL ℝ N * frickeGL ℝ N) f = frickeScalar N k • f

Slashing by W² is multiplication by frickeScalar N k. W² = (-N) • 1 is a scalar matrix, so it acts trivially on ℍ and has constant denom; what is left of the weight-k slash is the constant |det W²| ^ (k - 1) * (-N) ^ (-k).

theorem TauCeti.slash_mul_frickeGL {N : ℕ} [NeZero N] (k : ℤ) (f : UpperHalfPlane → ℂ) (A : GL (Fin 2) ℝ) : SlashAction.map k (A * frickeGL ℝ N) f = frickeScalar N k • SlashAction.map k (A * (frickeGL ℝ N)⁻¹) f

Collapsing a Fricke factor: slashing by A * W is frickeScalar N k • slashing by A * W⁻¹, because A * W = (A * W⁻¹) * W². This is the step that lets the two Fricke factors of a W-conjugated operator be replaced by a single one.

theorem TauCeti.frickeOperator_frickeOperator {N : ℕ} [NeZero N] (k : ℤ) : frickeOperator k ∘ₗ frickeOperator k = frickeScalar N k • LinearMap.id

W_N ∘ W_N = frickeScalar N k • id on M_k(Γ₁(N)). Composing the operator with itself slashes by W², which frickeGL_sq_slash identifies with the scalar.

@[simp]

theorem TauCeti.frickeOperator_frickeOperator_apply {N : ℕ} [NeZero N] (k : ℤ) (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k) : (frickeOperator k) ((frickeOperator k) f) = frickeScalar N k • f

W_N (W_N f) = frickeScalar N k • f for a modular form f, the pointwise form of frickeOperator_frickeOperator. This, not the composition equality, is the simp-normal form: a goal mentioning W_N at all mentions it applied to a form.

noncomputable def TauCeti.frickeOperatorEquiv {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 operator as a linear automorphism of M_k(Γ₁(N)), with inverse (frickeScalar N k)⁻¹ • W_N.

Equations

• TauCeti.frickeOperatorEquiv k = LinearEquiv.ofLinearMap (TauCeti.frickeOperator k) ((TauCeti.frickeScalar N k)⁻¹ • TauCeti.frickeOperator k) ⋯ ⋯

@[simp]

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

The bundled Fricke operator acts as the Fricke operator.

@[simp]

theorem TauCeti.frickeOperatorEquiv_symm_apply {N : ℕ} [NeZero N] (k : ℤ) (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k) : (frickeOperatorEquiv k).symm f = (frickeScalar N k)⁻¹ • (frickeOperator k) f

The inverse of the bundled Fricke operator is (frickeScalar N k)⁻¹ • W_N.

theorem TauCeti.frickeOperatorCusp_frickeOperatorCusp {N : ℕ} [NeZero N] (k : ℤ) : frickeOperatorCusp k ∘ₗ frickeOperatorCusp k = frickeScalar N k • LinearMap.id

W_N ∘ W_N = frickeScalar N k • id on S_k(Γ₁(N)), the cusp-form form of frickeOperator_frickeOperator. With frickeScalar_ne_zero this makes W_N invertible on cusp forms.

@[simp]

theorem TauCeti.frickeOperatorCusp_frickeOperatorCusp_apply {N : ℕ} [NeZero N] (k : ℤ) (f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k) : (frickeOperatorCusp k) ((frickeOperatorCusp k) f) = frickeScalar N k • f

W_N (W_N f) = frickeScalar N k • f for a cusp form f, the pointwise and simp-normal form of frickeOperatorCusp_frickeOperatorCusp.

noncomputable def TauCeti.frickeOperatorCuspEquiv {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 operator as a linear automorphism of S_k(Γ₁(N)), with inverse (frickeScalar N k)⁻¹ • W_N.

Equations

• TauCeti.frickeOperatorCuspEquiv k = LinearEquiv.ofLinearMap (TauCeti.frickeOperatorCusp k) ((TauCeti.frickeScalar N k)⁻¹ • TauCeti.frickeOperatorCusp k) ⋯ ⋯

@[simp]

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

The bundled Fricke operator on cusp forms acts as frickeOperatorCusp.

@[simp]

theorem TauCeti.frickeOperatorCuspEquiv_symm_apply {N : ℕ} [NeZero N] (k : ℤ) (f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k) : (frickeOperatorCuspEquiv k).symm f = (frickeScalar N k)⁻¹ • (frickeOperatorCusp k) f

The inverse of the bundled Fricke operator on cusp forms is (frickeScalar N k)⁻¹ • W_N.