\import Algebra.Group
\import Algebra.Group.Category
\import Algebra.Linear.Matrix
\import Algebra.Linear.Matrix.Smith (M~)
\import Algebra.Meta
\import Algebra.Module
\import Algebra.Module.Category
\import Algebra.Monoid
\import Algebra.Monoid.Category
\import Algebra.Ring
\import Algebra.Semiring
\import Arith.Fin
\import Arith.Nat
\import Category
\import Data.Array
\import Data.Fin (nat_fin_=)
\import Data.Or
\import Equiv
\import Function \hiding (id, o)
\import Function.Meta
\import HLevel
\import Logic
\import Meta
\import Order.LinearOrder
\import Paths
\import Paths.Meta
\import Set
\import Set.Fin
\open AddMonoid

\record LinearMap {R : Ring} \extends AddGroupHom {
  \override Dom : LModule R
  \override Cod : LModule R
  | func-*c {r : R} {x : Dom} : func (r *c x) = r *c func x

  \lemma linearComb {c : Array R} {l : Array Dom c.len} : func (BigSum (\lam j => c j *c l j)) = BigSum (\lam j => c j *c func (l j)) \elim c, l
    | nil, nil => func-zro
    | b :: c, a :: l => unfold BigSum $ func-+ *> pmap2 (+) func-*c linearComb

  \lemma inj->independent {l : Array Dom} (li : LModule.IsIndependent (map func l)) (inj : isInj func) : LModule.IsIndependent l
    => \lam c p j => li c (inv (linearComb {_} {c}) *> pmap func p *> func-zro) j

  \lemma IsIndependentSet_func {J : \Set} {g : J -> Dom} (fgi : LModule.IsIndependentSet (\lam j => func (g j))) : LModule.IsIndependentSet g
    => \lam c p => fgi c $ inv (func-BigSum *> pmap BigSum (exts \lam j => func-*c)) *> pmap func p *> func-zro

  \lemma IsIndependentDec_func {J : DecSet} {g : J -> Dom} (fgi : LModule.IsIndependentDec (\lam j => func (g j))) : LModule.IsIndependentDec g
    => LModule.IsIndependentSet<->IsIndependentDec. $ IsIndependentSet_func $ LModule.IsIndependentSet<->IsIndependentDec. fgi

  \lemma IsIndependentSet-inj {J : \Set} (inj : isInj func) {g : J -> Dom} (gi : LModule.IsIndependentSet g) : LModule.IsIndependentSet (\lam j => func (g j))
    => \lam c p => gi c $ inj $ func-BigSum *> pmap BigSum (exts \lam j => func-*c) *> p *> inv func-zro
} \where {
  \lemma extend-unique {R : Ring} {U V : LModule R} {l : Array U} (lb : U.IsBasis l) (lv : Array V l.len) : isProp (\Sigma (f : LinearMap U V) (\Pi (j : Fin l.len) -> f (l j) = lv j))
    => \lam t s => ext $ exts \lam u => rewrite (U.basis-split-char {_} {lb}) $ func-BigSum *> pmap BigSum (exts \lam j => func-*c *> pmap (_ *c) (t. j *> inv (s. j)) *> inv func-*c) *> inv func-BigSum

  \func extend {R : Ring} {U V : LModule R} {l : Array U} (lb : U.IsBasis l) (lv : Array V l.len) : LinearMap U V \cowith
    | func x => BigSum (\lam j => U.basis-split lb x j *c lv j)
    | func-+ {x} {y} => pmap BigSum (exts \lam j => pmap (`*c _) (U.basis-split-unique lb (\lam j => U.basis-split lb x j + U.basis-split lb y j) (pmap2 (+) U.basis-split-char (U.basis-split-char {_} {lb}) *> inv (U.BigSum_+ {_} {\lam j => U.basis-split lb x j *c l j}) *> pmap BigSum (exts \lam j => inv U.*c-rdistr)) j) *> *c-rdistr) *> V.BigSum_+ {_} {\lam j => U.basis-split lb x j *c lv j}
    | func-*c {r} {x} => pmap BigSum (exts \lam j => pmap (`*c _) (U.basis-split-unique lb (\lam j => r * U.basis-split lb x j) (pmap (r *c) (U.basis-split-char {_} {lb}) *> U.*c_BigSum-ldistr *> pmap BigSum (exts \lam j => inv *c-assoc)) j) *> *c-assoc) *> inv V.*c_BigSum-ldistr

  \lemma extend-char {R : Ring} {U V : LModule R} {l : Array U} (lb : U.IsBasis l) (lv : Array V l.len) (j : Fin l.len) : extend lb lv (l j) = lv j
    => V.BigSum-unique {\lam k => U.basis-split lb (l j) k *c lv k} j (\lam k j/=k => pmap (`*c _) (U.basis_split_/= j/=k) *> V.*c_zro-left) *> pmap (`*c _) U.basis_split_= *> ide_*c

  \lemma basis-ext {R : Ring} {U V : LModule R} (f g : LinearMap U V) {l : Array U} (lb : U.IsGenerated l) (p : \Pi (j : Fin l.len) -> f (l j) = g (l j)) (u : U) : f u = g u
    => \case lb u \with {
         | inP (c,q) => rewrite q $ f.func-BigSum *> pmap BigSum (exts \lam j => f.func-*c *> pmap (c j *c) (p j) *> inv g.func-*c) *> inv g.func-BigSum
       }

  \open LModule.IsIndependentSet

  \func extendSet {R : Ring} {U V : LModule R} {J : \Set} {u : J -> U} (ub : U.IsBasisSet u) (v : J -> V) : LinearMap U V \cowith
    | func x => (LModule.basisSet-split ub v x).
    | func-+ {x} {y} => \case (LModule.basisSet-split ub v (x + y))., (LModule.basisSet-split ub v x)., (LModule.basisSet-split ub v y). \with {
      | inP c1, inP c2, inP c3 => c1. *> ~_= v (=_~ ub. $ inv c1. *> pmap2 (+) c2. c3. *> inv (sum_++ u)) *> sum_++ v *> inv (pmap2 (+) c2. c3.)
    }
    | func-*c {r} {x} => \case (LModule.basisSet-split ub v (r *c x))., (LModule.basisSet-split ub v x). \with {
      | inP c1, inP c2 => c1. *> ~_= v (=_~ ub. (later $ inv c1. *> pmap (r *c) c2. *> sum-ldistr u)) *> inv (sum-ldistr v) *> pmap (r *c) (inv c2.)
    }

  \lemma extendSet-char {R : Ring} {U V : LModule R} {J : \Set} {u : J -> U} {ub : U.IsBasisSet u} {v : J -> V} {j : J} : extendSet ub v (u j) = v j
    => \case (LModule.basisSet-split ub v (u j)). \with {
         | inP c => c. *> ~_= v {c.} {(,j) :: nil} (=_~ ub. $ inv $ zro-right *> ide_*c *> c.) *> zro-right *> ide_*c
       }

  \lemma extendSet-unique {R : Ring} {U V : LModule R} (f g : LinearMap U V) {J : \Set} {u : J -> U} {ub : U.IsGeneratingSet u} (p : \Pi (j : J) -> f (u j) = g (u j)) (x : U) : f x = g x
    => \case ub x \with {
         | inP c => rewrite c. $ func-BigSum *> pmap BigSum (exts \lam j => func-*c *> pmap (_ *c) (p (c. j).) *> inv func-*c) *> inv func-BigSum
       }

  \func toMatrix {R : Ring} {U V : LModule R} {lv : Array V} (lu : Array U) (bv : V.IsBasis lv) (f : LinearMap U V) : Matrix R lu.len lv.len
    => mkMatrix \lam i => V.basis-split bv $ f (lu i)

  \lemma toMatrix_ide {R : Ring} {U : LModule R} {l : Array U} (lb : U.IsBasis l) : toMatrix l lb (id U) = 
    => matrixExt \lam i j => U.basis_split_basis

  \lemma toMatrix_* {R : Ring} {U V W : LModule R} (f : LinearMap U V) (g : LinearMap V W) {lv : Array V} {lw : Array W} (lu : Array U) (bv : V.IsBasis lv) (bw : W.IsBasis lw)
    : toMatrix lu bw (g ∘ f) = toMatrix lu bv f MatrixRing.product toMatrix lv bw g
    => matrixExt \lam i j =>
        \let h j : Array R lv.len => \lam k => V.basis-split bv (f (lu i)) k R.* W.basis-split bw (g (lv k)) j
        \in W.basis-split-unique bw (\lam j => BigSum (h j)) (pmap g (V.basis-split-char {lv} {bv}) *> g.linearComb {V.basis-split bv (f (lu i))} *> pmap BigSum (exts \lam j => pmap (_ *c) (W.basis-split-char {lw} {bw}) *> W.*c_BigSum-ldistr *> pmap BigSum (exts \lam k => inv *c-assoc)) *> W.BigSum-transpose _ *> inv (path (\lam i' => BigSum (\new Array W lw.len \lam j => W.*c_BigSum-rdistr {\new Array R lv.len (h j)} {lw j} i')))) j

  \func toLinearMap {R : Ring} {U V : LModule R} {lu : Array U} (bu : U.IsBasis lu) (lv : Array V) (A : Matrix R lu.len lv.len) : LinearMap U V
    => extend bu \lam j => MatrixRing.product-gen A (mkColumn lv) j 

  \lemma toLinearMap-basis {R : Ring} {U V : LModule R} {lu : Array U} (bu : U.IsBasis lu) (lv : Array V) {A : Matrix R lu.len lv.len} {i : Fin lu.len}
    : toLinearMap bu lv A (lu i) = BigSum (\lam j => A i j *c lv j)
    => extend-char bu (MatrixRing.product-gen A (mkColumn lv) __ ) i

  \lemma toLinearMap_toMatrix-left {R : Ring} {U V : LModule R} {n : Nat} {lu lu' : Array U n} (bu : U.IsBasis lu) (bu' : U.IsBasis lu') {lv : Array V} {bv : V.IsBasis lv} {f : LinearMap U V} {u : U}
    : toLinearMap bu' lv (toMatrix lu bv f) u = f (extend bu' lu u)
    => inv $ func-BigSum *> pmap BigSum (exts \lam j => func-*c *> pmap (_ *c) V.basis-split-char)

  \lemma toLinearMap_toMatrix-right {R : Ring} {U V : LModule R} {n : Nat} {lu : Array U} (bu : U.IsBasis lu) {lv lv' : Array V n} (bv : V.IsBasis lv) (bv' : V.IsBasis lv') {f : LinearMap U V} {u : U}
    : toLinearMap bu lv' (toMatrix lu bv f) u = extend bv lv' (f u)
    => path (\lam i => BigSum (\lam j => V.*c_BigSum-ldistr {U.basis-split bu u j} {\lam k => V.basis-split bv (f (lu j)) k *c lv' k} i)) *>
        V.BigSum-transpose _ *> pmap BigSum (exts \lam j => pmap BigSum (exts \lam j => inv V.*c-assoc) *>
          inv (V.*c_BigSum-rdistr {\lam k => U.basis-split bu u k * V.basis-split bv (f (lu k)) j}) *> pmap (`*c _) (inv $ V.basis-split-unique bv (\lam k => BigSum (\lam j => U.basis-split bu u j * V.basis-split bv (f (lu j)) k))
            (pmap f (U.basis-split-char {lu} {bu}) *> func-BigSum *> pmap BigSum (exts \lam j => func-*c *> pmap (*c _) (V.basis-split-char {lv} {bv}) *> V.*c_BigSum-ldistr *> pmap BigSum (exts \lam k => inv *c-assoc)) *>
              V.BigSum-transpose _ *> inv (path (\lam i => BigSum \lam j => V.*c_BigSum-rdistr {\lam k => U.basis-split bu u k * V.basis-split bv (f (lu k)) j} {lv j} i))) j))

  \func matrix-equiv {R : Ring} {U V : LModule R} {lu : Array U} {lv : Array V} (bu : U.IsBasis lu) (bv : V.IsBasis lv)
    : Equiv {LinearMap U V} {Matrix R lu.len lv.len}
    => \new QEquiv {
      | f => toMatrix lu bv __
      | ret => toLinearMap bu lv
      | ret_f f => exts \lam u => toLinearMap_toMatrix-left bu bu *> pmap f (basis-ext (extend bu \new lu) (id U) bu. (\lam j => inv U.basis-split-char) u)
      | f_sec A => matrixExt \lam i j => pmap (V.basis-split bv __ j) (V.BigSum-unique {\lam j => U.basis-split bu (lu i) j *c BigSum (\lam k => A j k *c lv k)} i (\lam k i/=k => pmap (`*c _) (U.basis_split_/= i/=k) *> V.*c_zro-left) *> pmap (`*c _) U.basis_split_= *> ide_*c) *> V.basis-split-unique bv (A i) idp j
    }

  \lemma toLinearMap_ide {R : Ring} {U : LModule R} {l : Array U} (lb : U.IsBasis l) : toLinearMap lb l MatrixRing.ide = id U
    => Equiv.isInj {matrix-equiv lb lb} $ f_sec {matrix-equiv lb lb} MatrixRing.ide *> inv (toMatrix_ide lb)

  \lemma toLinearMap_* {R : Ring} {U V W : LModule R} {lu : Array U} {lv : Array V} {lw : Array W} (A : Matrix R lu.len lv.len) (B : Matrix R lv.len lw.len) (bu : U.IsBasis lu) (bv : V.IsBasis lv) (bw : W.IsBasis lw)
    : toLinearMap bu lw (A MatrixRing.product B) = toLinearMap bv lw B ∘ toLinearMap bu lv A
    => Equiv.isInj {matrix-equiv bu bw} $ f_sec {matrix-equiv bu bw} (A MatrixRing.product B) *> inv (pmap2 (MatrixRing.product) (f_sec {matrix-equiv bu bv} A) (f_sec {matrix-equiv bv bw} B)) *> inv (toMatrix_* (toLinearMap bu lv A) (toLinearMap bv lw B) lu bv bw)

  \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}) : Iso {_} {U} {V} \cowith
    | f => toLinearMap bu lv A.val
    | hinv => toLinearMap bv lu A.inv
    | hinv_f => inv (toLinearMap_* A.val A.inv bu bv bu) *> cong A.inv-right *> toLinearMap_ide bu
    | f_hinv => inv (toLinearMap_* A.inv A.val bv bu bv) *> cong A.inv-left *> toLinearMap_ide bv

  \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 : Iso {_} {U} {V}) : Monoid.Inv {MatrixRing R n} \cowith
    | val => toMatrix lu bv e.f
    | inv => toMatrix lv bu e.hinv
    | inv-left => inv (toMatrix_* e.hinv e.f lv bu bv) *> pmap (toMatrix lv bv) e.f_hinv *> toMatrix_ide bv
    | inv-right => inv (toMatrix_* e.f e.hinv lu bv bu) *> pmap (toMatrix lu bu) e.hinv_f *> toMatrix_ide bu

  \lemma iso<->inj+surj {R : Ring} {U V : LModule R} {f : LinearMap U V} : Iso f <-> (\Sigma (isInj f) (isSurj f))
    => (\lam e => (\lam {u} {u'} p => inv (path (\lam i => hinv_f {e} i u)) *> pmap (hinv {e}) p *> path (\lam i => hinv_f {e} i u'),
                   \lam v => inP (hinv {e} v, path (\lam i => f_hinv {e} i v))),
        \lam s => \let e : Equiv f => Equiv.fromInjSurj f s. s.
                  \in \new Iso {
                    | hinv => \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
                    }
                    | hinv_f => exts e.ret_f
                    | f_hinv => exts e.f_ret
                  })

  \lemma iso-basis {R : Ring} {U V : LModule R} (f : Iso {_} {U} {V}) {l : Array U} (lb : U.IsBasis l) : V.IsBasis (map f.f l)
    => (\lam c p j => lb. c ((iso<->inj+surj. f). $ func-BigSum *> pmap BigSum (exts \lam j => func-*c) *> p *> inv func-zro) j,
        \lam v => TruncP.map (lb. (f.hinv v)) \lam s => (s., (iso<->inj+surj. f.reverse). $ s. *> pmap BigSum (exts \lam j => inv $ func-*c *> path (\lam i => _ *c f.hinv_f i (l j))) *> inv func-BigSum))

  \lemma change-basis-left {R : Ring} {U V W : LModule R} (f : LinearMap V W) {lu : Array U} {lv : Array V} (bu : U.IsBasis lu) (bv : V.IsBasis lv) (A : Matrix R lu.len lv.len)
    : f ∘ toLinearMap bu lv A = toLinearMap bu (map f lv) A
    => exts \lam u => func-BigSum *> pmap BigSum (exts \lam j => func-*c *> pmap (_ *c) (func-BigSum *> pmap BigSum (exts \lam k => func-*c)))

  \lemma change-basis-right {R : Ring} {U V W : LModule R} (f : Iso {_} {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 ∘ f.f = toLinearMap (iso-basis f.reverse bv) lw A
    => exts \lam u => pmap BigSum $ exts \lam j => pmap (`*c _) $ V.basis-split-unique bv _ (pmap f.f (U.basis-split-char {_} {iso-basis f.reverse bv}) *> func-BigSum *> pmap BigSum (exts \lam k => func-*c *> path (\lam i => _ *c f.f_hinv i (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) : Iso {_} {U} {V} \cowith
    | f => extend bu lv
    | hinv => extend bv lu
    | hinv_f => exts $ basis-ext (extend bv lu ∘ extend bu lv) (id U) bu. \lam j => pmap (extend bv lu) (extend-char bu lv j) *> extend-char bv lu j
    | f_hinv => exts $ basis-ext (extend bu lv ∘ extend bv lu) (id V) 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 (Iso.f {basis-iso bu' bu}) MatrixRing.product toMatrix lu' bv f = toMatrix lu bv f
    => inv $ Equiv.adjointInv {matrix-equiv bu bv} $ inv $ toLinearMap_* (toMatrix lu bu (extend bu' lu)) (toMatrix lu' bv f) bu bu' bv *>
        pmap2 (∘) (ret_f {matrix-equiv bu' bv} f) {_} {id U} (exts \lam u => toLinearMap_toMatrix-right bu bu bu' *> pmap 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 (Iso.f {basis-iso bv bv'}) = toMatrix lu bv f
    => inv $ Equiv.adjointInv {matrix-equiv bu bv} $ unfold $ inv $ toLinearMap_* (toMatrix lu bv' f) (toMatrix lv bv (extend bv lv')) bu bv' bv *>
        pmap2 (∘) {_} {id V} (exts \lam u => toLinearMap_toMatrix-left bv bv' *> pmap BigSum (exts \lam j => pmap (`*c _) $ V.basis-split-unique bv _ idp j) *> inv (V.basis-split-char {lv'} {bv'})) (ret_f {matrix-equiv bu bv'} 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)
}

\lemma linearMap_zro {R : Ring} {A B : LModule R} : LinearMap A B (\lam _ => ) \cowith
  | func-+ => inv zro-left
  | func-*c => inv B.*c_zro-right

\lemma linearMap_+ {R : Ring} {A B : LModule R} (f g : LinearMap A B) : LinearMap A B (\lam a => f a + g a) \cowith
  | func-+ => pmap2 (+) f.func-+ g.func-+ *> equation
  | func-*c => pmap2 (+) f.func-*c g.func-*c *> inv *c-ldistr

\lemma linearMap_negative {R : Ring} {A B : LModule R} (f : LinearMap A B) : LinearMap A B (\lam a => negative (f a)) \cowith
  | func-+ => pmap negative f.func-+ *> B.negative_+ *> +-comm
  | func-*c => pmap negative f.func-*c *> inv B.*c_negative-right

\lemma linearMap_BigSum {R : Ring} {A B : LModule R} {m : Nat} (f : Fin m -> LinearMap A B) : LinearMap A B (\lam a => BigSum (\lam i => f i a)) \cowith
  | func-+ => cong (ext (\lam i => func-+)) *> B.BigSum_+
  | func-*c => cong (ext (\lam i => func-*c)) *> inv B.*c_BigSum-ldistr

\func arrayLinearMap {R : Ring} {V : LModule R} (v : Array V) : LinearMap (ArrayLModule v.len (RingLModule R)) V \cowith
  | func c => BigSum \lam j => c j *c v j
  | func-+ {x} {y} => pmap BigSum (exts \lam j => *c-rdistr) *> V.BigSum_+ {_} {\lam j => x j *c v j}
  | func-*c => pmap BigSum (exts \lam j => *c-assoc) *> inv V.*c_BigSum-ldistr
  \where {
    \lemma surj-char {v : Array V} : isSurj (arrayLinearMap v) <-> V.IsGenerated v
      => (\lam s x => TruncP.map (s x) \lam t => (t., inv t.), \lam g x => TruncP.map (g x) \lam t => (t., inv t.))

    \lemma inj-char {v : Array V} : isInj (arrayLinearMap v) <-> V.IsIndependent v
      => (\lam inj c p j => path (\lam i => inj {c} {\lam _ => } (p *> inv (BigSum_zro \lam j => V.*c_zro-left)) i j),
          \lam ind {l} {l'} p => unfold at p $ exts \lam j => R.fromZero $ ind (\lam j => l j - l' j) (later (pmap BigSum (exts \lam j => V.*c-rdistr *> pmap (_ +) V.*c_negative-left) *> V.BigSum_+ {_} {\lam j => l j *c v j}) *> pmap (_ +) (inv V.BigSum_negative) *> V.toZero p) j )

    \lemma equiv-char {v : Array V} : Equiv (arrayLinearMap v) <-> V.IsBasis v
      => (\lam e => (inj-char. (Equiv.isInj {e}), surj-char. (Equiv.isSurj {e})), \lam b => Equiv.fromInjSurj _ (inj-char. b.) (surj-char. b.))
  }

\record BilinearMap {R : Ring} (A B C : LModule R) (\coerce func : A -> B -> C)
  | linear-left {b : B} : LinearMap A C (func __ b)
  | linear-right {a : A} : LinearMap B C (func a)

\func isMultiLinear {R : Ring} {n : Nat} {A B : LModule R} (f : Array A n -> B) : \Prop \elim n
  |  => \Sigma
  | suc n => \Pi (l : Array A n) (j : Fin (suc n)) -> LinearMap A B (\lam x => f (insert x l j))
  \where {
    \lemma reduce {n : Nat} (f : Array A (suc n) -> B) (fl : isMultiLinear f) {a : A} : isMultiLinear (\lam l => f (a :: l)) \elim n
      |  => ()
      | suc n => \lam l j => fl (a :: l) (suc j)

    \lemma reduce0 {n : Nat} (f : Array A (suc n) -> B) (fm : isMultiLinear f) {as : Array A n} : LinearMap A B (\lam a => f (a :: as))
      => coe (\lam i => LinearMap A B (\lam a => f (insert_zro {_} {_} {a} i))) (fm as ) right

    \lemma fromReplace {n : Nat} {f : Array A n -> B} (p : \Pi (l : Array A n) (j : Fin n) -> LinearMap A B (\lam x => f (replace l j x))) : isMultiLinear f \elim n
      |  => ()
      | suc n => \lam l j => \new LinearMap {
        | func-+ => inv (pmap f (replace_insert {_} {l} {j} {A.zro})) *> func-+ {p _ j} *> pmap2 (+) (pmap f replace_insert) (pmap f replace_insert)
        | func-*c => inv (pmap f (replace_insert {_} {l} {j} {A.zro})) *> func-*c {p _ j} *> pmap (_ *c) (pmap f replace_insert)
      }

    \lemma toReplace {n : Nat} {f : Array A n -> B} (fl : isMultiLinear f) (l : Array A n) (j : Fin n) : LinearMap A B (\lam x => f (replace l j x)) \elim n
      |  => \case j
      | suc n => \new LinearMap {
        | func-+ => inv (pmap f insert_skip) *> func-+ {fl _ j} *> pmap2 (f __ + f __) insert_skip insert_skip
        | func-*c => inv (pmap f insert_skip) *> func-*c {fl _ j} *> pmap (_ *c f __) insert_skip
      }

    \type IsLinearComb {R : Ring} {U : LModule R} (x : U) {J : \Set} (g : J -> U)
      => \Sigma (c : Array (\Sigma R J)) (x = U.BigSum \lam j => (c j). *c g (c j).)

    \func makeLinearComb {R : Ring} {U : LModule R} {J : \Set} (g : J -> U) (c : Array (\Sigma R J)) : \Sigma (x : U) (J : \Set) (g : J -> U) (IsLinearComb x g)
      => (_, J, g, (c,idp))

    \func linearComb-map (f : LinearMap A B) {x : A} {J : \Set} {g : J -> A} (xg : IsLinearComb x g) : IsLinearComb (f x) (\lam j => f (g j))
      => (xg., pmap f xg. *> f.func-BigSum *> pmap BigSum (exts \lam j => func-*c))

    \func linearComb-trans {R : Ring} {U : LModule R} {x : U} {n : Nat} {K : Fin (suc n) -> \Set} {H : (\Pi (i : Fin (suc n)) -> K i) -> U} {g : K  -> U} (xc : IsLinearComb x g)
                           (k : \Pi (j : K ) -> IsLinearComb (g j) (\lam (f : \Pi (i : Fin n) -> K (suc i)) => H (j :: f))) : IsLinearComb x H
      => \let | y j l => ((k (xc. j).). l).
              | z j l => (xc. j). :: ((k (xc. j).). l).
              | t => xc. *> path (\lam i => BigSum \lam j => (xc. j). *c (k (xc. j).). i) *>
                             path (\lam i => BigSum \lam j => U.*c_BigSum-ldistr {(xc. j).} {\lam l => y j l *c H (z j l)} i) *>
                             U.BigSum-double-dep _ (\lam s => (xc. s.). *c (y s. s. *c H (z s. s.)))
         \in (mkArray \lam s =>
            \let (j,l) => SigmaFin.aux.f s \in later ((xc. j). R.* y j l, z j l), t *> path \lam i => BigSum \lam s =>
            \let (j,l) => SigmaFin.aux.f s \in inv (U.*c-assoc {(xc. j).} {y j l} {H (z j l)}) i)

    \func linearComb-div {R : CRing} {x : R} {J : \Set} {g : J -> R} (c : IsLinearComb {R} {RingLModule R} x g) {d : R} (p : \Pi (j : J) -> TruncP (Monoid.LDiv d (g j))) : TruncP (Monoid.LDiv d x)
      => \case FinSet.finiteAC (\lam j => p (c. j).) \with {
           | inP f => inP $ rewrite c. $ Semiring.LDiv_BigSum \lam j => later $ Monoid.LDiv.factor-right (f j)
         }

    \func multiLinear-comb (args : Array (\Sigma (x : A) (J : \Set) (g : J -> A) (IsLinearComb x g))) (f : Array A args.len -> B) (fm : isMultiLinear f)
      : IsLinearComb (f (map __. args)) {\Pi (i : Fin args.len) -> (args i).} \lam g => f \lam i => (args i). (g i) \elim args
      | nil => ((, \case __) :: nil, inv $ zro-right *> ide_*c)
      | (x,J,g,xg) :: args => \let | t a => multiLinear-comb args (\lam l => f (a :: l)) (reduce f fm)
                                   | s : IsLinearComb (f (x :: map __. args)) (\lam j => f (g j :: map __. args)) => linearComb-map (reduce0 f fm {map __. args}) xg
                              \in linearComb-trans s \lam j => t (g j)
  }

\lemma isMultilinear_zro {R : Ring} {n : Nat} {A B : LModule R} : isMultiLinear {R} {n} {A} {B} (\lam x => ) \elim n
  |  => ()
  | suc n => \lam l j => linearMap_zro

\lemma isMultilinear_+ {R : Ring} {n : Nat} {A B : LModule R} {f g : Array A n -> B} (fl : isMultiLinear f) (gl : isMultiLinear g) : isMultiLinear (\lam x => f x + g x) \elim n
  |  => ()
  | suc n => \lam l j => linearMap_+ (fl l j) (gl l j)

\lemma isMultilinear_negative {R : Ring} {n : Nat} {A B : LModule R} {f : Array A n -> B} (fl : isMultiLinear f) : isMultiLinear (\lam x => negative (f x)) \elim n
  |  => ()
  | suc n => \lam l j => linearMap_negative (fl l j)

\lemma isMultilinear_BigSum {R : Ring} {n : Nat} {A B : LModule R} {m : Nat} (f : Fin m -> Array A n -> B) (fl : \Pi (j : Fin m) -> isMultiLinear (f j)) : isMultiLinear (\lam x => B.BigSum (\lam i => f i x)) \elim n
  |  => ()
  | suc n => \lam l j => linearMap_BigSum (fl __ l j)

\lemma isMultilinear_linear-left {R : Ring} {n : Nat} {A B C : LModule R} (f : LinearMap A B) {g : Array B n -> C} (gl : isMultiLinear g) : isMultiLinear (\lam l => g (map f l)) \elim n
  |  => ()
  | suc n => \lam l j => transport (LinearMap A C) (ext \lam a => pmap g (inv (map_insert f))) (gl (map f l) j ∘ {LModuleCat R} f)

\lemma isMultilinear_linear-right {R : Ring} {n : Nat} {A B C : LModule R} {f : Array A n -> B} (fl : isMultiLinear f) (g : LinearMap B C) : isMultiLinear (\lam l => g (f l)) \elim n
  |  => ()
  | suc n => \lam l j => g ∘ {LModuleCat R} fl l j

\func isAlternating {R : Ring} {n : Nat} {A B : LModule R} (f : Array A n -> B) : \Prop
  => \Sigma (isMultiLinear f) (\Pi (l : Array A n) -> (\Sigma (i j : Fin n) (i < j) (l i = l j)) -> f l = )
  \where {
    \open NatSemiring(<,zero<suc,suc<suc)

    \lemma to/= {f : Array A n -> B} (fa : isAlternating f) (l : Array A n) (t : \Sigma (i j : Fin n) (i /= j) (l i = l j)) : f l = 
      => fa. l \case NatSemiring.trichotomy t. t. \with {
        | less e => (t., t., e, t.)
        | equals e => absurd $ t. (nat_fin_= e)
        | greater e => (t., t., e, inv t.)
      }

    \lemma reduce {n : Nat} (f : Array A (suc n) -> B) (fa : isAlternating f) {a : A} : isAlternating (\lam l => f (a :: l))
      => (isMultiLinear.reduce f fa., \lam l s => fa. (a :: l) (suc s., suc s., suc<suc s., s.))

    \lemma substract1from0 {n : Nat} {f : Array A (suc (suc n)) -> B} (fa : isAlternating f) {a a' : A} {l : Array A n} : f (a :: a' :: l) = f (a - a' :: a' :: l)
      => inv $ func-+ {fa. (a' :: l) } *> pmap (_ +) (AddGroupHom.func-negative {fa. (a' :: l) } *> pmap negative (fa. _ (, , zero<suc, idp)) *> B.negative_zro) *> zro-right

    \lemma add0to1 {n : Nat} {f : Array A (suc (suc n)) -> B} (fa : isAlternating f) {a a' : A} {l : Array A n} : f (a :: a' :: l) = f (a :: a + a' :: l)
      => inv $ inv (path (\lam i => f (a :: insert_zro i))) *> func-+ {fa. (a :: l) } *> pmap2 (+) (fa. _ (, , zero<suc, inv (path (\lam i => insert_zro i )))) (path (\lam i => f (a :: insert_zro i))) *> zro-left

    \lemma alternating_perm {n : Nat} {f : Array A n -> B} (fa : isAlternating f) {l l' : Array A n} (p : Perm l l') : f l = Perm.sign p *c f l' \elim n, l, l', p
      | , nil, nil, perm-nil => inv ide_*c
      | suc n, x :: l, _ :: l', perm-:: idp p => alternating_perm (reduce (\lam l => f l) fa) p *> pmap (R.pow -1 __ `*c _) (inv Perm.inversions_perm-::)
      | suc (suc n), x :: x' :: l, _ :: _ :: _, perm-swap idp idp idp =>
          f (x :: x' :: l)            ==< substract1from0 fa >==
          f (x - x' :: x' :: l)       ==< add0to1 fa *> simplify >==
          f (x - x' :: x :: l)        ==< substract1from0 fa *> simplify >==
          f (negative x' :: x :: l)   ==< pmap (\lam y => f (y :: x :: l)) (inv A.neg_ide_*c) *> func-*c {fa. (x :: l) } *> inv (pmap (`*c _) ide-left) >==
           * -1 *c f (x' :: x :: l)  `qed
      | n, l1, l2, perm-trans p1 p2 => alternating_perm fa p1 *> pmap (_ *c) (alternating_perm fa p2) *> inv (pmap (`*c _) (pmap (R.pow -1) Perm.inversions_perm-trans *> R.pow_+) *> *c-assoc)
  }

\lemma isAlternating_zro {R : Ring} {n : Nat} {A B : LModule R} : isAlternating {R} {n} {A} {B} (\lam x => )
  => (isMultilinear_zro, \lam _ _ => idp)

\lemma isAlternating_+ {R : Ring} {n : Nat} {A B : LModule R} {f g : Array A n -> B} (fa : isAlternating f) (ga : isAlternating g) : isAlternating (\lam x => f x + g x)
  => (isMultilinear_+ fa. ga., \lam l c => pmap2 (+) (fa. l c) (ga. l c) *> zro-left)

\lemma isAlternating_negative {R : Ring} {n : Nat} {A B : LModule R} {f : Array A n -> B} (fa : isAlternating f) : isAlternating (\lam x => negative (f x))
  => (isMultilinear_negative fa., \lam l c => pmap negative (fa. l c) *> B.negative_zro)

\lemma isAlternating_linear-left {R : Ring} {n : Nat} {A B C : LModule R} (f : LinearMap A B) {g : Array B n -> C} (ga : isAlternating g) : isAlternating (\lam l => g (map f l))
  => (isMultilinear_linear-left f ga., \lam l t => ga. (map f l) (t., t., t., pmap f t.))

\lemma isAlternating_linear-right {R : Ring} {n : Nat} {A B C : LModule R} {f : Array A n -> B} (fa : isAlternating f) (g : LinearMap B C) : isAlternating (\lam l => g (f l))
  => (isMultilinear_linear-right fa. g, \lam l t => pmap g (fa. l t) *> g.func-zro)

\lemma alternating-unique {R : Ring} {n : Nat} {A B : LModule R} {f g : Array A n -> B} (fa : isAlternating f) (ga : isAlternating g)
                          {l : Array A n} (Ag : A.IsGenerated l) (fl=gl : f l = g l) (a : Array A n) : f a = g a
  => B.fromZero $ alternating-unique_zro (\lam x => f x - g x) (isAlternating_+ fa (isAlternating_negative ga)) l Ag (B.toZero fl=gl) a
  \where {
    \open FinLinearOrder (FinLinearOrderInst)
    \open Perm

    \lemma alternating-unique_zro (f : Array A n -> B) (fa : isAlternating f)
                                  (l : Array A n) (Ag : A.IsGenerated l) (fl=0 : f l = ) (a : Array A n) : f a = 
      => aux f fa. l Ag a \lam c => \case repeats-dec c \with {
        | inl e => isAlternating.to/= fa (map l c) (e., e., e., pmap l e.)
        | inr inj => isAlternating.alternating_perm fa {map l c} {l} (perm-map l (perm-fin c inj)) *> rewrite fl=0 B.*c_zro-right
      }

    \lemma aux {n : Nat} (f : Array A n -> B) (fl : isMultiLinear f) (l : Array A) (Ag : A.IsGenerated l)
               (a : Array A n) (p : \Pi (c : Array (Fin l.len) n) -> f (map l c) = ) : f a =  \elim n, a
      | , a => p nil
      | suc n, a0 :: a => \case Ag a0 \with {
        | inP a0g => rewrite a0g. $ inv (pmap f insert_zro) *> LinearMap.linearComb {fl a } {a0g.} *>
                      BigSum_zro (\lam j => pmap (_ *c) (later $ pmap f insert_zro *> aux (\lam r => f (l j :: r)) (isMultiLinear.reduce f fl) l Ag a (\lam c => p (j :: c))) *> B.*c_zro-right)
      }
  }