Library charpoly

(c) Copyright Microsoft Corporation and Inria. All rights reserved. 
Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq fintype.
Require Import bigops ssralg matrix poly.

This file contains the definitions of:                                    
 - char_poly A  : Characteristic polynomial of A                          
 - phi : the isomorphism between the rings  M(R[X]) and M(R)[X]           
   with R a commutative and                                               
    M(R[X]) : matrices with coefficients in the polynomial ring of R      
    M(R)[X] : polynomials with coefficients in the matrix ring of R       
 - Zpoly : the injection from the polynomial ring to M(R)[X]              
In addition to the lemmas relevant to these definitions, this file also   
contains a proof of the Cayley-Hamilton Theorem.                          

Import Prenex Implicits.

Import GRing.Theory.
Import Monoid.Theory.

Open Local Scope ring_scope.

Section Cayley.

Variable R : comRingType.

Variable n : pos_nat.

Notation Local nn := (pos_nat_val n) (only parsing).
Notation Local "'R'" := R
  (at level 0, format "'R'").
Notation Local "'R' [ 'X' ]" := {poly R}
  (at level 0, format "'R' [ 'X' ]").
Notation Local "'M' ( 'R' )" := (matrix R nn nn)
  (at level 0, format "'M' ( 'R' )").
Notation Local "'M' ( 'R' [ 'X' ] )" :=
  (matrix (poly_ringType R) nn nn)
  (at level 0, format "'M' ( 'R' [ 'X' ] )").
Notation Local "'M' ( 'R' ) [ 'X' ]" := {poly (matrix R n n)}
  (at level 0, format "'M' ( 'R' ) [ 'X' ]").

The characteristic polynomial 
Open Scope matrix_scope.
Definition matrixC (A : M(R)) : M(R[X]) := \matrix_(i, j) (A i j)%:P.

Definition char_poly (A : M(R)) : R[X] := \det ('X%:M - matrixC A).

The isomorhism phi : M(R[X]) <-> M(R)[X] 

Definition phi (A : M(R[X])) : M(R)[X] :=
  \poly_(k < \max_i \max_j size (A i j)) \matrix_(i, j) (A i j)`_k.

Lemma coef_phi : forall A i j k, (phi A)`_k i j = (A i j)`_k.

Lemma phi_polyC : forall A, phi (matrixC A) = A%:P.

Lemma phi_zero : phi 0 = 0.

Lemma phi_add : forall (A1 A2 : M(R[X])), phi (A1 + A2) = (phi A1) + (phi A2).

Lemma phi_opp : forall A, phi (- A) = - phi A.

Lemma phi_one : phi 1 = 1.

Lemma phi_mul : forall (A1 A2 : M(R[X])), phi (A1 * A2) = (phi A1) * (phi A2).

Writing a polynomial as a polynomial on matrices 

Definition Zpoly (p : R[X]) : M(R)[X] := \poly_(i < size p) (p`_i)%:M.

Lemma coef_Zpoly : forall p k, (Zpoly p)`_k = (p`_k)%:M.

Lemma ZpolyX : Zpoly 'X = 'X.

Lemma phi_Zpoly : forall p, phi p%:M = Zpoly p.

The theorem in three lines! 

Theorem Cayley_Hamilton : forall A, (Zpoly (char_poly A)).[A] = 0.

End Cayley.