1. Hecke operators, diamond operators, and character spaces🔗

Definition1.1

uses 0

Used by 2

Reverse dependency previews

Preview

Definition 1.2

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

For a level N, weight k, and a unit d \in (\mathbb{Z}/N)^\times, the diamond operator \langle d \rangle acts on M_k(\Gamma_1(N)) by slashing with any \gamma \in \Gamma_0(N) whose lower-right entry reduces to d. The diamonds form a commuting family of finite-order (hence semisimple) operators, packaged as the monoid homomorphism \texttt{diamondOpHom}. Following Miyake §4.3.

Lean code for Definition1.1●1 definition

defdefined in LeanModularForms/HeckeRIngs/GL2/Gamma1Pair.lean

complete

def HeckeRing.GL2.diamondOpHom {N : ℕ} [NeZero N] (k : ℤ) :
  (ZMod N)ˣ →*
    Module.End ℂ
      (ModularForm
        (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ)
          (CongruenceSubgroup.Gamma1 N))
        k)

def HeckeRing.GL2.diamondOpHom {N : ℕ}
  [NeZero N] (k : ℤ) :
  (ZMod N)ˣ →*
    Module.End ℂ
      (ModularForm
        (Subgroup.map
          (Matrix.SpecialLinearGroup.mapGL
            ℝ)
          (CongruenceSubgroup.Gamma1 N))
        k)

The diamond operator as a monoid homomorphism `(ZMod N)ˣ →* Module.End ℂ (...)`.

Definition1.2

uses 1

Used by 4

Reverse dependency previews

Preview

Theorem 1.3

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

Fix a level N and weight k. The space of modular forms decomposes under the diamond operators \langle d \rangle (Definition 1.1) into character (\chi-isotypic) spaces: for a Dirichlet character \chi : (\mathbb{Z}/N)^\times \to \mathbb{C}^\times, M_k(N, \chi) = \bigcap_{d} \ker\bigl(\langle d \rangle - \chi(d)\bigr), the intersection over all units d of the \chi(d)-eigenspaces of the diamonds, with cusp-form analogue S_k(N, \chi). In LeanModularForms this is \texttt{modFormCharSpace}. Following Miyake §4.3.

Lean code for Definition1.2●1 definition

defdefined in LeanModularForms/HeckeRIngs/GL2/Gamma1Pair.lean

complete

def HeckeRing.GL2.modFormCharSpace {N : ℕ} [NeZero N] (k : ℤ)
  (χ : (ZMod N)ˣ →* ℂˣ) :
  Submodule ℂ
    (ModularForm
      (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ)
        (CongruenceSubgroup.Gamma1 N))
      k)

def HeckeRing.GL2.modFormCharSpace {N : ℕ}
  [NeZero N] (k : ℤ)
  (χ : (ZMod N)ˣ →* ℂˣ) :
  Submodule ℂ
    (ModularForm
      (Subgroup.map
        (Matrix.SpecialLinearGroup.mapGL
          ℝ)
        (CongruenceSubgroup.Gamma1 N))
      k)

The modular-form Nebentypus character space `M_k(Γ₁(N), χ)`.

Theorem1.3

uses 1used by 1✓L∃∀N

The character spaces M_k(N, \chi) are independent and span everything, giving the isotypic decomposition (Definition 1.2) M_k(\Gamma_1(N)) = \bigoplus_{\chi} M_k(N, \chi), the sum over all characters \chi of (\mathbb{Z}/N)^\times. Following Miyake §4.3.

Lean code for Theorem1.3●2 theorems

theoremdefined in LeanModularForms/HeckeRIngs/GL2/CharacterDecomp.lean

complete

theorem HeckeRing.GL2.ModularForm_Gamma1_iSup_charSpace {N : ℕ} [NeZero N]
  (k : ℤ) : ⨆ χ, HeckeRing.GL2.modFormCharSpace k χ = ⊤

theorem HeckeRing.GL2.ModularForm_Gamma1_iSup_charSpace
  {N : ℕ} [NeZero N] (k : ℤ) :
  ⨆ χ,
      HeckeRing.GL2.modFormCharSpace k χ =
    ⊤

**The character subspaces `modFormCharSpace k χ` span the whole space**:
modular forms for `Γ₁(N)` decompose into the span of Nebentypus character
spaces, one for each character `(ZMod N)ˣ →* ℂˣ`.

theoremdefined in LeanModularForms/HeckeRIngs/GL2/CharacterDecomp.lean

complete

theorem HeckeRing.GL2.ModularForm_Gamma1_iSupIndep_charSpace {N : ℕ} [NeZero N]
  (k : ℤ) : iSupIndep fun χ ↦ HeckeRing.GL2.modFormCharSpace k χ

theorem HeckeRing.GL2.ModularForm_Gamma1_iSupIndep_charSpace
  {N : ℕ} [NeZero N] (k : ℤ) :
  iSupIndep fun χ ↦
    HeckeRing.GL2.modFormCharSpace k χ

**The character subspaces form an independent family.**

Proof for Theorem 1.3

uses 0

Each diamond operator has finite order, hence is semisimple, and the diamonds pairwise commute. A commuting family of semisimple operators is simultaneously diagonalisable, so the whole space is the supremum of the joint eigenspaces (the character spaces), and distinct joint eigenspaces are independent.

Definition1.4

uses 0

Used by 4

Reverse dependency previews

Preview

Theorem 1.5

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

For n \ge 1 the Hecke operator T_n on M_k(\Gamma_1(N)) is assembled multiplicatively from its prime-power components T_{p^r}, with T_1 = \mathrm{id}. It restricts to cusp forms as \texttt{heckeT\_n\_cusp}. Following Miyake §4.5 (Theorem 4.5.3).

Lean code for Definition1.4●2 definitions

defdefined in LeanModularForms/HeckeRIngs/GL2/HeckeT_n.lean

complete

def HeckeRing.GL2.heckeT_n {N : ℕ} [NeZero N] (k : ℤ) (n : ℕ) [NeZero n] :
  Module.End ℂ
    (ModularForm
      (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ)
        (CongruenceSubgroup.Gamma1 N))
      k)

def HeckeRing.GL2.heckeT_n {N : ℕ} [NeZero N]
  (k : ℤ) (n : ℕ) [NeZero n] :
  Module.End ℂ
    (ModularForm
      (Subgroup.map
        (Matrix.SpecialLinearGroup.mapGL
          ℝ)
        (CongruenceSubgroup.Gamma1 N))
      k)

**Hecke operator `T_n`** on `M_k(Γ₁(N))` for general `n ∈ ℕ⁺`.

Defined as the product of prime-power components:
`T_n = ∏_{p^v ‖ n} T_{p^v}`, assembled by peeling off `minFac(n)`.

The key algebraic properties (`heckeT_n_mul_coprime`, `heckeT_n_comm`) ensure
this is independent of the factorisation order.

Reference: [DS] §5.3, [Miy] §4.5.

defdefined in LeanModularForms/HeckeRIngs/GL2/AdjointTheory.lean

complete

def HeckeRing.GL2.heckeT_n_cusp {N : ℕ} [NeZero N] (k : ℤ) (n : ℕ)
  [NeZero n]
  (f :
    CuspForm
      (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ)
        (CongruenceSubgroup.Gamma1 N))
      k) :
  CuspForm
    (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ)
      (CongruenceSubgroup.Gamma1 N))
    k

def HeckeRing.GL2.heckeT_n_cusp {N : ℕ}
  [NeZero N] (k : ℤ) (n : ℕ) [NeZero n]
  (f :
    CuspForm
      (Subgroup.map
        (Matrix.SpecialLinearGroup.mapGL
          ℝ)
        (CongruenceSubgroup.Gamma1 N))
      k) :
  CuspForm
    (Subgroup.map
      (Matrix.SpecialLinearGroup.mapGL ℝ)
      (CongruenceSubgroup.Gamma1 N))
    k

`T_n` restricted to cusp forms.

Theorem1.5

uses 1

Used by 2

Reverse dependency previews

Preview

Theorem 2.2

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

For m, n coprime to N the Hecke operators commute, T_m T_n = T_n T_m, and are multiplicative on coprime indices, T_{mn} = T_m T_n when \gcd(m, n) = 1 (Definition 1.4). Following Miyake Theorem 4.5.4.

Lean code for Theorem1.5●2 theorems

theoremdefined in LeanModularForms/HeckeRIngs/GL2/Unified/RingTransport.lean

complete

theorem HeckeRing.GL2.heckeT_n_comm {N : ℕ} [NeZero N] (k : ℤ) (m n : ℕ)
  [NeZero m] [NeZero n] (hm : m.Coprime N) (hn : n.Coprime N) :
  HeckeRing.GL2.heckeT_n k m * HeckeRing.GL2.heckeT_n k n =
    HeckeRing.GL2.heckeT_n k n * HeckeRing.GL2.heckeT_n k m

theorem HeckeRing.GL2.heckeT_n_comm {N : ℕ}
  [NeZero N] (k : ℤ) (m n : ℕ) [NeZero m]
  [NeZero n] (hm : m.Coprime N)
  (hn : n.Coprime N) :
  HeckeRing.GL2.heckeT_n k m *
      HeckeRing.GL2.heckeT_n k n =
    HeckeRing.GL2.heckeT_n k n *
      HeckeRing.GL2.heckeT_n k m

`T_m` and `T_n` commute (for `m, n` coprime to the level `N`) — transported from the
commutative Hecke ring `𝕋(Γ₀(N))`.

theoremdefined in LeanModularForms/HeckeRIngs/GL2/Unified/RingTransport.lean

complete

theorem HeckeRing.GL2.heckeT_n_mul_coprime {N : ℕ} [NeZero N] (k : ℤ) (m n : ℕ)
  [NeZero m] [NeZero n] (hmn : m.Coprime n) (hm : m.Coprime N)
  (hn : n.Coprime N) :
  HeckeRing.GL2.heckeT_n k (m * n) =
    HeckeRing.GL2.heckeT_n k m * HeckeRing.GL2.heckeT_n k n

theorem HeckeRing.GL2.heckeT_n_mul_coprime {N : ℕ}
  [NeZero N] (k : ℤ) (m n : ℕ) [NeZero m]
  [NeZero n] (hmn : m.Coprime n)
  (hm : m.Coprime N) (hn : n.Coprime N) :
  HeckeRing.GL2.heckeT_n k (m * n) =
    HeckeRing.GL2.heckeT_n k m *
      HeckeRing.GL2.heckeT_n k n

Coprime multiplicativity `T_{mn} = T_m T_n` (for `m, n` coprime to the level `N`) —
transported from the ring identity `heckeRingDn_mul_coprime`.

Proof for Theorem 1.5

uses 0

Both identities are transported from the abstract \mathrm{GL}_2 Hecke ring R(\Gamma_0(N), \Delta_0(N)), which is commutative (it is the image of a polynomial ring under the Satake-style presentation), via the ring homomorphism sending the ring generator D_n to T_n.

Theorem1.6

Statement uses 2

Statement dependency previews

Preview

Definition 1.1

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

Used by 2

Reverse dependency previews

Preview

Theorem 2.2

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

The Hecke operators T_n (\gcd(n,N)=1) commute with the diamond operators \langle d \rangle (Definition 1.1, Definition 1.4); in particular each T_n preserves every character space M_k(N, \chi). Following Miyake Theorem 4.5.4(2).

Lean code for Theorem1.6●2 theorems

theoremdefined in LeanModularForms/HeckeRIngs/GL2/Unified/RingTransport.lean

complete

theorem HeckeRing.GL2.heckeT_n_comm_diamondOp {N : ℕ} [NeZero N] (k : ℤ) (n : ℕ)
  [NeZero n] (_hn : n.Coprime N) (d : (ZMod N)ˣ) :
  HeckeRing.GL2.diamondOp k d * HeckeRing.GL2.heckeT_n k n =
    HeckeRing.GL2.heckeT_n k n * HeckeRing.GL2.diamondOp k d

theorem HeckeRing.GL2.heckeT_n_comm_diamondOp
  {N : ℕ} [NeZero N] (k : ℤ) (n : ℕ)
  [NeZero n] (_hn : n.Coprime N)
  (d : (ZMod N)ˣ) :
  HeckeRing.GL2.diamondOp k d *
      HeckeRing.GL2.heckeT_n k n =
    HeckeRing.GL2.heckeT_n k n *
      HeckeRing.GL2.diamondOp k d

`T_n` commutes with the diamond operator `⟨d⟩` (for `n` coprime to the level `N`) —
on each character space the diamond acts by a scalar, so the identity glues from the
character decomposition.

theoremdefined in LeanModularForms/HeckeRIngs/GL2/HeckeT_n.lean

complete

theorem HeckeRing.GL2.heckeT_n_preserves_charSpace {N : ℕ} [NeZero N] (k : ℤ)
  (n : ℕ) [NeZero n] (_hn : n.Coprime N) (χ : (ZMod N)ˣ →* ℂˣ)
  {f :
    ModularForm
      (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ)
        (CongruenceSubgroup.Gamma1 N))
      k}
  (hf : f ∈ HeckeRing.GL2.modFormCharSpace k χ) :
  (HeckeRing.GL2.heckeT_n k n) f ∈ HeckeRing.GL2.modFormCharSpace k χ

theorem HeckeRing.GL2.heckeT_n_preserves_charSpace
  {N : ℕ} [NeZero N] (k : ℤ) (n : ℕ)
  [NeZero n] (_hn : n.Coprime N)
  (χ : (ZMod N)ˣ →* ℂˣ)
  {f :
    ModularForm
      (Subgroup.map
        (Matrix.SpecialLinearGroup.mapGL
          ℝ)
        (CongruenceSubgroup.Gamma1 N))
      k}
  (hf :
    f ∈
      HeckeRing.GL2.modFormCharSpace k
        χ) :
  (HeckeRing.GL2.heckeT_n k n) f ∈
    HeckeRing.GL2.modFormCharSpace k χ

`T_n` preserves the character space `M_k(Γ₁(N), χ)` for `n` coprime to `N`.

A thin wrapper over the general `heckeT_n_preserves_modFormCharSpace_all` (which holds for
**all** `n`); kept under its original name and signature for downstream consumers.

Reference: [DS] Prop 5.2.2(b) generalised.

Proof for Theorem 1.6

uses 0

The diamond operators lie in the same commutative Hecke ring as the T_n, so they commute. Commuting with all \langle d \rangle means T_n preserves each joint diamond eigenspace, i.e. each M_k(N, \chi).