The trace of an integral matrix is integral

Let k be a field which is an R-algebra. A square matrix M over k that is integral over R, in the R-algebra of matrices, has a trace integral over R. Over an algebraic closure the trace is the sum of the roots of the characteristic polynomial; each root lies in the spectrum, so the spectral mapping inclusion makes it a root of any monic polynomial over R killing M.

Over an integrally closed R with fraction field k this places the trace in R, which is how traces of integral elements of a noncommutative finite-dimensional algebra are controlled.

Main results

• Matrix.isIntegral_of_isRoot_charpoly: the roots of the characteristic polynomial of a matrix integral over R are integral over R.
• Matrix.isIntegral_trace: the trace of a matrix integral over R is integral over R.

theorem Matrix.isIntegral_of_isRoot_charpoly {R : Type u_1} {k : Type u_2} {n : Type u_3} [CommRing R] [Field k] [Algebra R k] [Fintype n] [DecidableEq n] {M : Matrix n n k} (hM : IsIntegral R M) {μ : k} (hμ : M.charpoly.IsRoot μ) : IsIntegral R μ

Every root of the characteristic polynomial of a matrix integral over R is integral over R: it lies in the spectrum, so it is killed by every monic polynomial over R killing the matrix.

theorem Matrix.isIntegral_trace {R : Type u_1} {k : Type u_2} {n : Type u_3} [CommRing R] [Field k] [Algebra R k] [Fintype n] [DecidableEq n] {M : Matrix n n k} (hM : IsIntegral R M) : IsIntegral R M.trace

The trace of an integral matrix is integral. If a square matrix M over a field k is integral over R, then so is its trace.