\import Algebra.Group
\import Algebra.Group.Category
\import Algebra.Group.Symmetric
\import Algebra.Linear.Matrix
\import Algebra.Meta
\import Algebra.Module
\import Algebra.Monoid
\import Algebra.Monoid.Category
\import Algebra.Ring
\import Algebra.Ring.RingHom
\import Algebra.Ring.Poly
\import Algebra.Semiring
\import Arith.Fin
\import Data.Array
\import Function.Meta
\import Logic
\import Logic.Meta
\import Meta
\import Paths
\import Paths.Meta
\import Set
\import Set.Fin
\open FinLinearOrder

\func charPoly {R : CRing} {n : Nat} (M : Matrix R n n) : Poly R
  => determinant $ padd   *c matrix-map (padd )  - matrix-map (padd ) M

\lemma charPoly-degree {R : CRing} {n : Nat} (M : Matrix R n n) : degree<= (charPoly M) n
  => degree<=_FinSum \lam j => degree<=_* (transport (degree<= __ ) (sign.sign_hom polyHom) idp) $ later $ degree<=_BigProd1 \lam _ => idp

\lemma charPoly-monic {R : CRing} {n : Nat} (M : Matrix R n n) : polyCoef (charPoly M) n = 
  => AddMonoidHom.func-FinSum polyCoefHom *> AbMonoid.FinSum-unique  (\lam (e : Sym n) e/=id =>
        leadCoef-product (transport (degree<= __ ) (sign.sign_hom polyHom) idp) (degree<=_BigProd1 \lam _ => idp) *>
        pmap (_ *) (pmap (polyCoef _) (inv Semiring.BigSum_replicate) *> leadCoef_BigProd (replicate n ) (\lam _ => idp) *>
                   later (\case FinSet.search (\lam j => e j /= j) (\lam j => decide) \with {
                     | yes (inP (j,ej/=j)) => R.BigProd_zro j $ later $ rewrite (decideEq/=_reduce ej/=j) (zro-left *> ide-left)
                     | no q => absurd $ e/=id $ Sym.equals \lam j => tightness \lam p => q (inP (j,p))
                   })) *> R.zro_*-right) *>
     pmap (\lam x => polyCoef (x * _) n) sign_ide *> pmap (polyCoef __ n) ide-left *> leadCoef_BigProd1 (\lam _ => idp) \lam j => later rewrite (decideEq=_reduce idp) simplify

\lemma charPoly_map {R S : CRing} (f : RingHom R S) {n : Nat} (A : Matrix R n n) : polyMap f (charPoly A) = charPoly (matrix-map f A)
  => unfold charPoly $ determinant_map (polyMapRingHom f) (padd   *c matrix-map (padd )  - matrix-map (padd ) A) *> cong (matrixExt \lam i j =>
      pmap2 (\lam x => padd (padd  x)) (func-+ *> pmap2 (+) f.func-zro (func-* *> pmap2 (*) f.func-ide (later $ mcases \with {
        | yes _ => f.func-ide
        | no _ => f.func-zro
      }))) (func-+ *> pmap2 (+) (func-+ *> pmap2 (+) f.func-zro (func-* *> pmap2 (*) f.func-zro (later $ mcases \with {
        | yes _ => f.func-ide
        | no _ => f.func-zro
      }))) f.func-negative))

\type isEigenvalue {R : Ring} {n : Nat} (A : Matrix R n n) (a : R)
  => ∃ (U : Matrix R n ) (\Pi (x : R) -> x *c U =  -> x = ) (a *c U = A MatrixRing.product U)

-- | An eigenvalue of a matrix is a root of its characteristic polynomial.
\lemma eigen-root {R : CRing} {n : Nat} (A : Matrix R n n) {a : R} (e : isEigenvalue A a) : polyEval (charPoly A) a =  \elim e
  | inP (U,c,p) => determinant_map (polyEvalRingHom a) (padd   *c matrix-map (padd )  - matrix-map (padd ) A) *>
                    cong (matrixExt \lam i j => equation) *> c (determinant (a *c  - A)) (equations-determinant {_} {RingLModule R} (a *c  - A) $
                    product-rdistr (a *c ) (negative A) *> pmap ((a *c ) product U +) product_negative-left *> AddGroup.toZero (inv (MatrixAlgebra.product_*c-comm-left ) *> cong product_ide-left *> p))
  \where \open MatrixRing