Quotients of Groups |
Require
Export
equiv.
Require
Export
group.
Require
quot.
Implicit Arguments On.
Module
Group_Quot.
Export
Quot.
Export
Group.
Record
Compatible_Group [A:Group_Data; Q:(Equivalence A)] : Prop := {
mul_compatible : (Compatible2 Q Q [x,y:A](class Q (mul x y)));
inv_compatible : (Compatible Q [x:A](class Q (inv 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 (!mul A)).
Abstract NewDestruct HQ; Trivial.
Defined
.
Local
Bid : B := (class Q (!one A)).
Local
Biv : B->B.
Proof
.
Apply (quot_law Q (!inv A)).
Abstract NewDestruct HQ; Trivial.
Defined
.
Local
B_data : Group_Data := (Build_Group_Data Bop Bid Biv).
Remark
B_theory :
(Group_Theory (!mul B_data) (!one B_data) (!inv 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; 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
Group_Quot.