Manin symbols and the modular relations

A Manin symbol is the modular symbol on the oriented edge from g · ∞ to g · 0, for g ∈ SL₂(ℤ). These edges generate the modular-symbol module. Reversing an edge by S gives the two-term relation, and the three edges of the triangle permuted by U = TS give the three-term relation. These and invariance under -1 hold with every homogeneous coefficient polynomial. They are the relations used in a finite Manin-symbol presentation and in the comparison with period polynomials.

References

• Y. I. Manin, Parabolic points and zeta functions of modular curves, 1972.
• W. Stein, Modular Forms: A Computational Approach, §8.2.

noncomputable def TauCeti.ModularSymbols.maninSymbol {R : Type u_1} [CommRing R] (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) {w : ℕ} (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) : ↥(MvPolynomial.homogeneousSubmodule (Fin 2) R w) →ₗ[R] ModularSymbols R Γ w

The Manin symbol represented by the oriented unimodular edge g · ∞ → g · 0, linear in the homogeneous coefficient polynomial.

@[simp]

theorem TauCeti.ModularSymbols.maninSymbol_apply {R : Type u_1} [CommRing R] (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) {w : ℕ} (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) (P : ↥(MvPolynomial.homogeneousSubmodule (Fin 2) R w)) : (maninSymbol Γ g) P = (symbol Γ ((Matrix.SpecialLinearGroup.mapGL ℚ) g • OnePoint.infty) ((Matrix.SpecialLinearGroup.mapGL ℚ) g • ↑0)) P

theorem TauCeti.ModularSymbols.maninSymbol_eq_mk {R : Type u_1} [CommRing R] (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) {w : ℕ} (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) (P : ↥(MvPolynomial.homogeneousSubmodule (Fin 2) R w)) : (maninSymbol Γ g) P = (Representation.Coinvariants.mk (MonoidHom.comp (symbolRep R w) Γ.subtype)) (((degreeZeroRep R) g) ⟨MonoidAlgebra.single OnePoint.infty 1 - MonoidAlgebra.single (↑0) 1, ⋯⟩ ⊗ₜ[R] P)

A Manin symbol is the coinvariant class of the translate of [∞] - [0] tensored with its coefficient polynomial.

theorem TauCeti.ModularSymbols.maninSymbol_mul_of_mem {R : Type u_1} [CommRing R] (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) {w : ℕ} {h : Matrix.SpecialLinearGroup (Fin 2) ℤ} (hh : h ∈ Γ) (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) (P : ↥(MvPolynomial.homogeneousSubmodule (Fin 2) R w)) : (maninSymbol Γ (h * g)) P = (maninSymbol Γ g) (((binaryFormRep R w) (MulOpposite.op ↑h)) P)

The subgroup relation for Manin symbols. Left multiplication of an edge by an element of Γ can be transferred to the right action on its coefficient polynomial.

@[simp]

theorem TauCeti.ModularSymbols.maninSymbol_mul_S {R : Type u_1} [CommRing R] (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) {w : ℕ} (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) : maninSymbol Γ (g * ModularGroup.S) = -maninSymbol Γ g

The two-term Manin relation: right multiplication by S reverses the edge.

@[simp]

theorem TauCeti.ModularSymbols.maninSymbol_neg {R : Type u_1} [CommRing R] (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) {w : ℕ} (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) : maninSymbol Γ (-g) = maninSymbol Γ g

The Manin symbol is unchanged when its matrix is multiplied by the central element -1.

theorem TauCeti.ModularSymbols.maninSymbol_add_mul_T_mul_S_add_mul_T_mul_S_sq {R : Type u_1} [CommRing R] (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) {w : ℕ} (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) : maninSymbol Γ g + maninSymbol Γ (g * (ModularGroup.T * ModularGroup.S)) + maninSymbol Γ (g * (ModularGroup.T * ModularGroup.S) ^ 2) = 0

The three-term Manin relation for the oriented triangle with vertices g · ∞, g · 1, and g · 0.

theorem TauCeti.ModularSymbols.span_maninSymbol_eq_top {R : Type u_1} [CommRing R] (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) {w : ℕ} : Submodule.span R (Set.range fun (x : Matrix.SpecialLinearGroup (Fin 2) ℤ × ↥(MvPolynomial.homogeneousSubmodule (Fin 2) R w)) => (maninSymbol Γ x.1) x.2) = ⊤

The Manin symbols maninSymbol Γ g P, for g ∈ SL(2, ℤ) and homogeneous binary forms P of degree w, span 𝕄_w(Γ; R).