Characteristic polynomial of a rank-two endomorphism: coefficient criterion #
Theorem statement: LinearMap.charpoly_eq_iff_of_finrank_eq_two
(e04ad550-8399-5638-ab27-356c7b9b79da), by Claude, 2026-09-05.
Proof: submission 5f78c23a-064a-5d75-9f75-3be1d1b3f971, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
Let $R$ be a nontrivial commutative ring and $M$ an $R$-module that is free and finite over $R$,
with $\operatorname{finrank}_R M = 2$. Let $f \colon M \to M$ be an $R$-linear endomorphism and let
$a, b \in R$. The assertion is an equivalence: the characteristic polynomial f.charpoly equals
$X^2 - C(a)\,X + C(b)$ in $R[X]$ (the constants $a$ and $b$ being embedded via the
constant-polynomial map) if and only if both $\operatorname{tr}_{R,M}(f) = a$ and $\det(f) = b$,
where the trace and determinant are the Mathlib trace and determinant of a linear endomorphism of a
finite free module. Thus, in rank two, prescribing the characteristic polynomial in the normalised
shape $X^2 - aX + b$ is the same as prescribing the trace and the determinant of $f$.
This is the rank-two Cayley–Hamilton normalisation in the form of a two-way criterion: it converts a condition on the characteristic polynomial of a two-dimensional representation into the pair of conditions on trace and determinant, and back. It is used in the identification of Frobenius characteristic polynomials on the Tate module of a Weierstrass curve, in the trace–determinant characterisation of when a residual Galois representation is attached to a form, and in the level-lowering step for newforms with a unipotent residual local behaviour.
Explanation of the source proof #
Proof transplanted from the FLT repository: https://github.com/anthropics/fermats-last-theorem/blob/aa2d8b34692b16c70f699536de0d8e75b9a3e9ef/P2M/Sol/S_LinearMap_charpoly_eq_iff_of_finrank_eq_two.lean
<!-- Generated by add_prove2me_provenance.py -->