\import Algebra.Group
\import Algebra.Group.SubGroup
\import Algebra.Module
\import Algebra.Module.LinearMap
\import Algebra.Monoid
\import Algebra.Monoid.SubMonoid
\import Algebra.Pointed
\import Algebra.Pointed.SubPointed
\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)
}

\instance IModule (S : SubLModule {}) : LModule S.R
  | AddGroup => IAddGroup S
  | +-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
  \where
    \func embed : LinearMap (IModule S) S.S \cowith
      | AddGroupHom => IAddGroup.embed
      | func-*c => idp

\func topSubLModule {R : Ring} (M : LModule R) : SubLModule R 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)
  }

\func KernelLModule (f : LinearMap {}) : SubLModule f.R f.Dom \cowith
  | SubAddGroup => KernelAddGroup f
  | contains_*c fb=0 => func-*c *> pmap (_ *c) fb=0 *> LModule.*c_zro-right

\func ImageLModule (f : LinearMap {}) : SubLModule f.R f.Cod \cowith
  | SubAddGroup => ImageAddGroup f
  | contains_*c {r} (inP (a,fa=b)) => inP (r *c a, func-*c *> pmap (r *c) fa=b)

\func ImLModule (f : LinearMap {}) : LModule
  => IModule (ImageLModule f)

\func ImLModuleLeftHom (f : LinearMap {}) : LinearMap f.Dom (ImLModule f) \cowith
  | AddGroupHom => ImAddGroupLeftHom f
  | func-*c => ext func-*c