\import Algebra.Group
\import Algebra.Group.Sub
\import Algebra.Module
\import Algebra.Monoid
\import Algebra.Monoid.Sub
\import Algebra.Pointed
\import Algebra.Pointed.Sub
\import Algebra.Ring
\import Algebra.Ring.Ideal
\import Data.Array
\import Logic
\import Logic.Meta
\import Meta
\import Order.Lattice
\import Paths
\import Paths.Meta

\class SubLModule (R : Ring) \extends SubAddGroup {
  \override S : LModule R
  | contains_*c {a : R} {b : S} : contains b -> contains (a *c b)

  \func IModule : LModule R \cowith
    | AddGroup => IAddGroup
    | +-comm => ext +-comm
    | *c r p => (r *c p., contains_*c p.)
    | *c-assoc => ext *c-assoc
    | *c-ldistr => ext *c-ldistr
    | *c-rdistr => ext *c-rdistr
    | ide_*c => ext ide_*c
}

\func topSubLModule {R : Ring} (M : LModule R) : SubLModule { | R => R | S => M } \cowith
  | contains _ => \Sigma
  | contains_zro => ()
  | contains_+ _ _ => ()
  | contains_negative _ => ()
  | contains_*c _ => ()

\instance SubLModuleSemilattice (R : Ring) (M : LModule R) : TopMeetSemilattice (SubLModule { | R => R | S => M })
  | <= U V => \Pi {a : M} -> U a -> V a
  | <=-refl c => c
  | <=-transitive f g c => g (f c)
  | <=-antisymmetric f g => exts \lam _ => ext (f,g)
  | meet (U V : SubLModule { | R => R | S => M }) : SubLModule { | R => R | S => M } \cowith {
    | contains a => \Sigma (U a) (V a)
    | contains_zro => (contains_zro, contains_zro)
    | contains_+ s t => (contains_+ s. t., contains_+ s. t.)
    | contains_negative s => (contains_negative s., contains_negative s.)
    | contains_*c s => (contains_*c s., contains_*c s.)
  }
  | meet-left => __.
  | meet-right => __.
  | meet-univ f g c => (f c, g c)
  | top => topSubLModule M
  | top-univ _ => ()

\func \infixl  *m {R : Ring} (I : LIdeal R) {M : LModule R} (S : SubLModule { | R => R | S => M }) : SubLModule { | R => R | S => M } \cowith
  | contains a => ∃ (l : Array (\Sigma (x : R) (I x) M)) (a = M.BigSum (map (\lam s => s. *c s.) l))
  | contains_zro => inP (nil,idp)
  | contains_+ (inP s) (inP t) => inP (s. ++ t., pmap2 (+) s. t. *> inv M.BigSum_++ *> pmap M.BigSum (inv (map_++ (\lam s => s. *c s.))))
  | contains_negative (inP s) => inP (map (later \lam t => (negative t., contains_negative t., t.)) s., pmap negative s. *> M.BigSum_negative *> pmap M.BigSum (exts \lam _ => inv M.*c_negative-left))
  | contains_*c {a} {_} (inP s) => inP (map (later \lam t => (a * t., ideal-left t., t.)) s., pmap (a *c) s. *> M.*c_BigSum-ldistr *> pmap M.BigSum (exts \lam _ => inv M.*c-assoc))

\func OneDimSubmod {R : Ring} {L : LModule R} (v : L) : SubLModule R L \cowith
  | contains u => ∃ (r : R) (r *c v = u)
  | contains_zro => inP (, L.*c_zro-left)
  | contains_+ p q => \case \elim p, \elim q \with {
    | inP r1, inP r2 => inP (r1. + r2., rewrite (*c-rdistr, r1., r2.) idp)
  }
  | contains_negative p => \case \elim p \with {
    | inP r => inP (negative r., rewrite (L.*c_negative-left, pmap negative r.) idp)
  }
  | contains_*c {a} p => \case \elim p \with {
    | inP r => inP (a * r., rewrite (*c-assoc, r.) idp)
  }