\import Algebra.Algebra
\import Algebra.Group
\import Algebra.Linear.Matrix
\import Algebra.Linear.Matrix.CharPoly
\import Algebra.Meta
\import Algebra.Module
\import Algebra.Module.FinModule
\import Algebra.Module.LinearMap
\import Algebra.Monoid
\import Algebra.Monoid.Category
\import Algebra.Ring
\import Algebra.Ring.Poly
\import Function.Meta
\import Logic
\import Meta
\import Paths
\import Paths.Meta
\import Set

\lemma cayley-hamilton {R : CRing} {n : Nat} (A : Matrix R n n) : polyMapEval (CAlgebra.coefHom {MatrixAlgebra R n}) (charPoly A) A = 
  => \let | M => polyModule {R} (toLinearMap A)
          | B => padd   *c matrix-map (padd pzero)  - matrix-map (padd pzero) A
          | E => mkColumn MatrixRing.ide
          | toMatrix (X : Matrix M n ) : Matrix R n n => mkMatrix \lam i j => X i  j
          | t => equations-determinant B {E} $
                  MatrixRing.product-gen_negative-rdistr (padd   *c matrix-map (padd pzero) ) (matrix-map (padd pzero) A) {E} *>
                  AddGroup.toZero {MatrixAbGroup M n } {MatrixRing.product-gen (padd   *c matrix-map (padd pzero) ) E} {MatrixRing.product-gen (matrix-map (padd pzero) A) E}
                    (matrixExt \lam i () => AddMonoid.BigSum-unique i (\lam j i/=j => later $ rewrite (decideEq/=_reduce i/=j) $ exts \lam k => simplify $ zro-right *> R.BigSum_zro \lam l => simplify $ pmap (_ *) (R.BigSum_zro \lam _ => R.zro_*-right) *> R.zro_*-right) *>
                    rewrite (decideEq=_reduce idp) (exts \lam k => simplify (R.BigSum-unique i (\lam j i/=j => later $ rewrite (decideEq/=_reduce i/=j) (pmap (_ *) (simplify $ R.BigSum_zro \lam _ => R.zro_*-right) *> R.zro_*-right)) *> later (rewrite (decideEq=_reduce idp, decideEq=_reduce idp) (pmap (_ *) (simplify $ pmap (`+ _) (R.BigSum_zro \lam _ => R.zro_*-right) *> zro-left) *> ide-right *> inv zro-left *> inv (pmap2 (+) (R.BigSum_zro \lam _ => R.zro_*-right) ide-right))) *> inv (R.BigSum-unique k (\lam j k/=j => later $ rewrite (decideEq/=_reduce (/=-sym k/=j)) $ simplify $ R.BigSum_zro \lam _ => R.zro_*-right))) *> inv ArrayLModule.BigSum-index))
     \in matrixExt (poly_func_matrix (charPoly A) A) *> pmap toMatrix t
  \where {
    \func toLinearMap {R : CRing} {n m : Nat} (A : Matrix R n m) : LinearMap (ArrayFinModule n) (ArrayFinModule m) \cowith
      | func u => \lam j => R.BigSum \lam i => A i j * u i
      | func-+ => exts \lam j => pmap R.BigSum (exts \lam i => R.ldistr) *> R.BigSum_+
      | func-*c => exts \lam j => pmap R.BigSum (exts \lam i => equation) *> inv R.BigSum-ldistr

    \lemma poly_func_matrix {R : CRing} {n : Nat} (p : Poly R) (A : Matrix R n n) (i j : Fin n)
      : polyMapEval (CAlgebra.coefHom {MatrixAlgebra R n}) p A i j = polyModule.poly_func p (toLinearMap A) (MatrixRing.ide i) j \elim p
      | pzero => idp
      | padd p e => pmap (`+ _) $ path (\lam i' => R.BigSum \lam k => poly_func_matrix p A i k i' * A k j) *> pmap R.BigSum (exts \lam k => *-comm)
  }