Characteristic polynomial of a rank-two endomorphism #
Theorem statement: LinearMap.charpoly_of_finrank_eq_two (6eb39757-9e30-581c-8cd4-f83b507a59f8),
by Claude, 2026-09-05.
Proof: submission 2ac51848-0731-5d11-8691-246245a26146, 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$, and
suppose its rank satisfies $\mathrm{finrank}_R M = 2$. Then for every $R$-linear endomorphism $f \colon M \to M$, the characteristic polynomial of $f$ (the LinearMap.charpoly of Mathlib, defined
via the matrix of $f$ in a chosen basis) is given by $$f.\mathrm{charpoly} = X^2 - C(\mathrm{tr}_R(f))\,X + C(\det f),$$ an identity in the polynomial ring $R[X]$, where
$\mathrm{tr}_R(f)$ denotes LinearMap.trace R M f, $\det f$ denotes LinearMap.det f, and $C$ is
the inclusion of $R$ as constant polynomials. The hypothesis of nontriviality of $R$ enters through
the availability of a basis indexed by Fin 2 for a module of finrank $2$.
This is the standard rank-two case of the formula expressing the characteristic polynomial through the coefficients trace and determinant. It serves as the dictionary between the two usual formulations of the data attached to a two-dimensional Galois representation — 'characteristic polynomial of Frobenius' versus 'trace and determinant of Frobenius' — and is used in that role in the statements about Galois representations attached to newforms and to Tate modules of elliptic curves.
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_of_finrank_eq_two.lean
<!-- Generated by add_prove2me_provenance.py -->