Level-one period-polynomial relations for the MTT left action

Definition

MTT_LevelOnePeriodRelations

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

group-cohomologymodular-formsperiods

Let $V_n$ be the complex space of homogeneous binary polynomials of degree $n$ , with the existing MTT left substitution action $\rho$ . Put $S=\left(\begin{smallmatrix}0&-1\\1&0\end{smallmatrix}\right)$ , $T=\left(\begin{smallmatrix}1&1\\0&1\end{smallmatrix}\right)$ and $R=ST$ . Define

W_n=\ker(1+\rho(S))\cap\ker(1+\rho(R)+\rho(R)^2)\subseteq V_n.

For even $n$ , these are the two period-polynomial relations arising from $S^2=R^3=-I$ . They describe the possible value at $S$ of a parabolic cocycle normalized to vanish at $T$ , and provide a finite-dimensional relation space for the level-one MTT dimension argument.

Formalization Note The file identifies $\Gamma_1(1)$ with $\mathrm{SL}_2(\mathbf Z)$ and defines the two kernels with the existing coefficient representation. No dimension formula, period theorem, or surjectivity assertion is included.

Definition code

import Definitions.Def_MTT_ParabolicCohomology

/-! # The two Manin relations for the MTT left coefficient action -/

noncomputable section

namespace MTT.Cohomology

/-- At level one, every integral determinant-one matrix is in Gamma1. -/
def levelOneIncl : Matrix.SpecialLinearGroup (Fin 2) ℤ ≃* CongruenceSubgroup.Gamma1 1 where
  toFun g := ⟨g, by
    rw [CongruenceSubgroup.Gamma1_mem]
    exact ⟨Subsingleton.elim _ _, Subsingleton.elim _ _, Subsingleton.elim _ _⟩⟩
  invFun := Subtype.val
  left_inv _ := rfl
  right_inv _ := rfl
  map_mul' _ _ := rfl

/-- Binary homogeneous polynomials satisfying the S and ST period relations. -/
def periodRelations (n : ℕ) : Submodule ℂ (gammaOneRep 1 n) :=
  LinearMap.ker ((gammaOneRep 1 n).ρ (levelOneIncl ModularGroup.S) + LinearMap.id) ⊓
    LinearMap.ker (
      ((gammaOneRep 1 n).ρ (levelOneIncl (ModularGroup.S * ModularGroup.T))) ^ 2 +
      (gammaOneRep 1 n).ρ (levelOneIncl (ModularGroup.S * ModularGroup.T)) + LinearMap.id)

theorem mem_periodRelations_iff {n : ℕ} (P : gammaOneRep 1 n) :
    P ∈ periodRelations n ↔
      (gammaOneRep 1 n).ρ (levelOneIncl ModularGroup.S) P + P = 0 ∧
      (gammaOneRep 1 n).ρ (levelOneIncl (ModularGroup.S * ModularGroup.T))
          ((gammaOneRep 1 n).ρ (levelOneIncl (ModularGroup.S * ModularGroup.T)) P) +
        (gammaOneRep 1 n).ρ (levelOneIncl (ModularGroup.S * ModularGroup.T)) P + P = 0 := by
  simp only [periodRelations, Submodule.mem_inf, LinearMap.mem_ker, LinearMap.add_apply,
    LinearMap.id_apply, pow_two, Module.End.mul_apply]

end MTT.Cohomology

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. This formalization retains the MTT LEFT action and uses R=ST (whose cube is -I), rather than copying the source's right-action notation. The defining relations are independently derived from the cocycle identities in the subsequent theorem proof.

View graph