Library Group

Require Import Utf8.
Require Export Monoid.

Set Implicit Arguments.

Generalizable All Variables.

Definition is_inverse_of M' (M : ComputationalMonoid M') : M → M → Prop :=
  fun x y ⇒ x ★ y = id ∧ y ★ x = id.
Definition inverse_of M' (M : ComputationalMonoid M') : M → Type :=
  fun x ⇒ { x' | is_inverse_of _ x x' }.

Record ComputationalGroup (M : Type) :=
  {
    group_monoid :> ComputationalMonoid M;
    group_inverse : group_monoid → group_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 G2 → GroupHomomorphism G0 G1 → GroupHomomorphism G0 G2
  := fun m1 m2 ⇒ compose_monoid_homomorphisms m1 m2.