\import Algebra.Meta
\import Algebra.Module
\import Algebra.Monoid
\import Algebra.Ring
\import Algebra.Ring.RingHom
\import Algebra.Ring.MPoly
\import Logic.Meta
\import Paths

\class AAlgebra \extends Ring, LModule {
  \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)

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

\class CAlgebra \extends AAlgebra, CRing

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