A quadratic form forced by per-prime matrix congruences #
Let q and t be integers, thought of as the size of the base field and the trace of Frobenius.
This file shows that an integer D is forced to equal the binary quadratic form
q * r ^ 2 - t * (r * s) + s ^ 2 as soon as, for every prime ℓ other than one exceptional p,
D is realised modulo ℓ as the determinant of the pencil r • M - s • 1 of some 2 × 2 matrix
M over ZMod ℓ with determinant q and trace t.
Nothing about elliptic curves appears here, and none is proved: the matrix data is a
hypothesis throughout. The intended instance — where D is the degree of r π - s for the
q-power Frobenius π, and M is its matrix on the ℓ-torsion — is what makes the conclusion
the Hasse quadratic form, but supplying that instance is the work of the Weil pairing and is not
done here.
Two forms of the hypothesis are provided, because a Weil pairing supplies determinants rather
than traces: one taking M.trace = t directly, and one taking (1 - M).det = q + 1 - t, from
which the trace is read off.
Main results #
eq_quadratic_form_of_det_trace: from per-prime data withdetandtrace.eq_quadratic_form_of_det_det_one_sub: the same fromdetdata alone. When the realised integer is non-negative — as a degree is — non-negativity of the form follows by rewriting,eq_quadratic_form_of_det_trace h ▸ hD; that is left to consumers rather than exported as a corollary.
Provenance #
Ported from the AINTLIB HasseWeil project (Apache-2.0), revision 513e83879e2f, file
HasseWeil/WeilPairing/Reduction.lean, declarations deg_eq_of_frobMatrix_data,
frob_det_congruence and deg_eq_of_frob_det_data.
Three deviations. The source's fourth declaration, qf_nonneg_of_frobMatrix_data, is not
reproduced: it is a one-line ▸ transport of the equality theorem above it that repeats the whole
matrix-data interface to do so, which is why the Main results section above leaves that step to
consumers. The source's det_smul_sub_smul_one_fin_two_of takes M.det = q and
M.trace = t as hypotheses; TauCeti already has the unconditional
Matrix.det_smul_sub_smul_one_fin_two (merged as #2328), so that lemma is used and the
hypotheses are substituted at the call site. And the source's det_one_sub_fin_two is not
reproduced: (1 - M).det = 1 - M.trace + M.det is a three-line computation, kept private here.
The names say what is concluded rather than naming the elliptic-curve instance, since no curve
occurs in any statement.
The per-prime congruence. If M has determinant q, trace t, and the pencil
r • M - s • 1 has determinant D, then D agrees with q * r ^ 2 - t * (r * s) + s ^ 2
modulo ℓ.
The per-prime congruence, from determinants alone. A Weil pairing supplies determinants
rather than traces, so the trace hypothesis is replaced by (1 - M).det = q + 1 - t.
The quadratic form is forced. If for every prime ℓ ≠ p the integer D is realised
modulo ℓ as the pencil determinant of a 2 × 2 matrix with determinant q and trace t, then
D = q * r ^ 2 - t * (r * s) + s ^ 2 as integers.