\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, GSet {
  | **-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 **_zro {g : G} : g **  =  => rewrite (inv *c_zro-right, **_*c, *c_zro-left, *c_zro-left) idp

  \lemma **_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 _ => **_ide
}

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