\import Algebra.Group.Category
\import Algebra.Module
\import Algebra.Module.LinearMap
\import Algebra.Monoid.Category
\import Algebra.Ring
\import Algebra.Ring.RingHom
\import Category
\import Category.Meta
\import Logic
\import Paths
\import Paths.Meta

\instance LModuleCat (R : Ring) : Cat (LModule R)
  | Hom A B => LinearMap A B
  | id A => \new LinearMap {
    | func a => a
    | func-+ => idp
    | func-*c => idp
  }
  | o g f => \new LinearMap {
    | func a => g (f a)
    | func-+ => pmap g func-+ *> func-+
    | func-*c => pmap g func-*c *> func-*c
  }
  | id-left => idp
  | id-right => idp
  | o-assoc => idp
  | univalence => sip (\lam (f : LinearMap) g => exts (f.func-zro, \lam x x' => f.func-+, \lam x => f.func-negative, \lam e x => f.func-*c))

\instance KerLModule {R : Ring} {A B : LModule R} (f : LinearMap A B) : LModule R
  | AbGroup => KerAbGroup f
  | *c r a => (r *c a., func-*c *> pmap (r *c) a. *> B.*c_zro-right)
  | *c-assoc => ext *c-assoc
  | *c-ldistr => ext *c-ldistr
  | *c-rdistr => ext *c-rdistr
  | ide_*c => ext ide_*c

\func KerLModuleHom {R : Ring} {A B : LModule R} (f : LinearMap A B) : LinearMap (KerLModule f) f.Dom \cowith
  | AddGroupHom => KerGroupHom f
  | func-*c => idp

\instance ImageLModule {R : Ring} {A B : LModule R} (f : LinearMap A B) : LModule R
  | AbGroup => ImageAbGroup f
  | *c r a => (r *c a., TruncP.map a. \lam s => (r *c s., func-*c *> pmap (r *c) s.))
  | *c-assoc => ext *c-assoc
  | *c-ldistr => ext *c-ldistr
  | *c-rdistr => ext *c-rdistr
  | ide_*c => ext ide_*c

\func ImageLModuleLeftHom {R : Ring} {A B : LModule R} (f : LinearMap A B) : LinearMap f.Dom (ImageLModule f) \cowith
  | AddGroupHom => ImageGroupLeftHom f
  | func-*c => ext func-*c

\func ImageLModuleRightHom {R : Ring} {A B : LModule R} (f : LinearMap A B) : LinearMap (ImageLModule f) f.Cod \cowith
  | AddGroupHom => ImageGroupRightHom f
  | func-*c => idp

\instance LinearMapRing {R : Ring} (U : LModule R) : Ring (LinearMap U U)
  | zro => linearMap_zro
  | + => linearMap_+
  | zro-left => exts \lam u => U.zro-left
  | +-assoc => exts \lam u => U.+-assoc
  | +-comm => exts \lam u => U.+-comm
  | negative => linearMap_negative
  | negative-left => exts \lam u => U.negative-left
  | ide => id U
  | * f g => g ∘ f
  | ide-left => idp
  | ide-right => idp
  | *-assoc => idp
  | ldistr => idp
  | rdistr => exts \lam u => func-+
  \where {
    \func *c-hom {R : CRing} {U : LModule R} : RingHom R (LinearMapRing U) \cowith
      | func (r : R) : LinearMap U U \cowith {
        | func u => r *c u
        | func-+ => *c-ldistr
        | func-*c => inv *c-assoc *> pmap (`*c _) R.*-comm *> *c-assoc
      }
      | func-+ => exts \lam u => *c-rdistr
      | func-ide => exts \lam u => ide_*c
      | func-* => exts \lam u => pmap (`*c u) R.*-comm *> *c-assoc
  }