The Fricke operator on nebentypus character spaces #
The Fricke operator W_N of TauCeti/NumberTheory/ModularForms/Fricke/Operator.lean shifts the
diamond label by an inverse, W_N ∘ ⟨d⟩ = ⟨d⁻¹⟩ ∘ W_N (frickeOperator_diamondOp). Reading that
on a joint eigenspace of the diamond operators turns it into a statement about nebentypus: W_N
carries M_k(Γ₁(N), χ) into M_k(Γ₁(N), χ⁻¹), and since W_N ∘ W_N is the nonzero scalar
frickeScalar N k (frickeOperator_frickeOperator_apply), that transport is an isomorphism.
Main definitions #
TauCeti.frickeCharRestrict,TauCeti.frickeCharCuspRestrict:W_Nrestricted to theχ-nebentypus space, landing in theχ⁻¹-nebentypus space, on modular and on cusp forms.TauCeti.frickeCharEquiv,TauCeti.frickeCharCuspEquiv: those restrictions bundled as linear isomorphismsM_k(Γ₁(N), χ) ≃ₗ[ℂ] M_k(Γ₁(N), χ⁻¹)andS_k(Γ₁(N), χ) ≃ₗ[ℂ] S_k(Γ₁(N), χ⁻¹), with inverse(frickeScalar N k)⁻¹ • W_N.
Main results #
TauCeti.frickeOperator_mem_modFormCharSpace,TauCeti.frickeOperatorCusp_mem_cuspFormCharSpace: the transport itself,W_Nmaps theχ-nebentypus space into theχ⁻¹-nebentypus space.
The inverse character #
The target character is mathlib's χ⁻¹, the inverse in the commutative group (ZMod N)ˣ →* ℂˣ
(MonoidHom.instCommGroup), for which MonoidHom.inv_apply gives χ⁻¹ d = (χ d)⁻¹. The source
introduces a named chiConj χ = χ.comp invMonoidHom for this; that is the same monoid hom —
χ d⁻¹ = (χ d)⁻¹ is map_inv — so no definition is made here, matching the χ⁻¹ spelling
already used in the module docstring of Fricke/Operator.lean.
The round trip χ⁻¹⁻¹ = χ that a two-sided inverse needs is inv_inv_monoidHom below. That is
mathlib's inv_inv mathematically, but inv_inv is stated for InvolutiveInv and does not match
the Inv (M →* G) instance path syntactically, so it is proved pointwise instead, where the
inversion happens in ℂˣ.
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.
Three changes from the source. Its chiConj is dropped in favour of mathlib's χ⁻¹, as above.
Its private frickeOperator_sq_apply is dropped: frickeOperator_frickeOperator_apply of
Fricke/Involution.lean is that statement, already public. And the cusp-form halves, which the
source does not carry, are included here, since cuspFormCharSpace and
frickeOperatorCusp_diamondOpCusp are both available and every other result in this Fricke
development is stated on modular and on cusp forms alike.
References #
The Fricke operator shifts the nebentypus to its inverse: it carries M_k(Γ₁(N), χ) into
M_k(Γ₁(N), χ⁻¹).
On an f with ⟨d⟩ f = χ(d) • f, the diamond-shift frickeOperator_diamondOp read at d⁻¹
gives ⟨d⟩ (W f) = W (⟨d⁻¹⟩ f) = χ(d⁻¹) • (W f), and χ(d⁻¹) = χ⁻¹(d).
The Fricke operator shifts the nebentypus to its inverse, on cusp forms: it carries
S_k(Γ₁(N), χ) into S_k(Γ₁(N), χ⁻¹). The cusp-form counterpart of
frickeOperator_mem_modFormCharSpace, from the cusp-form diamond-shift.
The Fricke operator restricted to a nebentypus space, as a ℂ-linear map
M_k(Γ₁(N), χ) →ₗ[ℂ] M_k(Γ₁(N), χ⁻¹).
This is frickeOperator cut down by LinearMap.restrict.
Equations
Instances For
On underlying modular forms, frickeCharRestrict is frickeOperator.
The Fricke operator restricted to a nebentypus space of cusp forms, as a ℂ-linear map
S_k(Γ₁(N), χ) →ₗ[ℂ] S_k(Γ₁(N), χ⁻¹). The cusp-form counterpart of frickeCharRestrict.
Equations
Instances For
On underlying cusp forms, frickeCharCuspRestrict is frickeOperatorCusp. The cusp-form
counterpart of coe_frickeCharRestrict_apply, stated for the same reason.
The Fricke automorphism carries the χ-space onto the χ⁻¹-space. The surjective
refinement of frickeOperator_mem_modFormCharSpace, which gives only the forward inclusion.
The Fricke isomorphism between nebentypus spaces
M_k(Γ₁(N), χ) ≃ₗ[ℂ] M_k(Γ₁(N), χ⁻¹).
The ambient automorphism frickeOperatorEquiv restricted to the pair of character spaces it
matches up.
Equations
- TauCeti.frickeCharEquiv k χ = (TauCeti.frickeOperatorEquiv k).ofSubmodules (modFormCharSpace k χ) (modFormCharSpace k χ⁻¹) ⋯
Instances For
On underlying modular forms, frickeCharEquiv is frickeOperator.
On underlying modular forms, the inverse of frickeCharEquiv is
(frickeScalar N k)⁻¹ • frickeOperator.
The Fricke automorphism carries the χ-space of cusp forms onto the χ⁻¹-space. The
cusp-form counterpart of map_frickeOperatorEquiv_modFormCharSpace.
The Fricke isomorphism between nebentypus spaces of cusp forms
S_k(Γ₁(N), χ) ≃ₗ[ℂ] S_k(Γ₁(N), χ⁻¹). The cusp-form counterpart of frickeCharEquiv.
Equations
- TauCeti.frickeCharCuspEquiv k χ = (TauCeti.frickeOperatorCuspEquiv k).ofSubmodules (cuspFormCharSpace k χ) (cuspFormCharSpace k χ⁻¹) ⋯
Instances For
On underlying cusp forms, frickeCharCuspEquiv is frickeOperatorCusp.
On underlying cusp forms, the inverse of frickeCharCuspEquiv is
(frickeScalar N k)⁻¹ • frickeOperatorCusp.