\import Algebra.Group
\import Algebra.Group.GSet.ExampleActions
\import Algebra.Group.GSet
\import Algebra.Module
\import Algebra.Module.LinearMap
\import Algebra.Pointed
\import Algebra.Ring
\import Meta
\import Paths
\import Paths.Meta

-- basic reference right now is https://www.uni-math.gwdg.de/tammo/rep.pdf
-- REPRESENTATION THEORY Tammo tom Dieck
-- also : https://www.maths.dur.ac.uk/users/jack.g.shotton/repthy/index.html

\class LinRepres \extends LModule, GroupAction {
  | **-ldistr {g :  G} {e e' : E} : g ** (e + e') = g ** e + g ** e'
  | **-*c {g :  G} {e : E} {c : R} : g ** (c *c e) = c *c (g ** e)

  \lemma g**-zro {g : G} : g **  =  => rewrite (inv *c_zro-right, **-*c, *c_zro-left, *c_zro-left) idp

  \lemma g**-negative {g : G} {e : E} : g ** negative e = negative (g ** e) => rewrite (inv neg_ide_*c, **-*c, neg_ide_*c) idp

  \func toLinearMap(g : G) : LinearMap \this \this \cowith
    | func e => g ** e
    | func-+ => **-ldistr
    | func-*c => **-*c

  \lemma toLinearMap-ide : toLinearMap ide = LinearMap.id
    => exts \lam _ => unfold id-action
}

\func TrivialAction {R : Ring} (E : LModule R) (G : Group) : LinRepres R G \cowith
  | LModule => E
  | GroupAction => trivialAction G E
  | **-*c => idp
  | **-ldistr => idp