Groups

Definition of the notion of Group

Definition is_CGroup (G : CMonoid) (inv : CSetoid_un_op G) :=
  forall x, is_inverse csg_op 0 x (inv x).

Record CGroup : Type :=
  {cg_crr :> CMonoid;
   cg_inv : CSetoid_un_op cg_crr;
   cg_proof : is_CGroup cg_crr cg_inv}.

Notation "− x" := (cg_inv x) (at level 2, right associativity).

Definition cg_minus (G : CGroup) (x y : G) := x[+] [--]y.

In the names of lemmas, we will denote − with inv, and − with minus.

Infix "−" := cg_minus (at level 50, left associativity).

Group axioms

Let G be a group.

Section CGroup_axioms.
Variable G : CGroup.

Lemma cg_inverse : forall x : G, is_inverse csg_op 0 x [--] x.

End CGroup_axioms.

Group basics

General properties of groups. Let G be a group.

Section CGroup_basics.
Variable G : CGroup.

Lemma cg_rht_inv_unfolded : forall x : G, x[+] [--] x [=] 0.

Lemma cg_lft_inv_unfolded : forall x : G, [--] x[+]x [=] 0.

Lemma cg_minus_correct : forall x : G, x [-] x [=] 0.

Lemma cg_inverse' : forall x : G, is_inverse csg_op 0 [--] x x.

Lemma cg_minus_unfolded : forall x y : G, x [-] y [=] x[+] [--] y.

Lemma cg_minus_wd : forall x x' y y' : G, x [=] x' -> y [=] y' -> x [-] y [=] x' [-] y'.

Lemma cg_minus_strext : forall x x' y y' : G, x [-] y [#] x' [-] y' -> x [#] x' or y [#] y'.

Definition cg_minus_is_csetoid_bin_op : CSetoid_bin_op G :=
Build_CSetoid_bin_op G (cg_minus (G:=G)) cg_minus_strext.

Lemma grp_inv_assoc : forall x y : G, x[+]y [-] y [=] x.

Lemma cg_inv_unique : forall x y : G, x[+]y [=] 0 -> y [=] [--] x.

Lemma cg_inv_inv : forall x : G, [--] [--] x [=] x.

Lemma cg_cancel_lft : forall x y z : G, x[+]y [=] x[+]z -> y [=] z.

Lemma cg_cancel_rht : forall x y z : G, y[+]x [=] z[+]x -> y [=] z.

Lemma cg_inv_unique' : forall x y : G, x[+]y [=] 0 -> x [=] [--] y.

Lemma cg_inv_unique_2 : forall x y : G, x [-] y [=] 0 -> x [=] y.

Lemma cg_zero_inv : [--] (0:G) [=] 0.

Lemma cg_inv_zero : forall x : G, x [-] 0 [=] x.

Lemma cg_inv_op : forall x y : G, [--] (x[+]y) [=] [--] y[+] [--] x.

Useful for interactive proof development.

Lemma x_minus_x : forall x y : G, x [=] y -> x [-] y [=] 0.

Sub-groups

Let P be a predicate on G containing 0 and closed under + and − .

Section SubCGroups.
Variable P : G -> CProp.
Variable Punit : P 0.
Variable op_pres_P : bin_op_pres_pred _ P csg_op.
Variable inv_pres_P : un_op_pres_pred _ P cg_inv.

Let subcrr : CMonoid := Build_SubCMonoid _ _ Punit op_pres_P.
Let subinv : CSetoid_un_op subcrr := Build_SubCSetoid_un_op _ _ _ inv_pres_P.

Lemma isgrp_scrr : is_CGroup subcrr subinv.

Definition Build_SubCGroup : CGroup := Build_CGroup subcrr _ isgrp_scrr.

End SubCGroups.

End CGroup_basics.

Add Parametric Morphism c : (@cg_minus c) with signature (@cs_eq (cg_crr c)) ==> (@cs_eq c) ==> (@cs_eq c) as cg_minus_wd_morph.
Qed.

Associative properties of groups

Let G be a group.

Section Assoc_properties.
Variable G : CGroup.

Lemma assoc_2 : forall x y z : G, x[+] (y [-] z) [=] x[+]y [-] z.

Lemma zero_minus : forall x : G, 0 [-] x [=] [--] x.

Lemma cg_cancel_mixed : forall x y : G, x [=] x [-] y[+]y.

Lemma plus_resp_eq : forall x y z : G, y [=] z -> x[+]y [=] x[+]z.

End Assoc_properties.

Apartness in Constructive Groups

Specific properties of apartness. Let G be a group.

Section cgroups_apartness.
Variable G : CGroup.

Lemma cg_add_ap_zero : forall x y : G, x[+]y [#] 0 -> x [#] 0 or y [#] 0.

Lemma op_rht_resp_ap : forall x y z : G, x [#] y -> x[+]z [#] y[+]z.

Lemma cg_ap_cancel_rht : forall x y z : G, x[+]z [#] y[+]z -> x [#] y.

Lemma plus_cancel_ap_rht : forall x y z : G, x[+]z [#] y[+]z -> x [#] y.

Lemma minus_ap_zero : forall x y : G, x [#] y -> x [-] y [#] 0.

Lemma zero_minus_apart : forall x y : G, x [-] y [#] 0 -> x [#] y.

Lemma inv_resp_ap_zero : forall x : G, x [#] 0 -> [--] x [#] 0.

Lemma inv_resp_ap : forall x y : G, x [#] y -> [--] x [#] [--] y.

Lemma minus_resp_ap_rht : forall x y z : G, x [#] y -> x [-] z [#] y [-] z.

Lemma minus_resp_ap_lft : forall x y z : G, x [#] y -> z [-] x [#] z [-] y.

Lemma minus_cancel_ap_rht : forall x y z : G, x [-] z [#] y [-] z -> x [#] y.

End cgroups_apartness.

Section CGroup_Ops.

The Group of bijective Setoid functions

Definition PS_Inv (A : CSetoid) : PS_as_CMonoid A -> PS_as_CMonoid A.
Defined.

Definition Inv_as_un_op (A : CSetoid) : CSetoid_un_op (PS_as_CMonoid A).
Defined.

Lemma PS_is_CGroup :
forall A : CSetoid, is_CGroup (PS_as_CMonoid A) (Inv_as_un_op A).

Definition PS_as_CGroup (A : CSetoid) :=
Build_CGroup (PS_as_CMonoid A) (Inv_as_un_op A) (PS_is_CGroup A).

Functional operations

As before, we lift our group operations to the function space of the group.

Let G be a group and F,F':(PartFunct G) with domains given respectively by P and Q.

Variable G : CGroup.

Variables F F' : PartFunct G.

Section Part_Function_Inv.

Lemma part_function_inv_strext : forall x y (Hx : P x) (Hy : P y),
[--] (F x Hx) [#] [--] (F y Hy) -> x [#] y.

Definition Finv := Build_PartFunct _ _
(dom_wd _ F) (fun x Hx => [--] (F x Hx)) part_function_inv_strext.

End Part_Function_Inv.

Section Part_Function_Minus.

Lemma part_function_minus_strext : forall x y (Hx : Conj P Q x) (Hy : Conj P Q y),
F x (Prj1 Hx) [-] F' x (Prj2 Hx) [#] F y (Prj1 Hy) [-] F' y (Prj2 Hy) -> x [#] y.

Definition Fminus := Build_PartFunct G _ (conj_wd (dom_wd _ F) (dom_wd _ F'))
(fun x Hx => F x (Prj1 Hx) [-] F' x (Prj2 Hx)) part_function_minus_strext.

End Part_Function_Minus.

Let R:G->CProp.

Variable R:G -> CProp.

Lemma included_FInv : ⊆ R P -> ⊆ R (Dom Finv).

Lemma included_FInv' : ⊆ R (Dom Finv) -> ⊆ R P.

Lemma included_FMinus : ⊆ R P -> ⊆ R Q -> ⊆ R (Dom Fminus).

Lemma included_FMinus' : ⊆ R (Dom Fminus) -> ⊆ R P.

Lemma included_FMinus'' : ⊆ R (Dom Fminus) -> ⊆ R Q.

End CGroup_Ops.

Notation "{--} x" := (Finv x) (at level 2, right associativity).

Infix "{-}" := Fminus (at level 50, left associativity).