Documentation

TauCeti.NumberTheory.ModularForms.Fricke.Normalized

The normalized Fricke operator 𝒲_N #

The raw Fricke slash f ↦ f ∣[k] W, W = !![0, -1; N, 0], is not an involution: it squares to the scalar frickeScalar N k = (-1) ^ k * N ^ (k - 2) (TauCeti.frickeOperator_frickeOperator). Dividing it by (√N) ^ (k - 2) removes the N-power and leaves only the sign. This file applies that arithmetic normalization,

𝒲_N f = (√N) ^ (2 - k) β€’ (f ∣[k] W),

proves 𝒲_N ∘ 𝒲_N = (-1) ^ k β€’ id, and reads off the two consequences the theory rests on: in even weight 𝒲_N is an involution, and its Β±1 eigenspaces are complementary in M_k(Γ₁(N)) and in S_k(Γ₁(N)).

Why the normalization is fixed once #

Every later Atkin–Lehner statement β€” 𝒲_Q 𝒲_R = 𝒲_{QR / gcd(Q, R) Β²} for exact divisors, the signs 𝒲_Q f = Ξ΅_Q f on a newform, and the sign i ^ k Β· Ξ΅_N of the functional equation of L(s, f) β€” is a statement about the normalized operator; with the raw slash they all acquire a stray power of N. So the constant is fixed once, in TauCeti/NumberTheory/ModularForms/AtkinLehner/Normalizer.lean, and the operator built from it is what the rest of the theory quantifies over.

The two constants #

Two scalars attached to W have names, and they are not the same one:

They are related by TauCeti.atkinLehnerNormalizer_sq_mul_frickeScalar: the square of the normalizer cancels the N-power of the scalar, leaving (-1) ^ k. That single identity is the whole arithmetic content of the file; everything else is bookkeeping around it.

Main definitions #

Main results #

Why Even k is a hypothesis, and not a defect #

𝒲_N ∘ 𝒲_N = (-1) ^ k β€’ id is sharp: at odd k the normalized operator squares to -1. A further factor of i would repair that, but it is not what the arithmetic normalization means β€” (√N) ^ (2 - k) is the constant the functional equation and the Petersson pairing are stated with, and a weight-dependent extra root of unity would desynchronise those statements from this one. Nothing is lost where the sign theory is stated: for trivial nebentypus and odd k the space is already zero, since Ο‡(-1) = 1 β‰  -1 = (-1) ^ k and TauCeti.modFormCharSpace_eq_bot_of_char_neg_one_ne applies. So the square law is kept at every weight β€” it is what the bundled automorphism below needs β€” and only the involution and the eigenspace splitting ask for Even k.

References #

The normalizing constant #

source
theorem TauCeti.atkinLehnerNormalizer_sq_mul_frickeScalar {N : β„•} [NeZero N] (k : β„€) :
atkinLehnerNormalizer N k ^ 2 * frickeScalar N k = (-1) ^ k

The normalization cancels the N-power of frickeScalar, leaving the sign (-1) ^ k. The constant itself is TauCeti.atkinLehnerNormalizer N k, the normalizer of the whole Atkin–Lehner family at the divisor Q = N; only its interaction with frickeScalar is special to the Fricke matrix.

The operator #

source
noncomputable def TauCeti.normalizedFrickeOperator {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 normalized Fricke operator 𝒲_N on M_k(Γ₁(N)): the raw slash by W scaled by atkinLehnerNormalizer N k. Unlike frickeOperator it squares to a sign, and in even weight it is an involution.

Equations
Instances For
    source
    theorem TauCeti.normalizedFrickeOperator_def {N : β„•} [NeZero N] (k : β„€) :
    normalizedFrickeOperator k = atkinLehnerNormalizer N k β€’ frickeOperator k

    Defining equation for normalizedFrickeOperator, for clients that cannot unfold it.

    source
    @[simp]
    theorem TauCeti.coe_normalizedFrickeOperator {N : β„•} [NeZero N] (k : β„€) (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k) :
    ⇑((normalizedFrickeOperator k) f) = atkinLehnerNormalizer N k β€’ SlashAction.map k (frickeGL ℝ N) ⇑f

    On underlying functions the normalized Fricke operator is (√N) ^ (2 - k) β€’ (⇑f ∣[k] W).

    source
    noncomputable def TauCeti.normalizedFrickeOperatorCusp {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 normalized Fricke operator on cusp forms S_k(Γ₁(N)).

    Equations
    Instances For
      source
      theorem TauCeti.normalizedFrickeOperatorCusp_def {N : β„•} [NeZero N] (k : β„€) :
      normalizedFrickeOperatorCusp k = atkinLehnerNormalizer N k β€’ frickeOperatorCusp k

      Defining equation for normalizedFrickeOperatorCusp.

      source
      @[simp]
      theorem TauCeti.coe_normalizedFrickeOperatorCusp {N : β„•} [NeZero N] (k : β„€) (f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k) :
      ⇑((normalizedFrickeOperatorCusp k) f) = atkinLehnerNormalizer N k β€’ SlashAction.map k (frickeGL ℝ N) ⇑f

      On underlying functions the normalized Fricke operator on cusp forms is (√N) ^ (2 - k) β€’ (⇑f ∣[k] W).

      source
      @[simp]
      theorem TauCeti.normalizedFrickeOperator_coe_cuspForm {N : β„•} [NeZero N] (k : β„€) (f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k) :
      (normalizedFrickeOperator k) (ModularFormClass.modularForm f) = ModularFormClass.modularForm ((normalizedFrickeOperatorCusp k) f)

      The two normalized Fricke operators agree under the coercion S_k(Γ₁(N)) β†’ M_k(Γ₁(N)), since the raw ones do and the scalar is the same.

      The square law #

      source
      theorem TauCeti.normalizedFrickeOperator_normalizedFrickeOperator {N : β„•} [NeZero N] (k : β„€) :
      normalizedFrickeOperator k βˆ˜β‚— normalizedFrickeOperator k = (-1) ^ k β€’ LinearMap.id

      𝒲_N ∘ 𝒲_N = (-1) ^ k β€’ id on M_k(Γ₁(N)).

      source
      @[simp]
      theorem TauCeti.normalizedFrickeOperator_normalizedFrickeOperator_apply {N : β„•} [NeZero N] (k : β„€) (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k) :
      (normalizedFrickeOperator k) ((normalizedFrickeOperator k) f) = (-1) ^ k β€’ f

      𝒲_N (𝒲_N f) = (-1) ^ k β€’ f for a modular form f, the pointwise form of normalizedFrickeOperator_normalizedFrickeOperator. As for the raw operator this, not the composition equality, is the simp-normal form.

      source
      theorem TauCeti.normalizedFrickeOperatorCusp_normalizedFrickeOperatorCusp {N : β„•} [NeZero N] (k : β„€) :
      normalizedFrickeOperatorCusp k βˆ˜β‚— normalizedFrickeOperatorCusp k = (-1) ^ k β€’ LinearMap.id

      𝒲_N ∘ 𝒲_N = (-1) ^ k β€’ id on S_k(Γ₁(N)).

      source
      @[simp]
      theorem TauCeti.normalizedFrickeOperatorCusp_normalizedFrickeOperatorCusp_apply {N : β„•} [NeZero N] (k : β„€) (f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k) :
      (normalizedFrickeOperatorCusp k) ((normalizedFrickeOperatorCusp k) f) = (-1) ^ k β€’ f

      𝒲_N (𝒲_N f) = (-1) ^ k β€’ f for a cusp form f.

      Even weight: an involution #

      source
      theorem TauCeti.normalizedFrickeOperator_involutive {N : β„•} [NeZero N] {k : β„€} (hk : Even k) :
      Function.Involutive ⇑(normalizedFrickeOperator k)

      In even weight 𝒲_N is an involution of M_k(Γ₁(N)) β€” the property the raw Fricke slash lacks and the whole normalization exists to supply.

      source
      theorem TauCeti.normalizedFrickeOperatorCusp_involutive {N : β„•} [NeZero N] {k : β„€} (hk : Even k) :
      Function.Involutive ⇑(normalizedFrickeOperatorCusp k)

      In even weight 𝒲_N is an involution of S_k(Γ₁(N)).

      The bundled automorphism #

      source
      noncomputable def TauCeti.normalizedFrickeOperatorEquiv {N : β„•} [NeZero N] (k : β„€) :
      ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k ≃ₗ[β„‚] ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k

      𝒲_N as a linear automorphism of M_k(Γ₁(N)), with inverse (-1) ^ k β€’ 𝒲_N. In even weight the inverse is the operator itself.

      Equations
      Instances For
        source
        @[simp]
        theorem TauCeti.normalizedFrickeOperatorEquiv_apply {N : β„•} [NeZero N] (k : β„€) (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k) :
        (normalizedFrickeOperatorEquiv k) f = (normalizedFrickeOperator k) f

        The bundled normalized Fricke automorphism acts as normalizedFrickeOperator.

        source
        @[simp]
        theorem TauCeti.normalizedFrickeOperatorEquiv_symm_apply {N : β„•} [NeZero N] (k : β„€) (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k) :
        (normalizedFrickeOperatorEquiv k).symm f = (-1) ^ k β€’ (normalizedFrickeOperator k) f

        The inverse of the bundled normalized Fricke automorphism is (-1) ^ k β€’ 𝒲_N.

        source
        noncomputable def TauCeti.normalizedFrickeOperatorCuspEquiv {N : β„•} [NeZero N] (k : β„€) :
        CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k ≃ₗ[β„‚] CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k

        𝒲_N as a linear automorphism of S_k(Γ₁(N)), with inverse (-1) ^ k β€’ 𝒲_N.

        Equations
        Instances For
          source
          @[simp]
          theorem TauCeti.normalizedFrickeOperatorCuspEquiv_apply {N : β„•} [NeZero N] (k : β„€) (f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k) :
          (normalizedFrickeOperatorCuspEquiv k) f = (normalizedFrickeOperatorCusp k) f

          The bundled normalized Fricke automorphism on cusp forms acts as normalizedFrickeOperatorCusp.

          source
          @[simp]
          theorem TauCeti.normalizedFrickeOperatorCuspEquiv_symm_apply {N : β„•} [NeZero N] (k : β„€) (f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k) :
          (normalizedFrickeOperatorCuspEquiv k).symm f = (-1) ^ k β€’ (normalizedFrickeOperatorCusp k) f

          The inverse of the bundled normalized Fricke automorphism on cusp forms.

          The nebentypus #

          source
          theorem TauCeti.normalizedFrickeOperator_mem_modFormCharSpace {N : β„•} [NeZero N] (k : β„€) (Ο‡ : (ZMod N)Λ£ β†’* β„‚Λ£) {f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k} (hf : f ∈ modFormCharSpace k Ο‡) :
          (normalizedFrickeOperator k) f ∈ modFormCharSpace k χ⁻¹

          The normalized Fricke operator shifts the nebentypus to its inverse: it carries M_k(Γ₁(N), Ο‡) into M_k(Γ₁(N), χ⁻¹). Scaling by a constant does not move a subspace, so this is the raw statement frickeOperator_mem_modFormCharSpace read through the normalization.

          source
          theorem TauCeti.normalizedFrickeOperatorCusp_mem_cuspFormCharSpace {N : β„•} [NeZero N] (k : β„€) (Ο‡ : (ZMod N)Λ£ β†’* β„‚Λ£) {f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k} (hf : f ∈ cuspFormCharSpace k Ο‡) :
          (normalizedFrickeOperatorCusp k) f ∈ cuspFormCharSpace k χ⁻¹

          The normalized Fricke operator shifts the nebentypus to its inverse, on cusp forms.

          source
          noncomputable def TauCeti.normalizedFrickeCharRestrict {N : β„•} [NeZero N] (k : β„€) (Ο‡ : (ZMod N)Λ£ β†’* β„‚Λ£) :
          β†₯(modFormCharSpace k Ο‡) β†’β‚—[β„‚] β†₯(modFormCharSpace k χ⁻¹)

          The normalized Fricke operator restricted to a nebentypus space, as a linear map from M_k(Γ₁(N), Ο‡) to M_k(Γ₁(N), χ⁻¹).

          Equations
          Instances For
            source
            @[simp]
            theorem TauCeti.coe_normalizedFrickeCharRestrict_apply {N : β„•} [NeZero N] (k : β„€) (Ο‡ : (ZMod N)Λ£ β†’* β„‚Λ£) (f : β†₯(modFormCharSpace k Ο‡)) :
            ↑((normalizedFrickeCharRestrict k Ο‡) f) = (normalizedFrickeOperator k) ↑f

            On underlying modular forms, normalizedFrickeCharRestrict is normalizedFrickeOperator.

            source
            noncomputable def TauCeti.normalizedFrickeCharCuspRestrict {N : β„•} [NeZero N] (k : β„€) (Ο‡ : (ZMod N)Λ£ β†’* β„‚Λ£) :
            β†₯(cuspFormCharSpace k Ο‡) β†’β‚—[β„‚] β†₯(cuspFormCharSpace k χ⁻¹)

            The normalized Fricke operator restricted to a cusp-form nebentypus space, as a linear map from S_k(Γ₁(N), Ο‡) to S_k(Γ₁(N), χ⁻¹).

            Equations
            Instances For
              source
              @[simp]
              theorem TauCeti.coe_normalizedFrickeCharCuspRestrict_apply {N : β„•} [NeZero N] (k : β„€) (Ο‡ : (ZMod N)Λ£ β†’* β„‚Λ£) (f : β†₯(cuspFormCharSpace k Ο‡)) :
              ↑((normalizedFrickeCharCuspRestrict k Ο‡) f) = (normalizedFrickeOperatorCusp k) ↑f

              On underlying cusp forms, normalizedFrickeCharCuspRestrict is normalizedFrickeOperatorCusp.

              source
              @[simp]
              theorem TauCeti.map_normalizedFrickeOperatorEquiv_modFormCharSpace {N : β„•} [NeZero N] (k : β„€) (Ο‡ : (ZMod N)Λ£ β†’* β„‚Λ£) :
              Submodule.map (↑(normalizedFrickeOperatorEquiv k)) (modFormCharSpace k Ο‡) = modFormCharSpace k χ⁻¹

              The normalized Fricke automorphism carries the Ο‡-space onto the χ⁻¹-space.

              source
              noncomputable def TauCeti.normalizedFrickeCharEquiv {N : β„•} [NeZero N] (k : β„€) (Ο‡ : (ZMod N)Λ£ β†’* β„‚Λ£) :
              β†₯(modFormCharSpace k Ο‡) ≃ₗ[β„‚] β†₯(modFormCharSpace k χ⁻¹)

              The normalized Fricke isomorphism between nebentypus spaces M_k(Γ₁(N), Ο‡) ≃ₗ[β„‚] M_k(Γ₁(N), χ⁻¹).

              Equations
              Instances For
                source
                @[simp]
                theorem TauCeti.coe_normalizedFrickeCharEquiv_apply {N : β„•} [NeZero N] (k : β„€) (Ο‡ : (ZMod N)Λ£ β†’* β„‚Λ£) (f : β†₯(modFormCharSpace k Ο‡)) :
                ↑((normalizedFrickeCharEquiv k Ο‡) f) = (normalizedFrickeOperator k) ↑f

                On underlying modular forms, normalizedFrickeCharEquiv is normalizedFrickeOperator.

                source
                @[simp]
                theorem TauCeti.coe_normalizedFrickeCharEquiv_symm_apply {N : β„•} [NeZero N] (k : β„€) (Ο‡ : (ZMod N)Λ£ β†’* β„‚Λ£) (g : β†₯(modFormCharSpace k χ⁻¹)) :
                ↑((normalizedFrickeCharEquiv k Ο‡).symm g) = (-1) ^ k β€’ (normalizedFrickeOperator k) ↑g

                On underlying modular forms, the inverse of normalizedFrickeCharEquiv is (-1) ^ k β€’ normalizedFrickeOperator.

                source
                @[simp]
                theorem TauCeti.map_normalizedFrickeOperatorCuspEquiv_cuspFormCharSpace {N : β„•} [NeZero N] (k : β„€) (Ο‡ : (ZMod N)Λ£ β†’* β„‚Λ£) :
                Submodule.map (↑(normalizedFrickeOperatorCuspEquiv k)) (cuspFormCharSpace k Ο‡) = cuspFormCharSpace k χ⁻¹

                The normalized Fricke automorphism carries the Ο‡-space of cusp forms onto the χ⁻¹-space.

                source
                noncomputable def TauCeti.normalizedFrickeCharCuspEquiv {N : β„•} [NeZero N] (k : β„€) (Ο‡ : (ZMod N)Λ£ β†’* β„‚Λ£) :
                β†₯(cuspFormCharSpace k Ο‡) ≃ₗ[β„‚] β†₯(cuspFormCharSpace k χ⁻¹)

                The normalized Fricke isomorphism between cusp-form nebentypus spaces S_k(Γ₁(N), Ο‡) ≃ₗ[β„‚] S_k(Γ₁(N), χ⁻¹).

                Equations
                Instances For
                  source
                  @[simp]
                  theorem TauCeti.coe_normalizedFrickeCharCuspEquiv_apply {N : β„•} [NeZero N] (k : β„€) (Ο‡ : (ZMod N)Λ£ β†’* β„‚Λ£) (f : β†₯(cuspFormCharSpace k Ο‡)) :
                  ↑((normalizedFrickeCharCuspEquiv k Ο‡) f) = (normalizedFrickeOperatorCusp k) ↑f

                  On underlying cusp forms, normalizedFrickeCharCuspEquiv is normalizedFrickeOperatorCusp.

                  source
                  @[simp]
                  theorem TauCeti.coe_normalizedFrickeCharCuspEquiv_symm_apply {N : β„•} [NeZero N] (k : β„€) (Ο‡ : (ZMod N)Λ£ β†’* β„‚Λ£) (g : β†₯(cuspFormCharSpace k χ⁻¹)) :
                  ↑((normalizedFrickeCharCuspEquiv k Ο‡).symm g) = (-1) ^ k β€’ (normalizedFrickeOperatorCusp k) ↑g

                  On underlying cusp forms, the inverse of normalizedFrickeCharCuspEquiv is (-1) ^ k β€’ normalizedFrickeOperatorCusp.

                  The eigenspace splitting in even weight #

                  source
                  theorem TauCeti.isCompl_eigenspace_normalizedFrickeOperator {N : β„•} [NeZero N] {k : β„€} (hk : Even k) :
                  IsCompl (Module.End.eigenspace (normalizedFrickeOperator k) 1) (Module.End.eigenspace (normalizedFrickeOperator k) (-1))

                  In even weight the Β±1 eigenspaces of 𝒲_N are complementary in M_k(Γ₁(N)).

                  This is the splitting from which the sign of the functional equation of L(s, f) is read off: on the +1 eigenspace 𝒲_N f = f, on the -1 eigenspace 𝒲_N f = -f, and every modular form is uniquely a sum of one of each.

                  source
                  theorem TauCeti.isCompl_eigenspace_normalizedFrickeOperatorCusp {N : β„•} [NeZero N] {k : β„€} (hk : Even k) :
                  IsCompl (Module.End.eigenspace (normalizedFrickeOperatorCusp k) 1) (Module.End.eigenspace (normalizedFrickeOperatorCusp k) (-1))

                  In even weight the Β±1 eigenspaces of 𝒲_N are complementary in S_k(Γ₁(N)).