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