From ba82338180592787d95e756b7feb30f71ea70a73 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 6 Feb 2006 14:00:18 +0000 Subject: [PATCH] Basic facts about group morphisms. --- matita/library/algebra/groups.ma | 34 ++++++++++++++++++++++++++++++++ 1 file changed, 34 insertions(+) diff --git a/matita/library/algebra/groups.ma b/matita/library/algebra/groups.ma index 1ef9249fc..5c5e1f00c 100644 --- a/matita/library/algebra/groups.ma +++ b/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 -- 2.39.2