diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-06-24 17:10:14 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2016-06-24 17:10:14 -0400 |
| commit | 7488addb5938b203d1c9402908cc9b440d9573b6 (patch) | |
| tree | 2ec78b0f4a386225bcd77e53170711f2db431f4d /src | |
| parent | 4666ede72bbb35cd889cd62888339791ee7ab3a3 (diff) | |
isomorphism_to_subgroup_group
Diffstat (limited to 'src')
| -rw-r--r-- | src/Algebra.v | 25 |
1 files changed, 22 insertions, 3 deletions
diff --git a/src/Algebra.v b/src/Algebra.v index e45ab8c33..a46b010b5 100644 --- a/src/Algebra.v +++ b/src/Algebra.v @@ -283,8 +283,8 @@ Module Group. Admitted. End Homomorphism. - Section SurjectiveHomomorphism. - Lemma surjective_homomorphism_group + Section GroupByHomomorphism. + Lemma surjective_homomorphism_from_group {G EQ OP ID INV} {groupG:@group G EQ OP ID INV} {H eq op id inv} {Equivalence_eq: @Equivalence H eq} {eq_dec: forall x y, {eq x y} + {~ eq x y}} @@ -309,7 +309,26 @@ Module Group. repeat rewrite <-?phi_op, <-?phi_inv, <-?phi_id; f_equiv; auto using associative, left_identity, right_identity, left_inverse, right_inverse. Qed. - End SurjectiveHomomorphism. + + Lemma isomorphism_to_subgroup_group + {G EQ OP ID INV} + {Equivalence_EQ: @Equivalence G EQ} {eq_dec: forall x y, {EQ x y} + {~ EQ x y}} + {Proper_OP:Proper(EQ==>EQ==>EQ)OP} + {Proper_INV:Proper(EQ==>EQ)INV} + {H eq op id inv} {groupG:@group H eq op id inv} + {phi} + {eq_phi_EQ: forall x y, eq (phi x) (phi y) -> EQ x y} + {phi_op : forall a b, phi (OP a b) = op (phi a) (phi b)} + {phi_inv : forall a, phi (INV a) = inv (phi a)} + {phi_id : phi ID = id} + : @group G EQ OP ID INV. + Proof. + repeat split; eauto with core typeclass_instances; intros; + eapply eq_phi_EQ; + repeat rewrite ?phi_op, ?phi_inv, ?phi_id; + auto using associative, left_identity, right_identity, left_inverse, right_inverse. + Qed. + End GroupByHomomorphism. End Group. Require Coq.nsatz.Nsatz. |