Documentation

Mathlib.NumberTheory.ModularForms.NormTrace

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.

source
instance instMulActionSubtypeGeneralLinearGroupFinOfNatNatRealMemSubgroup {โ„‹ : Subgroup (GL (Fin 2) โ„)} :
MulAction โ†ฅโ„‹ โ†ฅโ„‹
Equations
    source
    instance instMulActionSubtypeGeneralLinearGroupFinOfNatNatRealMemSubgroupQuotientSubgroupOf {๐’ข โ„‹ : Subgroup (GL (Fin 2) โ„)} :
    MulAction (โ†ฅโ„‹) (โ†ฅโ„‹ โงธ ๐’ข.subgroupOf โ„‹)
    Equations
      source
      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
        Instances For
          source
          @[simp]
          theorem SlashInvariantForm.quotientFunc_mk {๐’ข โ„‹ : Subgroup (GL (Fin 2) โ„)} {F : Type u_1} (f : F) [FunLike F UpperHalfPlane โ„‚] {k : โ„ค} [SlashInvariantFormClass F ๐’ข k] (h : โ†ฅโ„‹) :
          quotientFunc f โŸฆhโŸง = SlashAction.map k (โ†‘h)โปยน โ‡‘f
          source
          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 โ„‹) :
          SlashAction.map k h (quotientFunc f q) = quotientFunc f (โŸจh, hhโŸฉโปยน โ€ข q)
          source
          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
            Instances For
              source
              @[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 โ„‹] :
              โ‡‘(SlashInvariantForm.trace โ„‹ f) = โˆ‘ q : โ†ฅโ„‹ โงธ ๐’ข.subgroupOf โ„‹, quotientFunc f q
              source
              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
                Instances For
                  source
                  @[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] :
                  โ‡‘(SlashInvariantForm.norm โ„‹ f) = โˆ q : โ†ฅโ„‹ โงธ ๐’ข.subgroupOf โ„‹, quotientFunc f q
                  source
                  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
                    Instances For
                      source
                      @[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
                      source
                      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
                        Instances For
                          source
                          @[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
                          source
                          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
                            Instances For
                              source
                              @[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
                              source
                              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) :
                              ModularForm.norm โ„‹ f โ‰  0
                              source
                              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] :
                              ModularForm.norm โ„‹ f = 0 โ†” โ‡‘f = 0
                              source
                              theorem ModularForm.isZero_of_neg_weight {๐’ข : Subgroup (GL (Fin 2) โ„)} [๐’ข.IsArithmetic] {k : โ„ค} (hk : k < 0) (f : ModularForm ๐’ข k) :
                              f = 0
                              source
                              theorem ModularForm.eq_const_of_weight_zero {๐’ข : Subgroup (GL (Fin 2) โ„)} [๐’ข.IsArithmetic] (f : ModularForm ๐’ข 0) :
                              โˆƒ (c : โ„‚), โ‡‘f = Function.const UpperHalfPlane c