Abelian groups |
Require
Export
abmonoid.
Require
Export
cgroup.
Implicit Arguments On.
Module
AbGroup <: Cat_Sig.
Export
Misc.
Section
Group_Theory.
Variable
A:Type; add:A->A->A; zero:A; opp:A->A.
Record
Group_Theory : Prop := {
ax_add_assoc : (x,y,z:A) (add x (add y z))==(add (add x y) z);
ax_add_commut : (x,y:A) (add x y)==(add y x);
ax_zero_sx : (x:A) (add zero x)==x;
ax_opp_sx : (x:A) (add (opp x) x)==zero
}.
End
Group_Theory.
Record
Group_Data : Type := {
group_carrier :> Type;
add : group_carrier->group_carrier->group_carrier;
zero : group_carrier;
opp : group_carrier->group_carrier
}.
Implicits
zero [1].
Record
Group : Type := {
group_data :> Group_Data;
group_theory :>
(Group_Theory (!add group_data) (!zero group_data) (!opp group_data))
}.
Definition
Obj : Type := Group.
Section
Group_Facts.
Variable
A:Group.
Lemma
add_assoc : (x,y,z:A) (add x (add y z))==(add (add x y) z).
Proof
.
Intros; Apply (ax_add_assoc A).
Qed
.
Lemma
add_commut : (x,y:A) (add x y)==(add y x).
Proof
.
Intros; Apply (ax_add_commut A).
Qed
.
Lemma
zero_sx : (x:A) (add zero x)==x.
Proof
.
Intros; Apply (ax_zero_sx A).
Qed
.
Lemma
opp_sx : (x:A) (add (opp x) x)==zero.
Proof
.
Intros; Apply (ax_opp_sx A).
Qed
.
Hints
Resolve add_assoc add_commut zero_sx opp_sx.
Lemma
zero_dx : (x:A) (add x zero)==x.
Proof
.
Intros; Rewrite add_commut; Auto.
Qed
.
Lemma
opp_dx : (x:A) (add x (opp x))==zero.
Proof
.
Intros; Rewrite add_commut; Auto.
Qed
.
Lemma
add_sx_cancel : (x,y,z:A) (add x y)==(add x z) -> y==z.
Proof
.
Intros.
Rewrite <- zero_sx with y.
Rewrite <- zero_sx with z.
Rewrite <- opp_sx with x.
Do 2 Rewrite <- add_assoc.
Rewrite H.
Reflexivity.
Qed
.
End
Group_Facts.
Hints
Resolve add_assoc add_commut zero_sx opp_sx add_sx_cancel zero_dx
opp_dx.
Record
Morph_Theory [A,B:Group; f:A->B] : Prop := {
morph_add : (x,y:A) (f (add x y))==(add (f x) (f y));
morph_opp : (x:A) (f (opp x))==(opp (f x))
}.
Record
Group_Morph [A,B:Group] : Type := {
morph_data :> A->B;
morph_theory :> (Morph_Theory morph_data)
}.
Definition
Morph [A,B:Group] : Type := (Group_Morph A B).
Lemma
morph_extens : (A,B:Group; f,g:(Morph A B))
((x:A)(f x)==(g x)) -> f==g.
Proof
.
NewDestruct f; NewDestruct g; Simpl; Intros.
Assert U : morph_data0 == morph_data1.
Apply nondep_extensionality; Assumption.
NewDestruct U.
Assert U : morph_theory0 == morph_theory1.
Apply proof_irrelevance.
NewDestruct U.
Reflexivity.
Qed
.
Section
morph_comp.
Variable
A,B,C:Group.
Variable
f:(Morph B C); g:(Morph A B).
Local
h [x:A] : C := (f (g x)).
Remark
h_th : (Morph_Theory h).
Proof
.
Unfold h; Split; Intros.
Rewrite (morph_add g).
Rewrite (morph_add f).
Reflexivity.
Rewrite (morph_opp g).
Rewrite (morph_opp f).
Reflexivity.
Qed
.
Definition
morph_comp : (Morph A C).
Proof
.
Split with h;
Apply h_th.
Defined
.
End
morph_comp.
Definition
morph_id [A:Group] : (Morph A A).
Proof
.
Intros.
Split with [x:A]x.
Abstract Split; Auto.
Defined
.
Implicits
morph_id [1].
Lemma
morph_comp_assoc : (A,B,C,D:Group)
(h:(Morph C D); g:(Morph B C); f:(Morph A B))
(morph_comp h (morph_comp g f))==(morph_comp (morph_comp h g) f).
Proof
.
Intros; Apply morph_extens; Trivial.
Qed
.
Lemma
morph_id_sx : (A,B:Group; f:(Morph A B))
(morph_comp morph_id f)==f.
Proof
.
Intros; Apply morph_extens; Trivial.
Qed
.
Lemma
morph_id_dx : (A,B:Group; f:(Morph A B))
(morph_comp f morph_id)==f.
Proof
.
Intros; Apply morph_extens; Trivial.
Qed
.
Definition
abmonoid_of_abgroup [A:Group] : AbMonoid.Monoid.
Proof
.
Intros.
Split with (AbMonoid.Build_Monoid_Data (!add A) (!zero A)).
Abstract NewDestruct (!group_theory A); Split; Simpl; Auto.
Defined
.
Definition
cgroup_of_abgroup [A:Group] : CGroup.Group.
Proof
.
Intros.
Split with (CGroup.Build_Group_Data (!add A) (!zero A) (!opp A)).
Abstract NewDestruct (!group_theory A); Split; Simpl; Auto.
Defined
.
Definition
abgroup_of_cgroup [A:CGroup.Group] : Group.
Proof
.
Intros.
Split with (Build_Group_Data (!CGroup.mul A) (!CGroup.one A) (!CGroup.inv A)).
Abstract NewDestruct (!CGroup.group_theory A); Split; Simpl; Auto.
Defined
.
End
AbGroup.