\import Algebra.Group
\import Algebra.Group.Sub
\import Algebra.Monoid
\import Algebra.Monoid.Category
\import Algebra.Pointed
\import Algebra.Pointed.Category
\import Category (Cat, Precat)
\import Category.Functor
\import Category.Meta
\import Category.Subcat
\import Equiv
\import Function
\import Function.Meta
\import Logic
\import Logic.Meta
\import Paths
\import Paths.Meta
\import Set.Category
\open Group

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

  \lemma func-inverse {x : Dom} : func (inverse x) = inverse (func x) => check-for-inv $
    func x * func (inverse x)   ==< inv func-* >==
    func (x * inverse x)        ==< pmap func inverse-right >==
    func ide                    ==< func-ide >==
    ide `qed

  \func Kernel : NormalSubGroup Dom \cowith
    | contains x => func x = ide
    | contains_ide => func-ide
    | contains_inverse {x : Dom} (p : func x = ide) =>
      func (inverse x)     ==< func-inverse >==
      inverse (func x)     ==< pmap inverse p >==
      inverse ide          ==< Group.inverse_ide >==
      ide `qed

    | isNormal g {h} p =>
      func (g * h * inverse g)                 ==< func-* >==
      func (g * h) * (func (inverse g))        ==< pmap (`* (func (inverse g))) func-* >==
      func g * func h * (func (inverse g))     ==< pmap (\lam z => func g * z * (func (inverse g))) p >==
      func g * ide * (func (inverse g))        ==< pmap (`* (func (inverse g))) ide-right >==
      func g * (func (inverse g))              ==< inv func-* >==
      func (g * inverse g)                     ==< pmap func inverse-right >==
      func ide                                 ==< func-ide >==
      ide `qed

    | contains_* {x} {y} p q =>
      func (x * y)     ==< func-* >==
      func x * func y  ==< pmap (`* func y) p >==
      ide * func y     ==< ide-left >==
      func y           ==< q >==
      ide `qed

  \func TrivialKernel : \Prop => \Pi {g : Dom} -> Kernel g -> g = ide

  \func same-images-test {a b : Dom} (p : func a = func b) : Kernel (inverse a * b) =>
    func (inverse a * b)          ==< func-* >==
    func (inverse a) * func b     ==< pmap (`* func b) func-inverse >==
    inverse (func a) * func b     ==< equality-corrolary (func a) (func b) p >==
    ide `qed

  \lemma Kernel-injectivity-test (p : TrivialKernel) : isInj func =>
    \lam q => equality-check (p (same-images-test q))

  \lemma Kernel-injectivity-corrolary (p : isInj func) : TrivialKernel =>
    \lam q => p (q *> inv func-ide)

  \func isIsomorphism : \Prop => \Sigma (isInj func) (isSurj func)
}

\func quotient-map {S : Group} {H : NormalSubGroup S} : GroupHom S H.quotient \cowith
  | func (s : S) => NormalSubGroup.quotient-proj-setwise s
  | func-ide => idp
  | func-* => idp

\instance GroupCat : Cat Group
  | Hom => GroupHom
  | id => id
  | o {x y z : Group} (g : GroupHom y z) (f : GroupHom x y) => \new GroupHom {
    | func x => g (f x)
    | func-ide => pmap g f.func-ide *> g.func-ide
    | func-* => pmap g f.func-* *> g.func-*
  }
  | id-left => idp
  | id-right => idp
  | o-assoc => idp
  | univalence => sip \lam f _ => exts (func-ide {f}, \lam _ _ => func-* {f}, \lam _ => GroupHom.func-inverse {f})
  \where {
    \func id (M : Group) : GroupHom M M \cowith
      | func x => x
      | func-ide => idp
      | func-* => idp
  }

\instance ImageGroup (f : GroupHom) : Group
  | Monoid => ImageMonoid f
  | inverse a => (inverse a., TruncP.map a. \lam s => (inverse s., f.func-inverse *> pmap inverse s.))
  | inverse-left => ext inverse-left
  | inverse-right => ext inverse-right


\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
}

\instance AddGroupCat : Cat AddGroup
  | Hom G H => AddGroupHom G H
  | id => id
  | o g f => \new AddGroupHom {
    | func x => g (f x)
    | func-+ => pmap g func-+ *> func-+
  }
  | id-left => idp
  | id-right => idp
  | o-assoc => idp
  | univalence => sip (\lam {X} {A} {B} (p1 : AddGroupHom) p2 => exts (p1.func-zro, \lam _ _ => p1.func-+, AddGroup.negative-equality A B p1.func-zro p1.func-+))
  \where {
    \func id (G : AddGroup) : AddGroupHom G G \cowith
      | func x => x
      | func-+ => idp

    \func forgetToAddMonoid : Functor AddGroupCat AddMonoidCat \cowith
      | F A => A
      | Func f => f
      | Func-id => idp
      | Func-o => idp

    \func forget : Functor AddGroupCat SetCat \cowith
      | F R => R
      | Func f => func {f}
      | Func-id => idp
      | Func-o => idp
  }

\instance AbGroupCat : Cat AbGroup
  => subCat (\new Embedding {AbGroup} {AddGroup} {
    | f A => A
    | isEmb A B => \new Retraction {
      | sec => AbGroup.equals A B
      | f_sec => idpe
    }
  })
  \where {
    \func forgetToAddGroup : Functor AbGroupCat AddGroupCat \cowith
      | F A => A
      | Func f => f
      | Func-id => idp
      | Func-o => idp

    \func forget : Functor AbGroupCat SetCat \cowith
      | F R => R
      | Func f => func {f}
      | Func-id => idp
      | Func-o => idp
  }

\instance KerAddGroup (f : AddGroupHom) : AddGroup
  | AddMonoid => KerAddMonoid f
  | negative a => (negative a., f.func-negative *> pmap negative a. *> AddGroup.negative_zro)
  | negative-left => ext negative-left
  | negative-right => ext negative-right

\func KerGroupHom (f : AddGroupHom) : AddGroupHom (KerAddGroup f) f.Dom \cowith
  | AddMonoidHom => KerMonoidHom f

\instance KerAbGroup {A : AbGroup} (f : AddGroupHom A) : AbGroup
  | AddGroup => KerAddGroup f
  | AbMonoid => KerAbMonoid f

\lemma kernel=0<->inj {f : AddGroupHom} : isInj f <-> (\Pi (x : Kernel f) -> x = )
  => (\lam fi x => ext $ fi $ x. *> inv func-zro,
      \lam c {a} {a'} p => AddGroup.fromZero $ pmap __. (c (a - a', func-+ *> pmap (_ +) f.func-negative *> AddGroup.toZero p)))

\instance ImageAddGroup (f : AddGroupHom) : AddGroup
  | AddMonoid => ImageAddMonoid f
  | negative a => (negative a., TruncP.map a. \lam s => (negative s., f.func-negative *> pmap negative s.))
  | negative-left => ext negative-left
  | negative-right => ext negative-right

\func ImageGroupLeftHom (f : AddGroupHom) : AddGroupHom f.Dom (ImageAddGroup f) \cowith
  | AddMonoidHom => ImageMonoidLeftHom f

\func ImageGroupRightHom (f : AddGroupHom) : AddGroupHom (ImageAddGroup f) f.Cod \cowith
  | AddMonoidHom => ImageMonoidRightHom f

\instance ImageAbGroup {A : AddGroup} {B : AbGroup} (f : AddGroupHom A B) : AbGroup
  | AddGroup => ImageAddGroup f
  | AbMonoid => ImageAbMonoid f