\import Algebra.Group
\import Algebra.Group.Product
\import Algebra.Meta
\import Algebra.Module.LinearMap
\import Algebra.Monoid
\import Algebra.Monoid.Category
\import Algebra.Pointed
\import Algebra.Ring
\import Algebra.Ring.Category
\import Algebra.Ring.RingHom
\import Algebra.Semiring
\import Arith.Nat
\import Category
\import Data.Array
\import Data.Fin (unfsuc)
\import Equiv
\import Equiv.Univalence (Equiv-to-=)
\import Function (isInj, isSurj)
\import Function.Meta
\import HLevel
\import Logic
\import Logic.Classical
\import Logic.Meta
\import Meta
\import Order.LinearOrder
\import Order.PartialOrder
\import Paths
\import Paths.Meta
\import Set
\import Set.Fin

\class LModule (R : Ring) \extends AbGroup {
  | \infixl  *c : R -> E -> E
  | *c-assoc {r r' : R} {a : E} : r * r' *c a = r *c (r' *c a)
  | *c-ldistr {r : R} {a b : E} : r *c (a + b) = r *c a + r *c b
  | *c-rdistr {r s : R} {a : E} : (r R.+ s) *c a = r *c a + s *c a
  | ide_*c {a : E} :  *c a = a

  \lemma cancel {r : R} {a b : E} (i : Monoid.Inv r) (s : r *c a = r *c b) : a = b
    => inv ide_*c *> inv (pmap (`*c a) i.inv-left) *> *c-assoc *> pmap (i.inv *c) s *> inv *c-assoc *> pmap (`*c b) i.inv-left *> ide_*c

  \lemma *c_zro-left {a : E} :  *c a = 
    => cancel-left ( *c a) $ inv *c-rdistr *> simplify

  \lemma *c_zro-right {r : R} : r *c  = 
    => cancel-left (r *c ) $ inv *c-ldistr *> simplify

  \lemma *c_negative-left {r : R} {a : E} : R.negative r *c a = negative (r *c a)
    => negative-unique (r *c a) (inv *c-rdistr *> pmap (`*c a) R.negative-left *> *c_zro-left) negative-right

  \lemma *c_negative-right {r : R} {a : E} : r *c negative a = negative (r *c a)
    => negative-unique (r *c a) (inv *c-ldistr *> pmap (r *c) negative-left *> *c_zro-right) negative-right

  \lemma neg_ide_*c {a : E} : -1 *c a = negative a
    => *c_negative-left *> pmap negative ide_*c

  \lemma *c_BigSum-rdistr {l : Array R} {a : E} : R.BigSum l *c a = BigSum (\lam i => l i *c a) \elim l
    | nil => *c_zro-left
    | r :: l => *c-rdistr *> pmap (_ +) *c_BigSum-rdistr

  \lemma *c_BigSum-ldistr {r : R} {l : Array E} : r *c BigSum l = BigSum (\lam i => r *c l i) \elim l
    | nil => *c_zro-right
    | a :: l => *c-ldistr *> pmap (_ +) *c_BigSum-ldistr

  \lemma *c_FinSum-rdistr {J : FinSet} {f : J -> R} {a : E} : R.FinSum f *c a = FinSum (\lam j => f j *c a)
    => \case R.FinSum_char f \with {
         | inP (e,p) => pmap (`*c a) p *> *c_BigSum-rdistr *> inv (FinSum_char2 _ e)
       }

  \lemma *c_FinSum-ldistr {r : R} {J : FinSet} {f : J -> E} : r *c FinSum f = FinSum (\lam j => r *c f j)
    => \case FinSum_char f \with {
         | inP (e,p) => pmap (r *c) p *> *c_BigSum-ldistr *> inv (FinSum_char2 _ e)
       }

  \func IsDependent (l : Array E) : \Prop
    => ∃ (c : Array R l.len) (BigSum (\lam j => c j *c l j) = ) (j : Fin l.len) (c j /= )

  \func IsIndependent (l : Array E) : \Prop
    => \Pi (c : Array R l.len) -> BigSum (\lam j => c j *c l j) =  -> \Pi (j : Fin l.len) -> c j = 

  \type IsGenerated (l : Array E) : \Prop
    => \Pi (x : E) -> ∃ (c : Array R l.len) (x = BigSum (\lam i => c i *c l i))

  \type IsBasis (l : Array E) : \Prop
    => \Sigma (IsIndependent l) (IsGenerated l)

  \lemma independent-subset {l : Array E} (li : IsIndependent l) {k : Nat} (p : k <= l.len) : IsIndependent (\lam j => l (fin-inc_<= p j))
    => \lam c q j => inv (fit_<' c _) *> li (fit R.zro c) (inv (BigSum-subset {_} {_} {\lam j => fit R.zro c j *c l j} p
                      (\lam i => pmap (`*c _) (inv (fit_<' c (fin_< i <∘l p))))
                      (\lam i k<=i => pmap (`*c _) (fit_>= c k<=i) *> *c_zro-left)) *> q) (fin-inc_<= p j)

  \lemma independent-nonZero {l : Array E} (lb : IsIndependent l) {j : Fin l.len} (p : l j = ) :  = {R} 
    => inv (lb (replace (replicate l.len R.zro) j ide) (BigSum_zro \lam k => later \case decideEq j k \with {
      | yes j=k => rewriteI j=k $ rewrite replace-index $ ide_*c *> p
      | no j/=k => rewrite (replace-notIndex {_} {replicate l.len R.zro} \lam p => j/=k $ fin_nat-inj p) *c_zro-left
    }) j) *> replace-index

  \type IsIndependentSet {J : \Set} (g : J -> E) : \Prop
    => \Pi (c : Array (\Sigma R J)) -> sum g c =  -> IsZeroSum c
    \where {
      \func sum (g : J -> E) (c : Array (\Sigma R J)) => BigSum (\lam j => (c j). *c g (c j).)

      \lemma sum-ldistr (g : J -> E) {r : R} {c : Array (\Sigma R J)} : r *c sum g c = sum g (map (\lam s => (r * s., s.)) c)
        => *c_BigSum-ldistr *> pmap BigSum (exts \lam j => inv *c-assoc)

      \lemma sum_++ (g : J -> E) {c d : Array (\Sigma R J)} : sum g (c ++ d) = sum g c + sum g d
        => pmap BigSum (map_++ (\lam s => s. *c g s.)) *> BigSum_++

      \lemma sum_Big++ (g : J -> E) {l : Array (Array (\Sigma R J))} : sum g (Big (++) nil l) = BigSum (map (sum g) l) \elim l
        | nil => idp
        | c :: l => sum_++ g *> pmap (_ +) (sum_Big++ g)

      \lemma sum_negative (g : J -> E) {c : Array (\Sigma R J)} : negative (sum g c) = sum g (map (\lam s => (R.negative s., s.)) c)
        => BigSum_negative *> pmap BigSum (exts \lam j => inv *c_negative-left)

      \lemma sum_EPerm (g : J -> E) {l l' : Array (\Sigma R J)} (p : EPerm l l') : sum g l = sum g l'
        => BigSum_EPerm $ EPerm.EPerm_map (\lam s => s. *c g s.) p

      \lemma =_~ (gi : IsIndependentSet g) {c d : Array (\Sigma R J)} (p : sum g c = sum g d) : c Z~ d
        => gi _ $ sum_++ g *> pmap2 (+) (inv (sum_negative g)) p *> negative-left

      \lemma IsZeroSum_= (g : J -> E) {c : Array (\Sigma R J)} (p : IsZeroSum c) : sum g c =  \elim p
        | inP (l',e,f) => sum_EPerm g e *> sum_Big++ g *> BigSum_zro \lam j => unfold sum $ inv *c_BigSum-rdistr *> pmap (`*c _) (f j) *> *c_zro-left

      \lemma ~_= (g : J -> E) {c d : Array (\Sigma R J)} (p : c Z~ d) : sum g c = sum g d
        => fromZero $ +-comm *> pmap (`+ _) (sum_negative g) *> later (inv (sum_++ g)) *> IsZeroSum_= g p
    }

  \lemma IsIndependentSet-inj {J K : \Set} {f : J -> K} (inj : isInj f) {g : K -> E} (gi : IsIndependentSet g) : IsIndependentSet (\lam j => g (f j))
    => \lam c p => \case IsZeroSum.nonEmpty $ gi (map (\lam s => (s., f s.)) c) p \with {
         | inP (l1 : Array, e, h) => inP
           \let | g (s : \Sigma R J) => (s., f s.)
                | pi (i : Fin l1.len) : \Sigma (j : J) (f j = (l1 i).) =>
                  \let | i' => ++.index-big {_} {map (\lam s => map (\lam p0 => (p0, s.)) s.) l1} i $ toFin  (nonZero>0 (l1 i).)
                       | (e',g) => EPerm.eperm_equiv e
                  \in ((c (e' i'))., pmap __. (inv (g i') *> ++.Big++-index))
                | l2 => mkArray \lam i => ((l1 i)., (pi i).)
                | l2p : map (\lam s => (s., f s.)) l2 = map (\lam s => (s.,s.)) l1
                      => exts \lam i => ext (idp, (pi i).)
           \in (l2, EPerm.EPerm_map.conv g (\lam p => ext (pmap __. p, inj $ pmap __. p)) $ transport (EPerm _) (Big++_map g {map (\lam s => map (__,s.) s.) l2}) $ transportInv (\lam x => EPerm _ (Big (++) nil (map {\Sigma (Array R) K} (\lam s => map (__,s.) s.) x))) l2p e,
                transportInv (\lam (l : Array (Array R)) => \Pi (j : Fin l.len) -> R.BigSum (l j) = ) (pmap (map __.) l2p) h)
       }

  \type IsIndependentDec {J : \Set} (g : J -> E) : \Prop
    => \Pi (l : Array J) (c : Array R l.len) -> isInj l -> BigSum (\lam j => c j *c g (l j)) =  -> \Pi (j : Fin c.len) -> c j = 

  \lemma IsIndependentSet<->IsIndependentDec {J : DecSet} {g : J -> E} : IsIndependentSet g <-> IsIndependentDec g
    => (\lam li l c inj p j => inv (count-unique {_} {J} {_} {c} inj j) *> IsZeroSum_count (li (\lam j => (c j, l j)) p) (l j),
        \lam li c p => count_IsZeroSum $ li _ (map (count c) $ nub (map __. c)) nub-isInj $ pmap BigSum (exts \lam j => *c_BigSum-rdistr *> pmap BigSum (exts \lam k => pmap (_ *c g __) $ keep.satisfies (\lam s => decideEq (nub (map (\lam p0 => p0.) c) j) s.) {c} {k})) *> inv (sum_Big++ g) *> inv (sum_EPerm g nub-split) *> p)

  \lemma IsIndependent<->IsIndependentSet {l : Array E} : IsIndependent l <-> IsIndependentSet l
    => (\lam li c p => count_IsZeroSum \lam j => li (count c) (inv sum_BigSum *> p) _,
        \lam li c p j => IsIndependentSet<->IsIndependentDec. li (mkArray \lam j => j) c (\lam q => q) p j)
    \where
      \lemma sum_BigSum {l : Array E} {c : Array (\Sigma R (Fin l.len))} : sum l c = BigSum (\lam j => count c j *c l j)
        => BigSum_EPerm (EPerm.EPerm_map (\lam s => s. *c l s.) nub-split) *> sum_Big++ l *> inv FinSum=BigSum *>
            inv (FinSum-inj (nub (map __. c)) nub-isInj (\lam j q => pmap (`*c _) (count_zro j \lam k => /=-sym \let (i,p) => nub-isSurj (map __. c) k \in later $ rewriteI p (q i)) *> *c_zro-left) *> pmap FinSum (exts \lam j =>
              \let (i,q) => nub-preimage j
              \in rewrite q $ *c_BigSum-rdistr *> pmap BigSum (exts \lam k => pmap (_ *c l __) $ keep.satisfies (\lam s => decideEq (c i). s.) {c} {k}))) *> FinSum=BigSum

  \lemma IsIndependentSet-fin {J : FinSet} {g : J -> E} : IsIndependentSet g <-> (\Pi (c : J -> R) -> FinSum (\lam j => c j *c g j) =  -> \Pi (j : J) -> c j = )
    => \case J.finEq \with {
      | inP (e : Equiv) => transport {FinSet} (\lam X => \Pi (g : X -> E) -> IsIndependentSet g <-> (\Pi (c : X -> R) -> FinSum (\lam j => c j *c g j) =  -> \Pi (j : X) -> c j = )) {FinFin J.finCard} {J} (ext (Equiv-to-= e, idp))
          (\lam g => <->sym (IsIndependent<->IsIndependentSet {_} {g}) `<->trans` later (\lam f c p j => f c (inv FinSum=BigSum *> p) j, \lam f c p j => f c (FinSum=BigSum *> p) j)) g
    }

  \type IsGeneratingSet {J : \Set} (g : J -> E) : \Prop
    => \Pi (x : E) -> ∃ (c : Array (\Sigma R J)) (x = IsIndependentSet.sum g c)

  \lemma IsGeneratingSet-fin {J : \Set} {g : J -> E} : IsGeneratingSet g <-> (\Pi (x : E) -> ∃ (K : FinSet) (c : K -> \Sigma R J) (x = FinSum (\lam k => (c k). *c g (c k).)))
    => (\lam gs x => TruncP.map (gs x) \lam s => (_, s., s. *> inv FinSum=BigSum), \lam gs x =>
         \have | (inP (K, c, p)) => gs x
               | (inP e) => finEq {K}
         \in inP (\lam j => c (e j), p *> FinSum_Equiv e *> FinSum=BigSum))

  \lemma IsGeneratingSet-surj {J K : \Set} {f : J -> K} (surj : isSurj f) {g : K -> E} (gi : IsGeneratingSet g) : IsGeneratingSet (\lam j => g (f j))
    => \lam x =>
        \have | (inP s) => gi x
              | (inP h) => FinSet.finiteAC (\lam i => surj (s. i).)
        \in inP (mkArray \lam i => ((s. i)., (h i).), s. *> pmap BigSum (exts \lam i => cong (inv (h i).)))

  \lemma IsBasisSet-equiv {J K : \Set} (e : Equiv {J} {K}) {g : K -> E} (gb : IsBasisSet g) : IsBasisSet (\lam j => g (e j))
    => (IsIndependentSet-inj e.isInj gb., IsGeneratingSet-surj e.isSurj gb.)

  \lemma IsGenerated<->IsGeneratingSet {l : Array E} : IsGenerated l <-> IsGeneratingSet l
    => (\lam lg x => TruncP.map (lg x) \lam s => (\lam j => (s. j, j), s.),
        \lam lg x => TruncP.map (lg x) \lam s => (count s., s. *> IsIndependent<->IsIndependentSet.sum_BigSum))

  \type IsBasisSet {J : \Set} (g : J -> E) : \Prop
    => \Sigma (IsIndependentSet g) (IsGeneratingSet g)

  \lemma IsBasis<->IsBasisSet {l : Array E} : IsBasis l <-> IsBasisSet l
    => (\lam b => (IsIndependent<->IsIndependentSet. b., IsGenerated<->IsGeneratingSet. b.),
        \lam b => (IsIndependent<->IsIndependentSet. b., IsGenerated<->IsGeneratingSet. b.))

  \lemma independent-split-unique {l : Array E} (li : IsIndependent l) {c d : Array R l.len} (p : BigSum (\lam j => c j *c l j) = BigSum (\lam j => d j *c l j)) (j : Fin l.len) : c j = d j
    => R.fromZero $ li (\lam i => c i - d i) (cancel-right _ $ inv (BigSum_+ {_} {_} {\lam j => (c j - d j) *c l j}) *> pmap BigSum (exts \lam j => pmap (`+ _) *c-rdistr *> +-assoc *> pmap (_ +) (pmap (`+ _) *c_negative-left *> negative-left) *> zro-right) *> p *> inv zro-left) j

  \lemma basis-split-pair {l : Array E} (lb : IsBasis l) (x : E) : \Sigma (c : Array R l.len) (x = BigSum (\lam j => c j *c l j))
    \level basis-split-unique lb. x
    => \case lb. x \with {
      | inP r => r
    }
    \where {
      \lemma basis-split-unique {l : Array E} (li : IsIndependent l) (x : E) : isProp (\Sigma (c : Array R l.len) (x = BigSum (\lam j => c j *c l j)))
        => \lam s t => ext $ exts $ independent-split-unique li (inv s. *> t.)
    }

  \sfunc basis-split {l : Array E} (lb : IsBasis l) (x : E) : Array R l.len
    => (basis-split-pair lb x).

  \lemma basis-split-char {l : Array E} {lb : IsBasis l} {x : E} : x = BigSum (\lam j => basis-split lb x j *c l j)
    => (basis-split-pair lb x). *> pmap BigSum (exts \lam j => pmap {Array R l.len} (__ j *c _) (inv \peval basis-split lb x))

  \lemma basis-split-unique {l : Array E} (lb : IsBasis l) {x : E} (d : Array R l.len) (p : x = BigSum (\lam j => d j *c l j)) (j : Fin l.len) : basis-split lb x j = d j
    => independent-split-unique lb. (inv basis-split-char *> p) j

  \lemma basis_split_basis {l : Array E} {lb : IsBasis l} {j k : Fin l.len} : basis-split lb (l j) k = (\case decideEq j k \with { | yes _ =>  | no _ =>  })
    => \let f : Array R l.len => \case decideEq j __ \with { | yes _ =>  | no _ =>  }
       \in independent-split-unique lb. {_} {f} (inv $ BigSum-unique {_} {\lam k => f k *c l k} j (\lam k j/=k => rewrite (decideEq/=_reduce j/=k) *c_zro-left) *> rewrite (decideEq=_reduce idp) ide_*c *> basis-split-char) k

  \lemma basis_split_= {l : Array E} {lb : IsBasis l} {j : Fin l.len} : basis-split lb (l j) j = 
    => basis_split_basis *> rewrite (decideEq=_reduce idp) idp

  \lemma basis_split_/= {l : Array E} {lb : IsBasis l} {j k : Fin l.len} (j/=k : j /= k) : basis-split lb (l j) k = 
    => basis_split_basis *> rewrite (decideEq/=_reduce j/=k) idp

  \type IsGeneratedFin {J : FinSet} (f : J -> E) : \Prop
    => \Pi (x : E) -> ∃ (c : J -> R) (x = FinSum (\lam j => c j *c f j))

  \func IsFinitelyGenerated : \Prop
    => ∃ (l : Array E) (IsGenerated l)

  \lemma basisSet_basis (J : FinSet) {g : J -> E} (gb : IsBasisSet g) : ∃ (l : Array E J.finCard) (IsBasis l)
    => \case FinSet.finEq \with {
         | inP e => inP (\lam j => g (e j), IsBasis<->IsBasisSet. $ IsBasisSet-equiv e gb)
       }

  \lemma free-char : ∃ (l : Array E) (IsBasis l) <-> ∃ (J : FinSet) (g : J -> E) (IsBasisSet g)
    => (TruncP.map __ \lam s => (FinFin (DArray.len {s.}), s., IsBasis<->IsBasisSet. s.), \case __ \with {
         | inP (J,g,gb) => basisSet_basis J gb
       })

  \lemma generated-array-fin {l : Array E} (g : IsGenerated l) : IsGeneratedFin l
    => \lam x => TruncP.map (g x) \lam t => (t., t. *> inv FinSum=BigSum)

  \lemma generated-fin-array {J : FinSet} {f : J -> E} (g : IsGeneratedFin f) : IsFinitelyGenerated
    => TruncP.map J.finEq \lam (e : Equiv {Fin J.finCard} {J}) =>
        (\lam i => f (e i), \lam x => TruncP.map (g x) \lam t => (\lam i => t. (e i), t. *> FinSum_Equiv e *> FinSum=BigSum))

  \func IsFaithful : \Prop
    => \Pi (r : R) -> (\Pi (m : E) -> r *c m = ) -> r = 
} \where {
  \func count {R : Semiring} {J : DecSet} (l : Array (\Sigma R J)) (j : J) : R
    => R.BigSum (map __. $ keep (\lam s => decideEq j s.) l)

  \lemma count_zro {R : Semiring} {J : DecSet} {l : Array (\Sigma R J)} (j : J) (p : \Pi (k : Fin l.len) -> j /= (l k).) : count {R} l j = 
    => R.BigSum_zro \lam k => later \let t => keep.preimage k
                                    \in absurd $ p t. $ keep.satisfies (\lam s => decideEq j s.) {l} *> pmap __. t.

  \lemma count-unique {R : Semiring} {J : DecSet} {l : Array J} {c : Array R l.len} (inj : isInj l) (k : Fin l.len) : count (\lam j => (c j, l j)) (l k) = c k \elim l, k
    | j :: l,  => unfold count $ rewrite (decideEq=_reduce idp) $ pmap (_ +) (pmap (\lam x => BigSum (map {\Sigma R J} __. x)) (keep-none \lam k p => \case inj {} {suc k} p)) *> zro-right
    | j :: l, suc k => unfold count $ mcases \with {
      | yes p => \case inj {suc k} {} p
      | no q => count-unique {R} {J} {l} {\lam j => c (suc j)} (\lam p => unfsuc (inj p)) k
    }

  \type IsZeroSum {R : Semiring} {J : \Set} (l : Array (\Sigma R J)) : \Prop
    => ∃ (l' : Array (\Sigma (Array R) J)) (EPerm l (Big (++) nil $ map (\lam s => map (__, s.) s.) l')) (\Pi (j : Fin l'.len) -> R.BigSum (l' j). = )
    \where {
      \private \lemma aux {l : Array (\Sigma (Array R) J)}
        : Big (++) nil (map (\lam s => map (__, s.) s.) l) =
          Big (++) nil (mkArray \lam i => map (__, (remove (\lam s => decideEq (DArray.len {s.}) ) l i).) (remove (\lam s => decideEq (DArray.len {s.}) ) l i).) \elim l
        | nil => idp
        | s :: l => mcases {} \with {
          | yes p => pmap2 (++) {_} {nil} (later $ cases (s.,p) \with {
            | nil, _ => idp
          }) aux
          | no n => pmap (_ ++) aux
        }

      \lemma nonEmpty {l : Array (\Sigma R J)} (zs : IsZeroSum l) : ∃ (l' : Array (\Sigma (c : Array R) J (c.len /= ))) (EPerm l (Big (++) nil $ map (\lam s => map (__, s.) s.) l')) (\Pi (j : Fin l'.len) -> R.BigSum (l' j). = ) \elim zs
        | inP (l1,e,f) =>
          \let l2 => remove (\lam s => decideEq (DArray.len {s.}) ) l1
          \in inP (mkArray \lam i => later ((l2 i)., (l2 i)., remove.no-element (\lam s => decideEq (DArray.len {s.}) ) {l1} {i}),
                   eperm-trans e $ EPerm.eperm-= aux,
                   \lam i => \let (k,p) => remove.preimage i \in pmap (\lam x => BigSum x.) p *> f k)
    }

  \type \infix  Z~ {R : Ring} {J : \Set} (l1 l2 : Array (\Sigma R J)) : \Prop
    => IsZeroSum (map (\lam s => (R.negative s., s.)) l2 ++ l1)

  \lemma count_IsZeroSum {R : Semiring} {J : DecSet} {l : Array (\Sigma R J)} (p : \Pi (j : Fin (DArray.len {nub $ map __. l})) -> count l (nub (map __. l) j) = ) : IsZeroSum l
    => inP (map (\lam j => (map __. $ keep (\lam s => decideEq j s.) l, j)) (nub $ map __. l), eperm-trans nub-split $ EPerm.eperm-= $ pmap (Big (++) nil) $ exts \lam i =>
        \let | j => nub (map __. l) i
             | l' => \new keep (\lam s => decideEq j s.) l
        \in (exts (\lam k => ext (idp, inv $ keep.satisfies (\lam s => decideEq j s.) {l})) : l' = map (\lam s => (s.,j)) l'), p)

  \lemma IsZeroSum_count {R : Semiring} {J : DecSet} {l : Array (\Sigma R J)} (p : IsZeroSum l) (j : J) : count l j =  \elim p
    | inP (l',e,f) => count_EPerm e *> count_Big++ *> BigSum_zro \lam i => later \case decideEq j (l' i). \with {
      | yes p => pmap (\lam x => BigSum (map {\Sigma R J} __. x)) (keep-all \lam k => later p) *> f i
      | no p => pmap (\lam x => BigSum (map {\Sigma R J} __. x)) $ keep-none \lam k => later p
    }
    \where {
      \lemma count_EPerm {l l' : Array (\Sigma R J)} (p : EPerm l l') {j : J} : count l j = count l' j
        => BigSum_EPerm $ EPerm.EPerm_map __. (EPerm.EPerm_keep p)

      \lemma count_++ {l l' : Array (\Sigma R J)} {j : J} : count (l ++ l') j = count l j + count l' j \elim l
        | nil => inv zro-left
        | s :: l => unfold count $ mcases \with {
          | yes q => pmap (s. +) count_++ *> inv +-assoc
          | no q => count_++
        }

      \lemma count_Big++ {ls : Array (Array (\Sigma R J))} {j : J} : count (Big (++) nil ls) j = BigSum (\lam i => count (ls i) j) \elim ls
        | nil => idp
        | l :: ls => count_++ *> pmap (_ +) count_Big++
    }

  \open IsIndependentSet

  \sfunc basisSet-split {R : Ring} {U V : LModule R} {J : \Set} {u : J -> U} (ub : IsBasisSet u) (v : J -> V) (x : U)
    : \Sigma (y : V) (∃ (c : Array (\Sigma R J)) (x = sum u c) (y = sum v c))
    => \case TruncP.rec-set (ub. x) (\lam s => sum v s.) (\lam s s' => ~_= v $ =_~ ub. $ inv s. *> s'.) \with {
      | (y, t) => (y, TruncP.map t \lam s => (s.., s.., inv s.))
    }

  \func pullback (f : RingHom) (M : LModule f.Cod) : LModule f.Dom \cowith
    | AbGroup => M
    | *c a x => f a *c x
    | *c-assoc => pmap (`*c _) f.func-* *> *c-assoc
    | *c-ldistr => *c-ldistr
    | *c-rdistr => pmap (`*c _) f.func-+ *> *c-rdistr
    | ide_*c => pmap (`*c _) f.func-ide *> ide_*c

  \lemma generated-fin-comp (f : RingHom) {M : LModule f.Cod} {I J : FinSet} {a : I -> f.Cod} {b : J -> M} (Cg : IsGeneratedFin {homLModule f} a) (Mg : IsGeneratedFin b)
    : IsGeneratedFin {pullback f M} (\lam (p : \Sigma J I) => a p. *c b p.)
    => \lam x => \have | (inP (d,p)) => Mg x
                       | (inP g) => choice (\lam j => Cg (d j))
                 \in inP (\lam s => (g s.). s., p *> path (\lam i => FinSum (\lam j => (g j). i *c b j)) *>
                            path (\lam i' => FinSum (\lam j => M.*c_FinSum-rdistr {I} {\lam i => (g j). i *c a i} {b j} i')) *> FinSum-double *> pmap FinSum (ext \lam s => *c-assoc))

  \lemma generated-pullback (f : RingHom) {M : LModule f.Cod} (Cg : IsFinitelyGenerated {homLModule f}) (Mg : M.IsFinitelyGenerated) : IsFinitelyGenerated {pullback f M} \elim Cg, Mg
    | inP (l,Cg), inP (l',Mg) => generated-fin-array {pullback f M} $ generated-fin-comp f (generated-array-fin Cg) (generated-array-fin Mg)

  \lemma generated-comp {R S T : Ring} (f : RingHom R S) (g : RingHom S T) (fg : IsFinitelyGenerated {homLModule f}) (gg : IsFinitelyGenerated {homLModule g}) : IsFinitelyGenerated {homLModule (g ∘ f)}
    => generated-pullback f fg gg
}

\instance ProductLModule (R : Ring) (A B : LModule R) : LModule R
  | AbGroup => ProductAbGroup A B
  | *c r p => (r *c p., r *c p.)
  | *c-assoc => pmap2 (__,__) *c-assoc *c-assoc
  | *c-ldistr => pmap2 (__,__) *c-ldistr *c-ldistr
  | *c-rdistr => pmap2 (__,__) *c-rdistr *c-rdistr
  | ide_*c => pmap2 (__,__) ide_*c ide_*c

\func RingLModule (R : Ring) : LModule R R \cowith
  | AbGroup => R
  | *c => *
  | *c-assoc => *-assoc
  | *c-ldistr => R.ldistr
  | *c-rdistr => R.rdistr
  | ide_*c => ide-left
  \where {
    \func *_hom-left {R : CRing} {x : R} : LinearMap (RingLModule R) (RingLModule R) \cowith
      | func y => x * y
      | func-+ => ldistr
      | func-*c => equation

    \func *_hom-right {R : Ring} {x : R} : LinearMap (RingLModule R) (RingLModule R) \cowith
      | func y => y * x
      | func-+ => rdistr
      | func-*c => *-assoc

    \lemma basis {R : Ring} : LModule.IsBasis {RingLModule R} ( :: nil)
      => (\lam c p () => inv ide-right *> inv zro-right *> p, \lam x => inP (x :: nil, simplify))
  }

\instance PowerLModule {R : Ring} (J : \Set) (M : LModule R) : LModule R (J -> M)
  | zro _ => 
  | + f g j => f j + g j
  | zro-left => ext (\lam j => zro-left)
  | zro-right => ext (\lam j => zro-right)
  | +-assoc => ext (\lam j => +-assoc)
  | negative f j => negative (f j)
  | negative-left => ext (\lam j => negative-left)
  | +-comm => ext (\lam j => +-comm)
  | *c r f j => r *c f j
  | *c-assoc => ext (\lam j => *c-assoc)
  | *c-ldistr => ext (\lam j => *c-ldistr)
  | *c-rdistr => ext (\lam j => *c-rdistr)
  | ide_*c => ext (\lam j => ide_*c)

\instance ArrayLModule {R : Ring} (n : Nat) (M : LModule R) : LModule R (Array M n)
  | zro _ => 
  | + f g j => f j + g j
  | zro-left => arrayExt (\lam j => zro-left)
  | zro-right => arrayExt (\lam j => zro-right)
  | +-assoc => arrayExt (\lam j => +-assoc)
  | negative f j => negative (f j)
  | negative-left => arrayExt (\lam j => negative-left)
  | +-comm => arrayExt (\lam j => +-comm)
  | *c r f j => r *c f j
  | *c-assoc => arrayExt (\lam j => *c-assoc)
  | *c-ldistr => arrayExt (\lam j => *c-ldistr)
  | *c-rdistr => arrayExt (\lam j => *c-rdistr)
  | ide_*c => arrayExt (\lam j => ide_*c)
  \where {
    \lemma skip_*c {R : CRing} {n : Nat} {r : R} {l : Array R (suc n)} {k : Fin (suc n)}
      : skip (r *c {ArrayLModule _ (RingLModule R)} l) k = r *c {ArrayLModule _ (RingLModule R)} skip l k \elim n, l, k
      | , a :: nil,  => idp
      | suc n, a :: l,  => idp
      | suc n, a :: l, suc k => path (\lam i => r *c a :: skip_*c i)

    \lemma skip_+ {R : CRing} {n : Nat} {l l' : Array R (suc n)} {k : Fin (suc n)}
      : skip (l + {ArrayLModule _ (RingLModule R)} l') k = skip l k + {ArrayLModule _ (RingLModule R)} skip l' k \elim n, l, l', k
      | , a :: nil, a' :: nil,  => idp
      | suc n, a :: l, a' :: l',  => idp
      | suc n, a :: l, a' :: l', suc k => path (\lam i => a + a' :: skip_+ i)

    \lemma BigSum-index {R : Ring} {n : Nat} {M : LModule R} {l : Array (Array M n)} {i : Fin n}
      : AddMonoid.BigSum {ArrayLModule n M} l i = M.BigSum (map {Array M n} (__ i) l) \elim l
      | nil => idp
      | a :: l => pmap (_ +) BigSum-index
  }

\func homLModule (f : RingHom) : LModule f.Dom \cowith
  | AbGroup => f.Cod
  | *c x y => f x * y
  | *c-assoc => pmap (`* _) f.func-* *> *-assoc
  | *c-ldistr => ldistr
  | *c-rdistr => pmap (`* _) f.func-+ *> rdistr
  | ide_*c => pmap (`* _) f.func-ide *> ide-left