\import Algebra.Linear.Matrix
\import Algebra.Meta
\import Algebra.Module
\import Algebra.Module.Category
\import Algebra.Module.LinearMap
\import Algebra.Monoid
\import Algebra.Ring
\import Arith.Nat
\import Category
\import Data.Array
\import Equiv
\import Function \hiding (id, o)
\import Function.Meta
\import Logic
\import Logic.Meta
\import Meta
\import Order.PartialOrder
\import Paths
\import Paths.Meta
\import Set
\import Set.Fin

\class FinModule \extends LModule
  | isFinModule : ∃ (l : Array E) (IsBasis l)
  \where {
    \open LinearMap

    \lemma surj-lift {R : Ring} {F : FinModule R} {U V : LModule R} (f : LinearMap F V) (g : LinearMap U V) (gs : isSurj g)
      : ∃ (h : LinearMap F U) ∀ x (g (h x) = f x)
      => \have | (inP (l,lb)) => F.isFinModule
               | (inP s) => FinSet.finiteAC (\lam j => gs (f (l j)))
               | h => extend lb \lam j => (s j).
         \in inP (h, basis-ext (g ∘ h) f lb. \lam j => pmap g (BigSum-unique {_} {\lam k => basis-split lb (l j) k *c (s k).} j (\lam k j/=k => pmap (`*c _) (basis_split_/= j/=k) *> *c_zro-left) *> pmap (`*c _) basis_split_= *> ide_*c) *> (s j).)

    \lemma surj-split {R : Ring} {U : LModule R} {V : FinModule R} (g : LinearMap U V) (gs : isSurj g)
      : ∃ (h : LinearMap V U) ∀ x (g (h x) = x)
      => surj-lift (id {LModuleCat R} V) g gs

    \lemma basis<=generating {R : NonZeroCRing} {U : LModule R} (l l' : Array U) (lb : U.IsBasis l) (l'g : U.IsGenerated l') : l.len <= l'.len
      => \let | g => arrayLinearMap l'
              | (inP (f : LinearMap U _, gf=id)) => surj-split {R} {_} {\new FinModule { | LModule => U | isFinModule => inP (l,lb) }} g (arrayLinearMap.surj-char. l'g)
              | A => toMatrix l ArrayFinModule.basis f
              | B => toMatrix {R} MatrixRing.ide lb g
         \in matrix-split_<= {R} {_} {_} {A} {B} $ inv (toMatrix_* {R} {U} f g l ArrayFinModule.basis lb) *> cong (exts gf=id) *> toMatrix_ide lb

    \lemma dimension-pair {R : NonZeroCRing} (U : FinModule R) : \Sigma (d : Nat) (∃ (l : Array U d) (U.IsBasis l))
      \level \lam s t => ext \case s., t. \with {
        | inP (l,lb), inP (l',l'b) => <=-antisymmetric (basis<=generating l l' lb l'b.) (basis<=generating l' l l'b lb.)
      } => \case U.isFinModule \with {
        | inP (l : Array, lb) => (l.len, inP (\new l, lb))
      }

    \func dimension {R : NonZeroCRing} (U : FinModule R) => (dimension-pair U).

    \lemma dimension-char {R : NonZeroCRing} {U : FinModule R} : ∃ (l : Array U (dimension U)) (U.IsBasis l)
      => (dimension-pair U).

    \lemma dimension-unique {R : NonZeroCRing} {U : FinModule R} {l : Array U} (b : U.IsBasis l) : dimension U = l.len
      => \case dimension-char \with {
           | inP (l',b') => <=-antisymmetric (basis<=generating l' l b' b.) (basis<=generating l l' b b'.)
         }

    \lemma dimension=0 {R : NonZeroCRing} {U : FinModule R} : (dimension U = ) <-> (\Pi (a : U) -> a = )
      => (\lam p a => \case rewrite p in dimension-char \with {
        | inP (l,lb) => basis-split-char {_} {_} {lb}
      }, \lam f => cases (dimension U, dimension-char) \with {
        | , _ => idp
        | suc n, inP (l,lb) => absurd $ R.zro/=ide $ inv $ lb. (replicate (suc n) ( : R)) (f _) 
      })

    \lemma surj-iso {R : NonZeroCRing} {U V : FinModule R} (p : dimension U = dimension V) (g : LinearMap U V) (gs : isSurj g) : Iso {LModuleCat R} g
      => \case dimension-char, dimension-char \with {
        | inP s, inP (lv,bv) => \let (lu,bu) => rewrite p s
                                \in basis-surj-iso bu bv g gs
      }
      \where
        \lemma basis-surj-iso {R : CRing} {U V : LModule R} {n : Nat} {lu : Array U n} (bu : U.IsBasis lu) {lv : Array V n} (bv : V.IsBasis lv) (g : LinearMap U V) (gs : isSurj g) : Iso  g
          => \case surj-split {R} {U} {\new FinModule { | LModule => V | isFinModule => inP (lv,bv) }} g gs \with {
            | inP (h,gh=id) => rewriteI (ret_f {matrix-equiv bu bv} g) $ toLinearMapIso bu bv $ matirx-inv {R} {n} {toMatrix lv bu h} {toMatrix lu bv g} $ inv (toMatrix_* {R} {V} h g lv bu bv) *> cong (exts gh=id) *> toMatrix_ide bv
          }
  }

\instance ArrayFinModule {R : Ring} (n : Nat) : FinModule R (Array R n)
  | LModule => ArrayLModule n (RingLModule R)
  | isFinModule => inP (_, basis)
  \where {
    \lemma basis {R : Ring} {n : Nat} : LModule.IsBasis {ArrayLModule n (RingLModule R)} MatrixRing.ide
      => (\lam c p j => inv ide-right *> (rewrite (decideEq=_reduce idp) in inv (R.BigSum-unique j \lam k j/=k => later $ rewrite (decideEq/=_reduce $ /=-sym j/=k) R.zro_*-right) *> inv ArrayLModule.BigSum-index *> path (\lam i => p i j)),
          \lam x => inP (x, exts \lam j => inv $ ArrayLModule.BigSum-index *> R.BigSum-unique j (\lam k j/=k => later $ rewrite (decideEq/=_reduce $ /=-sym j/=k) R.zro_*-right) *> rewrite (decideEq=_reduce idp) ide-right))
  }