Abelian Groups

Now we introduce commutativity and add some results.

Definition is_CAbGroup (G : CGroup) := commutes (csg_op (c:=G)).

Record CAbGroup : Type :=
{cag_crr :> CGroup;
cag_proof : is_CAbGroup cag_crr}.

Section AbGroup_Axioms.

Variable G : CAbGroup.

Let G be an Abelian Group.

Lemma CAbGroup_is_CAbGroup : is_CAbGroup G.

Lemma cag_commutes : commutes (csg_op (c:=G)).

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

End AbGroup_Axioms.

Section SubCAbGroups.

Subgroups of an Abelian Group

Variable G : CAbGroup.
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 G be an Abelian Group and P be a (CProp-valued) predicate on G that contains 0 and is closed under + and −.

Let subcrr : CGroup := Build_SubCGroup _ _ Punit op_pres_P inv_pres_P.

Lemma isabgrp_scrr : is_CAbGroup subcrr.

Definition Build_SubCAbGroup : CAbGroup := Build_CAbGroup subcrr isabgrp_scrr.

End SubCAbGroups.

Section Various.

Basic properties of Abelian groups

Variable G : CAbGroup.

Let G be an Abelian Group.

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

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

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

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

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

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

End Various.

End Abelian_Groups.

Section Nice_Char.

Building an abelian group

In order to actually define concrete abelian groups, it is not in general practical to construct first a semigroup, then a monoid, then a group and finally an abelian group. The presence of commutativity, for example, makes many of the monoid proofs trivial. In this section, we provide a constructor that will allow us to go directly from a setoid to an abelian group.

We start from a setoid S with an element unit, a commutative and associative binary operation plus which is strongly extensional in its first argument and admits unit as a left unit, and a unary setoid function inv which inverts elements respective to plus.

Variable S : CSetoid.
Variable unit : S.
Variable plus : S -> S -> S.

Let S be a Setoid and unit:S, plus:S->S->S and inv a unary setoid operation on S. Assume that plus is commutative, associative and `left-strongly-extensional ((plus x z) [#] (plus y z) -> x [#] y), that unit is a left-unit for plus and (inv x) is a right-inverse of x w.r.t. plus.

Hypothesis plus_lext : forall x y z : S, plus x z [#] plus y z -> x [#] y.
Hypothesis plus_lunit : forall x : S, plus unit x [=] x.
Hypothesis plus_comm : forall x y : S, plus x y [=] plus y x.
Hypothesis plus_assoc : associative plus.

Variable inv : CSetoid_un_op S.

Hypothesis inv_inv : forall x : S, plus x (inv x) [=] unit.

Lemma plus_rext : forall x y z : S, plus x y [#] plus x z -> y [#] z.

Lemma plus_runit : forall x : S, plus x unit [=] x.

Lemma plus_is_fun : bin_fun_strext _ _ _ plus.

Lemma inv_inv' : forall x : S, plus (inv x) x [=] unit.

Definition plus_fun : CSetoid_bin_op S := Build_CSetoid_bin_fun _ _ _ plus plus_is_fun.

Definition Build_CSemiGroup' : CSemiGroup.
Defined.

Definition Build_CMonoid' : CMonoid.
Defined.

Definition Build_CGroup' : CGroup.
Defined.

Definition Build_CAbGroup' : CAbGroup.
Defined.

End Nice_Char.

Iteration

For reflection the following is needed; hopefully it is also useful.

Section Group_Extras.

Variable G : CAbGroup.

Fixpoint nmult (a:G) (n:nat) {struct n} : G :=
  match n with
  | O => 0
  | S p => a[+]nmult a p
  end.

Lemma nmult_wd : forall (x y:G) (n m:nat), (x [=] y) -> n = m -> nmult x n [=] nmult y m.

Lemma nmult_one : forall x:G, nmult x 1 [=] x.

Lemma nmult_Zero : forall n:nat, nmult 0 n [=] 0.

Lemma nmult_plus : forall m n x, nmult x m[+]nmult x n [=] nmult x (m + n).

Lemma nmult_mult : forall n m x, nmult (nmult x m) n [=] nmult x (m * n).

Lemma nmult_inv : forall n x, nmult [--]x n [=] [--] (nmult x n).

Lemma nmult_plus' : forall n x y, nmult x n[+]nmult y n [=] nmult (x[+]y) n.

Definition zmult a z := caseZ_diff z (fun n m => nmult a n[-]nmult a m).

Lemma zmult_char : forall (m n:nat) z, z = (m - n)%Z ->
forall x, zmult x z [=] nmult x m[-]nmult x n.

Lemma zmult_wd : forall (x y:G) (n m:Z), (x [=] y) -> n = m -> zmult x n [=] zmult y m.

Lemma zmult_one : forall x:G, zmult x 1 [=] x.

Lemma zmult_min_one : forall x:G, zmult x (-1) [=] [--]x.

Lemma zmult_zero : forall x:G, zmult x 0 [=] 0.

Lemma zmult_Zero : forall k:Z, zmult 0 k [=] 0.

Lemma zmult_plus : forall m n x, zmult x m[+]zmult x n [=] zmult x (m + n).

Lemma zmult_mult : forall m n x, zmult (zmult x m) n [=] zmult x (m * n).

Lemma zmult_plus' : forall z x y, zmult x z[+]zmult y z [=] zmult (x[+]y) z.

End Group_Extras.