Dimension of the level-one period relations in terms of elliptic fixed spaces

Proved

MTT.Cohomology.periodRelations_finrank_add_fixed_finranks

by cbirkbeck · Sep 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

group-cohomologymodular-formsperiods

Let $n>0$ be even, $V_n=\operatorname{Sym}^n(\mathbf C^2)$ with the MTT left action $\rho$ , and let $S,T$ be the standard generators of $\mathrm{SL}_2(\mathbf Z)$ . Write $R=ST$ and $W_n=\ker(1+\rho(S))\cap\ker(1+\rho(R)+\rho(R)^2)$ . Then

\dim_{\mathbf C}W_n+\dim_{\mathbf C}V_n^{S}+\dim_{\mathbf C}V_n^{R}=n+1.

Here each fixed space is the kernel of its generator minus the identity. This determines the size of the period-relation space from two finite-order eigenspace counts, and supplies the algebraic dimension comparison needed in the level-one branch of the MTT mission.

Preamble

import Definitions.Def_MTT_LevelOnePeriodRelations
import Mathlib.LinearAlgebra.FiniteDimensional.Defs
set_option autoImplicit false
noncomputable section

Formal statement

theorem MTT.Cohomology.periodRelations_finrank_add_fixed_finranks {n : ℕ} (hn : Even n) (hnpos : 0 < n) :
    Module.finrank ℂ (MTT.Cohomology.periodRelations n) +
      Module.finrank ℂ (((MTT.Cohomology.gammaOneRep 1 n).ρ
        (MTT.Cohomology.levelOneIncl ModularGroup.S)) - LinearMap.id).ker +
      Module.finrank ℂ (((MTT.Cohomology.gammaOneRep 1 n).ρ
        (MTT.Cohomology.levelOneIncl (ModularGroup.S * ModularGroup.T))) - LinearMap.id).ker =
      n + 1 := by sorry

Source

Don Zagier, Periods of modular forms, traces of Hecke operators, and multiple zeta values, RIMS Kokyuroku 843 (1993), pp. 162–164, https://people.mpim-bonn.mpg.de/zagier/files/kokyuroku/843/fulltext.pdf. The formal proof uses a direct coinvariant computation and the dimension formula for the intersection of the two norm kernels, rather than an invariant bilinear pairing. Its translation-invariant polynomial argument adapts the accepted MTT boundary-Hecke proof 2c3fe658-d2de-4575-89b3-ebdfcfd22e7e.

View graph