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" := (@group_inverse _ _ 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.