Binary forms: substitution action and evaluation on the projective line #
Definition: HeckeEis_BinaryFormRep (b7d27b98-8127-543a-b6fd-ba1172da24bf), by Claude,
2026-09-05.
Over a commutative ring $K$, BinaryForm K n abbreviates the degree-$n$ homogeneous component
MvPolynomial.homogeneousSubmodule (Fin 2) K n, i.e. the submodule of $K[X_0,X_1]$ spanned by the
monomials of total degree $n$. For an integral $2\times 2$ matrix $M$, binarySubst K M is the
$K$-algebra endomorphism of $K[X_0,X_1]$ determined by $X_j \mapsto \sum_i (M_{ij} \bmod K)\,X_i$;
in classical notation $F \mapsto F\bigl((X_0,X_1)M\bigr)$, the row-vector convention. It fixes
constants, is the identity for $M = 1$, satisfies $\mathrm{binarySubst}(MM') = \mathrm{binarySubst}(M)\circ\mathrm{binarySubst}(M')$, and maps each BinaryForm K n into itself.
Restricting it therefore gives binaryFormRepSL K n, a representation of $SL_2(\mathbb{Z})$ on the
degree-$n$ binary forms (a model of $\mathrm{Sym}^n$ of the standard rank-two module), and, for a
natural number $\ell$, the $K$-linear endomorphism binaryFormAlphaAdj K n ℓ given by substitution
of $\mathrm{diag}(\ell,1)$, that is $F(X_0,X_1)\mapsto F(\ell X_0, X_1)$.
In the second part $p$ is a prime and $K$ a commutative ring of characteristic $p$. For $F \in K[X_0,X_1]$ and a unimodular row $v = (a,c)$ over $\mathbb{Z}/p$ (a pair with $xa+yc=1$ for some
$x,y$), evalRow p K F v is the value of $F$ at the images of $a$ and $c$ in $K$ under
ZMod.castHom. When $F$ is homogeneous of degree $p-1$, this value is unchanged if $v$ is rescaled
by a unit of $\mathbb{Z}/p$, since such a unit satisfies $u^{p-1}=1$; accordingly binaryFormEval p K is the $K$-linear map from BinaryForm K (p-1) to functions on the projective line
$\mathbb{P}^1(\mathbb{Z}/p)$ — the quotient of unimodular rows by unit scaling — whose value on the
class of $v=(a,c)$ is $F(a,c)$. A general auxiliary identity records $F(c\,x) = c^n F(x)$ for $F$
homogeneous of degree $n$ over any commutative ring.
Relation to Mathlib. BinaryForm is an abbreviation for Mathlib's
MvPolynomial.homogeneousSubmodule, binarySubst is Mathlib's MvPolynomial.aeval for a linear
substitution, and the group actions are packaged as Mathlib Representations; the index set
$\mathbb{P}^1(\mathbb{Z}/p)$ is the project's own quotient of unimodular rows, not a Mathlib
projectivization.
Where it is used. These two coefficient modules, $\mathrm{Sym}^{p-1}$ in characteristic $p$ and the functions on $\mathbb{P}^1(\mathbb{F}_p)$, together with the evaluation map intertwining the $SL_2(\mathbb{Z})$-actions and the $\mathrm{diag}(\ell,1)$ operators, provide the dictionary between weight $p+1$ at level $N$ and weight $2$ at level $Np$ that is used in the mod-$p$ weight and level comparisons of the argument.
<!-- Generated by add_prove2me_provenance.py -->
The module of homogeneous polynomials of degree n in two variables over K.
Equations
- HeckeEis.BinaryForm K n = MvPolynomial.homogeneousSubmodule (Fin 2) K n
Instances For
Substitution of the linear forms given by the columns of an integral two-by-two matrix.
Equations
- HeckeEis.binarySubst K M = MvPolynomial.aeval fun (j : Fin 2) => ∑ i : Fin 2, MvPolynomial.C ↑(M i j) * MvPolynomial.X i
Instances For
The representation of SL(2, ℤ) on degree-n binary forms by linear substitution.
Equations
- HeckeEis.binaryFormRepSL K n = { toFun := fun (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) => (HeckeEis.binarySubst K ↑g).toLinearMap.restrict ⋯, map_one' := ⋯, map_mul' := ⋯ }
Instances For
The linear substitution on binary forms associated to diag(ℓ, 1).
Equations
- HeckeEis.binaryFormAlphaAdj K n ℓ = (HeckeEis.binarySubst K !![↑ℓ, 0; 0, 1]).toLinearMap.restrict ⋯
Instances For
Evaluation of a binary polynomial at a unimodular row modulo p, with coordinates cast into
K.
Equations
- HeckeEis.evalRow p K F v = (MvPolynomial.eval ![(ZMod.castHom ⋯ K) (↑v).1, (ZMod.castHom ⋯ K) (↑v).2]) F
Instances For
Evaluation of degree-p - 1 binary forms as functions on the projective line over ZMod p.
Equations
- HeckeEis.binaryFormEval p K = { toFun := fun (F : ↥(HeckeEis.BinaryForm K (p - 1))) => Quotient.lift (HeckeEis.evalRow p K ↑F) ⋯, map_add' := ⋯, map_smul' := ⋯ }