\import Algebra.Group
\import Algebra.Meta
\import Algebra.Monoid
\import Algebra.Monoid.MonoidHom
\import Algebra.Pointed
\import Function
\import Function.Meta
\import Paths

\record GroupHom \extends MonoidHom {
  \override Dom : Group
  \override Cod : Group

  | func-ide => cancel_*-left (func ide) $ inv func-* *> pmap func ide-left *> inv ide-right

  \lemma func-inverse {a : Dom} : func (inverse a) = inverse (func a)
    => func-InvElem (Group.makeInv a) (Group.makeInv (func a)) idp

  \func IsIsomorphism : \Prop
    => \Sigma (IsInj func) (IsSurj func)
} \where {
  \func id {G : Group} : GroupHom G G \cowith
    | func x => x
    | func-* => idp

  \func \fixl  compose \alias \infixl  ∘ {G H K : Group} (g : GroupHom H K) (f : GroupHom G H) : GroupHom G K \cowith
    | func x => g (f x)
    | func-* => pmap g f.func-* *> g.func-*
}

\func conjugateHom {E : Group} (g : E) : GroupHom E E \cowith
  | func => conjugate g
  | func-ide => equation.group
  | func-* => equation.group

\record AddGroupHom \extends AddMonoidHom {
  \override Dom : AddGroup
  \override Cod : AddGroup
  | func-zro => AddGroup.cancel-left (func ) (inv func-+ *> pmap func zro-right *> inv zro-right)

  \lemma func-negative {x : Dom} : func (negative x) = negative (func x)
    => AddGroup.cancel-left (func x) (inv (negative-right *> inv (pmap func negative-right *> func-zro) *> func-+))

  \lemma func-minus {x y : Dom} : func (x - y) = func x - func y
    => func-+ *> pmap (_ +) func-negative

  \lemma injective (p : \Pi {a : Dom} -> func a =  -> a = ) : IsInj func
    => \lam q => AddGroup.fromZero $ p $ func-+ *> pmap (_ +) func-negative *> AddGroup.toZero q

  \lemma func-*i {n : Int} {x : Dom} : func (n AddGroup.*i x) = n AddGroup.*i func x \elim n
    | pos n => func-*n
    | neg n => func-*n *> pmap (n AddMonoid.*n) func-negative
} \where {
  \func toGroupHom {G H : AddGroup} (f : AddGroupHom G H) : GroupHom (AddGroup.toGroup G) (AddGroup.toGroup H) \cowith
    | func x => f x
    | func-* => f.func-+

  \func fromGroupHom {G H : Group} (f : GroupHom G H) : AddGroupHom (AddGroup.fromGroup G) (AddGroup.fromGroup H) \cowith
    | func x => f x
    | func-+ => f.func-*

  \func id {G : AddGroup} : AddGroupHom G G \cowith
    | func x => x
    | func-+ => idp

  \func \fixl  compose \alias \infixl  ∘ {A B C : AddGroup} (g : AddGroupHom B C) (f : AddGroupHom A B) : AddGroupHom A C \cowith
    | func x => g (f x)
    | func-+ => pmap g f.func-+ *> g.func-+
}