Prove2Me

Algebraic symbols equal normalized signed modular symbols

Open
HorizontalPadicL.algebraicSymbol_eq_signedModularSymbol

by davidloeffler · Sep 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

modular-formsmodular-symbolsnumber-theoryp-adic-l-functions

Expanding the polynomial (mX+a)^j identifies MTT.algebraicSymbol, after applying the complex embedding and multiplying by the appropriate period, with the signed classical modular symbol.

Deprecated. The statement omitted 0 < N, 2 <= k, and nonzero modulus hypotheses needed for the analytic modular-symbol comparison. Use replacement node e7219692-e94e-4394-a006-db87b2f9446a.

Preamble
import Definitions.Def_KN_SeededThetaConstruction

set_option autoImplicit false
noncomputable section
Formal statement
namespace HorizontalPadicL

/-- Expanding `(mX+a)^j` identifies `MTT.algebraicSymbol` with the signed
classical modular symbol after multiplication by the chosen period. -/
theorem algebraicSymbol_eq_signedModularSymbol
    {N k : ℕ} {ι : MTT.Qbar →+* ℂ}
    (f : MTT.Eigenform N k ι) (hnew : IsNewEigenform f)
    (P : MTT.Periods k ι f.form) (s : Bool) (j : ℕ) (a m : ℚ)
    (hj : j ≤ k - 2) :
    ι (MTT.algebraicSymbol P s j a m) * P.omega s =
      signedModularSymbol f.form s j a m := by sorry

end HorizontalPadicL
Source
Mazur--Tate--Teitelbaum modular-symbol period formalism; Kriz--Nordentoft, https://arxiv.org/pdf/2310.20678.

View graph