Quotients of Abelian Groups |
Require
Export
equiv_.
Require
Export
abgroup_.
Require
quot_.
Implicit Arguments On.
Module
AbGroup_Quot_.
Export
Quot_.
Export
AbGroup_.
Record
Compatible_Group [A:Group_Data; Q:(Equivalence A)] : Prop := {
add_compatible : (Compatible2 Q Q [x,y:A](class Q (add x y)));
opp_compatible : (Compatible Q [x:A](class Q (opp x)))
}.
Section
Group_Quot.
Variable
A:Group; Q:(Equivalence A); HQ:(Compatible_Group Q).
Definition
class_eq_Q := (!class_eq ? Q).
Hints
Resolve class_eq_Q.
Local
B := (quot Q).
Local
Bop : B->B->B.
Proof
.
Apply (quot_law2 Q (!add A)).
Abstract NewDestruct HQ; Trivial.
Defined
.
Local
Bid : B := (class Q (!zero A)).
Local
Biv : B->B.
Proof
.
Apply (quot_law Q (!opp A)).
Abstract NewDestruct HQ; Trivial.
Defined
.
Local
B_data : Group_Data := (Build_Group_Data Bop Bid Biv).
Remark
B_theory :
(Group_Theory (!add B_data) (!zero B_data) (!opp B_data)).
Proof
.
Split; Simpl; Unfold Bop Bid Biv; Intros.
Lift x; Lift y; Lift z; Unfold quot_law2.
Repeat Rewrite fact2_eq; Auto.
Lift x; Lift y; Unfold quot_law2.
Repeat Rewrite fact2_eq; Auto.
Lift x; Unfold quot_law2; Repeat Rewrite fact2_eq; Auto.
Lift x; Unfold quot_law2 quot_law.
Repeat Rewrite fact_eq; Repeat Rewrite fact2_eq; Auto.
Qed
.
Definition
group_quot : Group.
Proof
.
Split with B_data.
Exact B_theory.
Defined
.
End
Group_Quot.
End
AbGroup_Quot_.