\import Algebra.Module
\import Algebra.Monoid
\import Algebra.Ring
\import Algebra.Ring.RingHom
\import Paths

\class PseudoAlgebra \extends LModule, PseudoRing {
  \override R : CRing
  | *c-comm-left  {r : R} {a b : E} : r *c (a * b) = (r *c a) * b
  | *c-comm-right {r : R} {a b : E} : r *c (a * b) = a * (r *c b)
}

\class AAlgebra \extends PseudoAlgebra, Ring {
  | coefMap : R -> E
  | coefMap_*c {x : R} : coefMap x = x *c 
  \default coefMap \as coefMap-impl x => x *c 
  \default coefMap_*c \as coefMap_*c-impl {x} : coefMap-impl x = x *c  => idp

  \func coefHom : RingHom R \this \cowith
    | func => coefMap
    | func-+ => coefMap_*c *> *c-rdistr *> inv (pmap2 (+) coefMap_*c coefMap_*c)
    | func-ide => coefMap_*c *> ide_*c
    | func-* => coefMap_*c *> *c-assoc *> pmap (_ *c) (inv ide-left) *> *c-comm-left *> inv (pmap2 (*) coefMap_*c coefMap_*c)

  \lemma coefMap_natCoef {n : Nat} : coefMap (R.natCoef n) = natCoef n
    => coefHom.func-natCoef
}

\class PseudoCAlgebra \extends PseudoAlgebra, CRing
  | *c-comm-right => pmap (_ *c) *-comm *> *c-comm-left *> *-comm

\class CAlgebra \extends AAlgebra, PseudoCAlgebra

\func homAlgebra {R E : CRing} (f : RingHom R E) : CAlgebra \cowith
  | CRing => E
  | LModule => homLModule f
  | *c-comm-left => inv *-assoc

\func ringAlgebra {R : CRing} : CAlgebra R
  => homAlgebra RingHom.id

\func \infixl  *a {R : CRing} {A : AAlgebra R} {X : LModule A} (a : R) (x : X) : X
  => coefMap a *c x

\lemma *a-assoc {R : CRing} {A : AAlgebra R} {X : LModule A} {a b : R} {x : X} : a * b *a x = a *a (b *a x)
  => pmap (`*c x) A.coefHom.func-* *> *c-assoc