From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 6 Feb 2006 14:00:18 +0000 (+0000)
Subject: Basic facts about group morphisms.
X-Git-Tag: make_still_working~7627
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f423f114a31483595ea147d982275204cb5f8b0b;p=helm.git

Basic facts about group morphisms.
---

diff --git a/helm/software/matita/library/algebra/groups.ma b/helm/software/matita/library/algebra/groups.ma
index 1ef9249fc..5c5e1f00c 100644
--- a/helm/software/matita/library/algebra/groups.ma
+++ b/helm/software/matita/library/algebra/groups.ma
@@ -142,4 +142,38 @@ rewrite < (associative ? (is_semi_group ? (is_monoid ? G)));
 rewrite > (inv_is_right_inverse ? G);
 rewrite > (e_is_left_unit ? (is_monoid ? G));
 assumption.
+qed.
+
+(* Morphisms *)
+
+record morphism (G,G':Group) : Type ≝
+ { image: G → G';
+   f_morph: ∀x,y:G.image(x·y) = image x · image y
+ }.
+ 
+notation "hvbox(f˜ x)" with precedence 79
+for @{ 'morimage $f $x }.
+
+interpretation "Morphism image" 'morimage f x =
+ (cic:/matita/algebra/groups/image.con _ _ f x).
+ 
+theorem morphism_to_eq_f_1_1:
+ ∀G,G'.∀f:morphism G G'.f˜1 = 1.
+intros;
+apply (eq_op_x_y_op_z_y_to_eq G' (f˜1));
+rewrite > (e_is_left_unit ? (is_monoid ? G') ?);
+rewrite < (f_morph ? ? f);
+rewrite > (e_is_left_unit ? (is_monoid ? G));
+reflexivity.
+qed.
+ 
+theorem eq_image_inv_inv_image:
+ ∀G,G'.∀f:morphism G G'.
+  ∀x.f˜(x \sup -1) = (f˜x) \sup -1.
+intros;
+apply (eq_op_x_y_op_z_y_to_eq G' (f˜x));
+rewrite > (inv_is_left_inverse ? G');
+rewrite < (f_morph ? ? f);
+rewrite > (inv_is_left_inverse ? G);
+apply (morphism_to_eq_f_1_1 ? ? f).
 qed.
\ No newline at end of file