Norm and trace maps #
Given two subgroups π’, β of GL(2, β) with π’.relindex β β 0 (i.e. π’ β β has finite index
in β), we define a trace map from ModularForm (π’ β β) k to ModularForm β k.
@[implicit_reducible]
instance
instMulActionSubtypeGeneralLinearGroupFinOfNatNatRealMemSubgroupQuotientSubgroupOf
{π’ β : Subgroup (GL (Fin 2) β)}
:
MulAction (β₯β) (β₯β β§Έ π’.subgroupOf β)
Equations
noncomputable def
SlashInvariantForm.quotientFunc
{π’ β : Subgroup (GL (Fin 2) β)}
{F : Type u_1}
(f : F)
[FunLike F UpperHalfPlane β]
{k : β€}
[SlashInvariantFormClass F π’ k]
(q : β₯β β§Έ π’.subgroupOf β)
(Ο : UpperHalfPlane)
:
For f invariant under π’, this is a function on (β β§Έ π’ β β) Γ β β β which packages up the
translates of f by β.
Equations
- SlashInvariantForm.quotientFunc f q Ο = Quotient.liftOn q (fun (g : β₯β) => SlashAction.map k (βg)β»ΒΉ (βf) Ο) β―
Instances For
@[simp]
theorem
SlashInvariantForm.quotientFunc_mk
{π’ β : Subgroup (GL (Fin 2) β)}
{F : Type u_1}
(f : F)
[FunLike F UpperHalfPlane β]
{k : β€}
[SlashInvariantFormClass F π’ k]
(h : β₯β)
:
theorem
SlashInvariantForm.quotientFunc_smul
{π’ β : Subgroup (GL (Fin 2) β)}
{F : Type u_1}
(f : F)
[FunLike F UpperHalfPlane β]
{k : β€}
[SlashInvariantFormClass F π’ k]
{h : GL (Fin 2) β}
(hh : h β β)
(q : β₯β β§Έ π’.subgroupOf β)
:
noncomputable def
SlashInvariantForm.trace
{π’ : Subgroup (GL (Fin 2) β)}
(β : Subgroup (GL (Fin 2) β))
{F : Type u_1}
(f : F)
[FunLike F UpperHalfPlane β]
{k : β€}
[SlashInvariantFormClass F π’ k]
[π’.IsFiniteRelIndex β]
:
SlashInvariantForm β k
The trace of a slash-invariant form, as a slash-invariant form.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
SlashInvariantForm.coe_trace
{π’ : Subgroup (GL (Fin 2) β)}
(β : Subgroup (GL (Fin 2) β))
{F : Type u_1}
(f : F)
[FunLike F UpperHalfPlane β]
{k : β€}
[SlashInvariantFormClass F π’ k]
[π’.IsFiniteRelIndex β]
:
noncomputable def
SlashInvariantForm.norm
{π’ : Subgroup (GL (Fin 2) β)}
(β : Subgroup (GL (Fin 2) β))
{F : Type u_1}
(f : F)
[FunLike F UpperHalfPlane β]
{k : β€}
[SlashInvariantFormClass F π’ k]
[π’.IsFiniteRelIndex β]
[β.HasDetPlusMinusOne]
:
SlashInvariantForm β (k * β(Nat.card (β₯β β§Έ π’.subgroupOf β)))
The norm of a slash-invariant form, as a slash-invariant form.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
SlashInvariantForm.coe_norm
{π’ : Subgroup (GL (Fin 2) β)}
(β : Subgroup (GL (Fin 2) β))
{F : Type u_1}
(f : F)
[FunLike F UpperHalfPlane β]
{k : β€}
[SlashInvariantFormClass F π’ k]
[π’.IsFiniteRelIndex β]
[β.HasDetPlusMinusOne]
:
noncomputable def
ModularForm.trace
{π’ : Subgroup (GL (Fin 2) β)}
(β : Subgroup (GL (Fin 2) β))
{F : Type u_1}
(f : F)
[FunLike F UpperHalfPlane β]
{k : β€}
[π’.IsFiniteRelIndex β]
[ModularFormClass F π’ k]
:
ModularForm β k
The trace of a modular form, as a modular form.
Equations
- ModularForm.trace β f = { toSlashInvariantForm := SlashInvariantForm.trace β f, holo' := β―, bdd_at_cusps' := β― }
Instances For
@[simp]
theorem
ModularForm.coe_trace
{π’ : Subgroup (GL (Fin 2) β)}
(β : Subgroup (GL (Fin 2) β))
{F : Type u_1}
(f : F)
[FunLike F UpperHalfPlane β]
{k : β€}
[π’.IsFiniteRelIndex β]
[ModularFormClass F π’ k]
:
β(ModularForm.trace β f) = β q : β₯β β§Έ π’.subgroupOf β, SlashInvariantForm.quotientFunc f q
noncomputable def
CuspForm.trace
{π’ : Subgroup (GL (Fin 2) β)}
(β : Subgroup (GL (Fin 2) β))
{F : Type u_1}
(f : F)
[FunLike F UpperHalfPlane β]
{k : β€}
[π’.IsFiniteRelIndex β]
[CuspFormClass F π’ k]
:
CuspForm β k
The trace of a cusp form, as a cusp form.
Equations
- CuspForm.trace β f = { toSlashInvariantForm := (ModularForm.trace β f).toSlashInvariantForm, holo' := β―, zero_at_cusps' := β― }
Instances For
@[simp]
theorem
CuspForm.coe_trace
{π’ : Subgroup (GL (Fin 2) β)}
(β : Subgroup (GL (Fin 2) β))
{F : Type u_1}
(f : F)
[FunLike F UpperHalfPlane β]
{k : β€}
[π’.IsFiniteRelIndex β]
[CuspFormClass F π’ k]
:
β(CuspForm.trace β f) = β q : β₯β β§Έ π’.subgroupOf β, SlashInvariantForm.quotientFunc f q
noncomputable def
ModularForm.norm
{π’ : Subgroup (GL (Fin 2) β)}
(β : Subgroup (GL (Fin 2) β))
{F : Type u_1}
(f : F)
[FunLike F UpperHalfPlane β]
{k : β€}
[π’.IsFiniteRelIndex β]
[β.HasDetPlusMinusOne]
[ModularFormClass F π’ k]
:
ModularForm β (k * β(Nat.card (β₯β β§Έ π’.subgroupOf β)))
The norm of a modular form, as a modular form.
Equations
- ModularForm.norm β f = { toSlashInvariantForm := SlashInvariantForm.norm β f, holo' := β―, bdd_at_cusps' := β― }
Instances For
@[simp]
theorem
ModularForm.coe_norm
{π’ : Subgroup (GL (Fin 2) β)}
(β : Subgroup (GL (Fin 2) β))
{F : Type u_1}
(f : F)
[FunLike F UpperHalfPlane β]
{k : β€}
[π’.IsFiniteRelIndex β]
[β.HasDetPlusMinusOne]
[ModularFormClass F π’ k]
:
β(ModularForm.norm β f) = β q : β₯β β§Έ π’.subgroupOf β, SlashInvariantForm.quotientFunc f q
theorem
ModularForm.norm_ne_zero
{π’ : Subgroup (GL (Fin 2) β)}
(β : Subgroup (GL (Fin 2) β))
{F : Type u_1}
{f : F}
[FunLike F UpperHalfPlane β]
{k : β€}
[π’.IsFiniteRelIndex β]
[β.HasDetPlusMinusOne]
[ModularFormClass F π’ k]
(hf : βf β 0)
:
theorem
ModularForm.norm_eq_zero_iff
{π’ : Subgroup (GL (Fin 2) β)}
(β : Subgroup (GL (Fin 2) β))
{F : Type u_1}
(f : F)
[FunLike F UpperHalfPlane β]
{k : β€}
[π’.IsFiniteRelIndex β]
[β.HasDetPlusMinusOne]
[ModularFormClass F π’ k]
:
theorem
ModularForm.isZero_of_neg_weight
{π’ : Subgroup (GL (Fin 2) β)}
[π’.IsArithmetic]
{k : β€}
(hk : k < 0)
(f : ModularForm π’ k)
:
theorem
ModularForm.eq_const_of_weight_zero
{π’ : Subgroup (GL (Fin 2) β)}
[π’.IsArithmetic]
(f : ModularForm π’ 0)
:
β (c : β), βf = Function.const UpperHalfPlane c