\import Algebra.Linear.Matrix
\import Algebra.Linear.Matrix.Smith
\import Algebra.Meta
\import Algebra.Module
\import Algebra.Module.LinearMap
\import Algebra.Monoid
\import Algebra.Monoid.MonoidHom
\import Algebra.Ring
\import Data.Array
\import Equiv
\import Function
\import Function.Meta
\import Logic
\import Paths
\import Paths.Meta
\open LinearMap

\record ModuleIso {R : Ring} {U V : LModule R} (f : LinearMap U V) (finv : LinearMap V U)
                  (finv_f : \Pi (x : U) -> finv (f x) = x)
                  (f_finv : \Pi (y : V) -> f (finv y) = y) {

  \protected \func reverse : ModuleIso
    => \new ModuleIso finv f f_finv finv_f

  \protected \lemma isInj : IsInj f
    => \lam {u} {u'} p => inv (finv_f u) *> pmap finv p *> finv_f u'

  \protected \lemma isSurj : IsSurj f
    => \lam v => inP (finv v, f_finv v)
} \where {
  \use \func equals {R : Ring} {U V : LModule R} (e e' : ModuleIso {R} {U} {V}) (p : e.f = e'.f) : e = e'
    => ext (p, exts \lam y => pmap e.finv (inv $ path (\lam i => p i (e'.finv y)) *> f_finv y) *> finv_f _)

  \use \level levelProp {R : Ring} {U V : LModule R} (f : LinearMap U V) (e e' : ModuleIso f)
    => equals e e' idp

  \lemma iso<->inj+surj {R : Ring} {U V : LModule R} {f : LinearMap U V} : ModuleIso f <-> (\Sigma (IsInj f) (IsSurj f))
    => (\lam e => (e.isInj, e.isSurj),
        \lam s =>
          \let e : QEquiv f => QEquiv.fromInjSurj s. s.
          \in \new ModuleIso {
            | finv => \new LinearMap {
              | func => e.ret
              | func-+ => e.isInj $ e.f_ret _ *> inv (pmap2 (+) (e.f_ret _) (e.f_ret _)) *> inv f.func-+
              | func-*c => e.isInj $ e.f_ret _ *> pmap (_ *c) (inv (e.f_ret _)) *> inv f.func-*c
            }
            | finv_f => e.ret_f
            | f_finv => e.f_ret
          })
}

\func toLinearMapIso {R : Ring} {U V : LModule R} {n : Nat} {lu : Array U n} (bu : U.IsBasis lu) {lv : Array V n} (bv : V.IsBasis lv) (A : Monoid.Inv {MatrixRing R n}) : ModuleIso {R} {U} {V} \cowith
  | f => toLinearMap bu lv A.val
  | finv => toLinearMap bv lu A.inv
  | finv_f x => path \lam i => (inv (toLinearMap_* A.val A.inv bu bv bu) *> {LinearMap U U} cong A.inv-right *> toLinearMap_ide bu) i x
  | f_finv y => path \lam i => (inv (toLinearMap_* A.inv A.val bv bu bv) *> {LinearMap V V} cong A.inv-left *> toLinearMap_ide bv) i y

\func toMatrixInv {R : Ring} {U V : LModule R} {n : Nat} {lu : Array U n} (bu : U.IsBasis lu) {lv : Array V n} (bv : V.IsBasis lv) (e : ModuleIso {R} {U} {V}) : Monoid.Inv {MatrixRing R n} \cowith
  | val => toMatrix lu bv e.f
  | inv => toMatrix lv bu e.finv
  | inv-left => inv (toMatrix_* e.finv e.f lv bu bv) *> pmap (toMatrix lv bv) (exts e.f_finv) *> toMatrix_ide bv
  | inv-right => inv (toMatrix_* e.f e.finv lu bv bu) *> pmap (toMatrix lu bu) (exts e.finv_f) *> toMatrix_ide bu

\lemma iso-basis {R : Ring} {U V : LModule R} (f : ModuleIso {R} {U} {V}) {l : Array U} (lb : U.IsBasis l) : V.IsBasis (map f.f l)
  => (\lam c p j => lb. c (f.isInj $ f.f.func-BigSum *> pmap AddMonoid.BigSum (exts \lam j => func-*c) *> p *> inv f.f.func-zro) j,
      \lam v => TruncP.map (lb. (f.finv v)) \lam s => (s., f.reverse.isInj $ s. *> pmap AddMonoid.BigSum (exts \lam j => inv $ func-*c *> pmap (_ *c) (f.finv_f (l j))) *> inv AddMonoidHom.func-BigSum))

\lemma change-basis-right {R : Ring} {U V W : LModule R} (f : ModuleIso {R} {U} {V}) {lv : Array V} {lw : Array W} (bv : V.IsBasis lv) (bw : W.IsBasis lw) (A : Matrix R lv.len lw.len)
  : toLinearMap bv lw A LinearMap.∘ f.f = toLinearMap (iso-basis f.reverse bv) lw A
  => exts \lam u => pmap AddMonoid.BigSum $ exts \lam j => pmap (*c _) $ V.basis-split-unique bv _ (pmap f.f (U.basis-split-char {_} {iso-basis f.reverse bv}) *> AddMonoidHom.func-BigSum *> pmap AddMonoid.BigSum (exts \lam k => func-*c *> pmap (_ *c) (f.f_finv (lv k)))) j

\func basis-iso {R : Ring} {U V : LModule R} {n : Nat} {lu : Array U n} (bu : U.IsBasis lu) {lv : Array V n} (bv : V.IsBasis lv) : ModuleIso {R} {U} {V} \cowith
  | f => extend bu lv
  | finv => extend bv lu
  | finv_f => basis-ext (extend bv lu LinearMap.∘ extend bu lv) LinearMap.id bu. \lam j => pmap (extend bv lu) (extend-char bu lv j) *> extend-char bv lu j
  | f_finv => basis-ext (extend bu lv LinearMap.∘ extend bv lu) LinearMap.id bv. \lam j => pmap (extend bu lv) (extend-char bv lu j) *> extend-char bu lv j

\lemma change-basis_matrix-left {R : Ring} {U V : LModule R} (f : LinearMap U V) {n : Nat} {lu lu' : Array U n} (bu : U.IsBasis lu) (bu' : U.IsBasis lu') {lv : Array V} (bv : V.IsBasis lv)
  : toMatrix lu bu (basis-iso bu' bu).f MatrixRing.product toMatrix lu' bv f = toMatrix lu bv f
  => inv $ (matrix-equiv bu bv).adjointInv $ inv $ toLinearMap_* (toMatrix lu bu (extend bu' lu)) (toMatrix lu' bv f) bu bu' bv *>
      pmap2 (LinearMap.∘) ((matrix-equiv bu' bv).ret_f f) {_} {LinearMap.id} (exts \lam u => toLinearMap_toMatrix-right bu bu bu' *> pmap AddMonoid.BigSum (exts \lam j => pmap (*c _) $ U.basis-split-unique bu _ idp j) *> inv (U.basis-split-char {lu'} {bu'}))

\lemma change-basis_matrix-right {R : Ring} {U V : LModule R} (f : LinearMap U V) {lu : Array U} (bu : U.IsBasis lu) {n : Nat} {lv lv' : Array V n} (bv : V.IsBasis lv) (bv' : V.IsBasis lv')
  : toMatrix lu bv' f MatrixRing.product toMatrix lv bv (basis-iso bv bv').f = toMatrix lu bv f
  => inv $ (matrix-equiv bu bv).adjointInv $ inv $ toLinearMap_* (toMatrix lu bv' f) (toMatrix lv bv (extend bv lv')) bu bv' bv *>
      pmap2 (LinearMap.∘) {_} {LinearMap.id} (exts \lam u => toLinearMap_toMatrix-left bv bv' *> pmap AddMonoid.BigSum (exts \lam j => pmap (*c _) $ V.basis-split-unique bv _ idp j) *> inv (V.basis-split-char {lv'} {bv'})) ((matrix-equiv bu bv').ret_f f)

\lemma change-basis_M~ {R : Ring} {U V : LModule R} (f : LinearMap U V) {n m : Nat} {lu lu' : Array U n} (bu : U.IsBasis lu) (bu' : U.IsBasis lu') {lv lv' : Array V m} (bv : V.IsBasis lv) (bv' : V.IsBasis lv') : toMatrix lu bv f M~ toMatrix lu' bv' f
  => inP (toMatrixInv bu' bu' (basis-iso bu bu'), toMatrixInv bv' bv' (basis-iso bv' bv), inv $ pmap (MatrixRing.product toMatrix lv' bv' (extend bv' lv)) (change-basis_matrix-left f bu' bu bv) *> change-basis_matrix-right f bu' bv' bv)