Translation-normalized parabolic cocycles and their cohomology classes

Definition

MTT_NormalizedParabolicCocycles

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

group-cohomologymodular-formsperiods

Let $N,n$ be natural numbers, let $V_n=\operatorname{Sym}^n(\mathbf C^2)$ carry the MTT left action of $\Gamma_1(N)$ , and put $T=\left(\begin{smallmatrix}1&1\\0&1\end{smallmatrix}\right)$ . The translation belongs to every $\Gamma_1(N)$ . Define the subspace of normalized parabolic cocycles by

Z^1_{\mathrm{par},T}(\Gamma_1(N),V_n)=\{c\in Z^1_{\mathrm{par}}(\Gamma_1(N),V_n):c(T)=0\}.

The canonical linear map from this space to $H^1_{\mathrm{par}}(\Gamma_1(N),V_n)$ sends a cocycle to its class modulo principal cocycles. These definitions isolate the translation-normalization step in the MTT dimension argument. No surjectivity or dimension assertion is part of the definition.

Definition code

import Definitions.Def_MTT_ParabolicCohomology

/-! # Translation-normalized parabolic cocycles -/

noncomputable section

namespace MTT.Cohomology

/-- The standard translation belongs to every Gamma1(N). -/
def gammaOneT (N : ℕ) : CongruenceSubgroup.Gamma1 N :=
  ⟨ModularGroup.T, by
    rw [CongruenceSubgroup.Gamma1_mem]
    norm_num [ModularGroup.T]⟩

/-- Parabolic cocycles normalized to vanish on the standard translation. -/
def normalizedParabolic (N n : ℕ) : Submodule ℂ (parabolicCocycles N n) :=
  LinearMap.ker ((LinearMap.proj (gammaOneT N)).comp (parabolicCocycles N n).subtype)

/-- The canonical map from normalized representatives to parabolic cohomology. -/
def normalizedToH1 (N n : ℕ) : normalizedParabolic N n →ₗ[ℂ] ParabolicH1 N n :=
  (parabolicCoboundaries N n).mkQ.comp (normalizedParabolic N n).subtype

end MTT.Cohomology

Source

The standard parabolic-cocycle normalization at the cusp at infinity; compare Columbia Spring 2021 Eichler-Shimura seminar notes, section 1.1, https://www.math.columbia.edu/~dmarcil/Seminars/2021_Spring/Notes/Week4-5.pdf, and the period-polynomial normalization in Zagier, RIMS Kokyuroku 843 (1993), pp. 162-164. These definitions use the mission's existing parabolic cohomology and exact left coefficient action.

View graph