# Library Group

Require Import Utf8.
Require Export Monoid.

Set Implicit Arguments.

Generalizable All Variables.

Definition is_inverse_of M' (M : ComputationalMonoid M') : MMProp :=
fun x yx y = id y x = id.
Definition inverse_of M' (M : ComputationalMonoid M') : MType :=
fun x{ x' | is_inverse_of _ x x' }.

Record ComputationalGroup (M : Type) :=
{
group_monoid :> ComputationalMonoid M;
group_inverse : group_monoidgroup_monoid
}.

Class IsGroup G' (G : ComputationalGroup G') : Prop :=
{
GroupIsMonoid : IsMonoid G;
group_inverse_is_inverse : x, is_inverse_of _ x (group_inverse G x)
}.

Existing Instance GroupIsMonoid.

Record > Group (G : Type) :=
{
cgroup :> ComputationalGroup G;
is_group :> IsGroup cgroup
}.

Notation "i -1" := _ _ i) (at level 10) : type_scope.

## Group Homomorphisms

Definition IsGroupHomomorphism
`(G0H : @IsGroup G0' G0)
`(G1H : @IsGroup G1' G1)
:= MonoidHomomorphism (M0 := G0) _ (M'0 := G1) _.
Definition GroupHomomorphism
`(G0 : Group G0')
`(G1 : Group G1')
:= IsGroupHomomorphism (is_group G0) (is_group G1).
Definition identity_group_homomorphism `(G0 : Group G0') : GroupHomomorphism G0 G0
:= identity_monoid_homomorphism _.
Definition compose_group_homomorphisms
`(G0 : Group G0')
`(G1 : Group G1')
`(G2 : Group G2')
: GroupHomomorphism G1 G2GroupHomomorphism G0 G1GroupHomomorphism G0 G2
:= fun m1 m2compose_monoid_homomorphisms m1 m2.