Documentation

Mathlib.LinearAlgebra.Matrix.Charpoly.Univ

The universal characteristic polynomial #

In this file we define the universal characteristic polynomial Matrix.charpoly.univ, which is the charactistic polynomial of the matrix with entries Xᵢⱼ, and hence has coefficients that are multivariate polynomials.

It is universal in the sense that one obtains the characteristic polynomial of a matrix M by evaluating the coefficients of univ at the entries of M.

We use it to show that the coefficients of the characteristic polynomial of a matrix are homogeneous polynomials in the matrix entries.

Main results #

source
@[reducible, inline]
noncomputable abbrev Matrix.charpoly.univ (R : Type u_1) (n : Type u_3) [CommRing R] [Fintype n] [DecidableEq n] :
Polynomial (MvPolynomial (n × n) R)

The universal characteristic polynomial for n × n-matrices, is the charactistic polynomial of Matrix.mvPolynomialX n n ℤ with entries Xᵢⱼ.

Its i-th coefficient is a homogeneous polynomial of degree n - i, see Matrix.charpoly.univ_coeff_isHomogeneous.

By evaluating the coefficients at the entries of a matrix M, one obtains the characteristic polynomial of M, see Matrix.charpoly.univ_map_eval₂Hom.

Equations
Instances For
    source
    @[simp]
    theorem Matrix.charpoly.univ_map_eval₂Hom {R : Type u_1} {S : Type u_2} (n : Type u_3) [CommRing R] [CommRing S] [Fintype n] [DecidableEq n] (f : R →+* S) (M : n × n → S) :
    Polynomial.map (MvPolynomial.eval₂Hom f M) (Matrix.charpoly.univ R n) = (Matrix.of (Function.curry M)).charpoly
    source
    theorem Matrix.charpoly.univ_map_map {R : Type u_1} {S : Type u_2} (n : Type u_3) [CommRing R] [CommRing S] [Fintype n] [DecidableEq n] (f : R →+* S) :
    Polynomial.map (MvPolynomial.map f) (Matrix.charpoly.univ R n) = Matrix.charpoly.univ S n
    source
    @[simp]
    theorem Matrix.charpoly.univ_coeff_eval₂Hom {R : Type u_1} {S : Type u_2} (n : Type u_3) [CommRing R] [CommRing S] [Fintype n] [DecidableEq n] (f : R →+* S) (M : n × n → S) (i : ℕ) :
    (MvPolynomial.eval₂Hom f M) ((Matrix.charpoly.univ R n).coeff i) = (Matrix.of (Function.curry M)).charpoly.coeff i
    source
    theorem Matrix.charpoly.univ_monic (R : Type u_1) (n : Type u_3) [CommRing R] [Fintype n] [DecidableEq n] :
    (Matrix.charpoly.univ R n).Monic
    source
    theorem Matrix.charpoly.univ_natDegree (R : Type u_1) (n : Type u_3) [CommRing R] [Fintype n] [DecidableEq n] [Nontrivial R] :
    (Matrix.charpoly.univ R n).natDegree = Fintype.card n
    source
    @[simp]
    theorem Matrix.charpoly.univ_coeff_card (R : Type u_1) (n : Type u_3) [CommRing R] [Fintype n] [DecidableEq n] :
    (Matrix.charpoly.univ R n).coeff (Fintype.card n) = 1
    source
    theorem Matrix.charpoly.optionEquivLeft_symm_univ_isHomogeneous (R : Type u_1) (n : Type u_3) [CommRing R] [Fintype n] [DecidableEq n] :
    ((MvPolynomial.optionEquivLeft R (n × n)).symm (Matrix.charpoly.univ R n)).IsHomogeneous (Fintype.card n)
    source
    theorem Matrix.charpoly.univ_coeff_isHomogeneous (R : Type u_1) (n : Type u_3) [CommRing R] [Fintype n] [DecidableEq n] (i : ℕ) (j : ℕ) (h : i + j = Fintype.card n) :
    ((Matrix.charpoly.univ R n).coeff i).IsHomogeneous j