Module.ard

\import Algebra.Group
\import Algebra.Group.Product
\import Algebra.Monoid
\import Algebra.Ring
\import Function.Meta
\import Paths
\import Paths.Meta

\class LModule (R : Ring) \extends AbGroup {
  | \infixl 7 *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} : 1 *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 zro_*c-left {a : E} : 0 *c a = 0
    => cancel-left (0 *c a) $ inv *c-rdistr *> pmap (`*c a) R.zro-left *> inv zro-right

  \lemma zro_*c-right {r : R} : r *c 0 = 0
    => cancel-left (r *c 0) $ inv *c-ldistr *> pmap (r *c) zro-left *> inv zro-right
}

\meta LModule' R => LModule { | R => R }

\instance ProductLModule (R : Ring) (A B : LModule' R) : LModule' R
  | AbGroup => ProductAbGroup A B
  | *c r p => (r *c p.1, r *c p.2)
  | *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 => R } \cowith
  | AbGroup => R
  | *c => *
  | *c-assoc => *-assoc
  | *c-ldistr => R.ldistr
  | *c-rdistr => R.rdistr
  | ide_*c => ide-left

\instance PowerLModule {R : Ring} (J : \Set) (M : LModule' R) : LModule (J -> M) { | R => R }
  | zro _ => 0
  | + 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)