The twisting character of the χ-twisted Γ₀(N) Hecke ring

Delta0UpperUnit sends an element of Δ₀(N) to the unit its integral witness has in the upper-left corner mod N. Composing with a Dirichlet character χ : (ZMod N)ˣ →* ℂˣ gives

delta0NebentypusChar χ : Δ₀(N) →* ℂˣ

the coefficient the χ-twisted double-coset operator attaches to a monoid element.

It is not an extension of the nebentypus along Γ₀(N) → Δ₀(N), and the direction matters: delta0NebentypusChar_mapGL records that on Γ₀(N) it restricts to the inverse of χ ∘ Gamma0Map, the character modFormCharSpace is defined by. That is the convention rather than an accident — the twisted operator divides by the character, each representative contributing χ(·)⁻¹ • (f ∣[k] ·), so the value attached to a monoid element is the reciprocal of the one attached to a group element acting on forms. It is inherited directly from Delta0UpperUnit_mapGL, where the inverse first appears.

Main definitions

• HeckeRing.GL2.delta0NebentypusChar: the twisting character Δ₀(N) →* ℂˣ.

Main results

• HeckeRing.GL2.delta0NebentypusChar_apply: the defining equation, @[simp]. It is the only route to that equation from outside this file: the definition's body is not exposed, so downstream neither rfl, unfold, simp [delta0NebentypusChar] nor MonoidHom.comp_apply can recover it — but plain simp does, through this lemma.
• HeckeRing.GL2.delta0NebentypusChar_mapGL: on Γ₀(N) it is inverse to χ ∘ Gamma0Map.
• HeckeRing.GL2.delta0NebentypusChar_natDiagGL: its value on a positive natural diagonal.

References

• G. Shimura, Introduction to the arithmetic theory of automorphic functions, §3.5 (Hecke operators with nebentypus).
• Adapted from the AINTLIB LeanModularForms project (Chris Birkbeck), HeckeRIngs/GL2/Unified/TwistedHeckeRing.lean at commit 2baa76f742bdb4fb8ee323fabba41203bd390e08, declaration delta0NebentypusDeltaChar. The source builds the character as a bare MonoidHom with map_one'/map_mul' discharged by hand from its Classical.choose witness API; here those obligations are already carried by Delta0UpperUnit, so the character is a composition.

noncomputable def HeckeRing.GL2.delta0NebentypusChar (N : ℕ) (χ : (ZMod N)ˣ →* ℂˣ) : ↥(Delta0 N) →* ℂˣ

The twisting character of the χ-twisted Γ₀(N) Hecke ring: χ of the upper-left unit of an integral witness. Multiplicativity is inherited from Delta0UpperUnit, which is already a MonoidHom, so no hypothesis is needed on χ beyond being one.

Equations

• HeckeRing.GL2.delta0NebentypusChar N χ = χ.comp (HeckeRing.GL2.Delta0UpperUnit N)

@[simp]

theorem HeckeRing.GL2.delta0NebentypusChar_apply (N : ℕ) (χ : (ZMod N)ˣ →* ℂˣ) (g : ↥(Delta0 N)) : (delta0NebentypusChar N χ) g = χ ((Delta0UpperUnit N) g)

The defining equation: the twisting character is χ of the upper-left unit.

theorem HeckeRing.GL2.delta0NebentypusChar_mapGL (N : ℕ) (χ : (ZMod N)ˣ →* ℂˣ) (γ : ↥(CongruenceSubgroup.Gamma0 N)) : (delta0NebentypusChar N χ) ⟨(Matrix.SpecialLinearGroup.mapGL ℚ) ↑γ, ⋯⟩ = (χ ((CongruenceSubgroup.Gamma0Map N).toHomUnits γ))⁻¹

On Γ₀(N) the twisting character is inverse to the nebentypus. Delta0UpperUnit restricts to the inverse of Gamma0Map there, because ad ≡ 1; applying χ carries the inverse across. Reading this character as an extension of the nebentypus and dropping the inverse would negate every twist downstream.

theorem HeckeRing.GL2.delta0NebentypusChar_natDiagGL (N : ℕ) (χ : (ZMod N)ˣ →* ℂˣ) (a : Fin 2 → ℕ) (ha : ∀ (i : Fin 2), 0 < a i) (haN : (a 0).Coprime N) : (delta0NebentypusChar N χ) ⟨GLn.natDiagGL 2 a, ⋯⟩ = χ (ZMod.unitOfCoprime (a 0) haN)

The twisting character reads a positive natural diagonal from its upper-left entry.