X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Flibrary%2Falgebra%2Fgroups.ma;h=9ab695239665e8418d6279f8f1609334e7ddada1;hb=e1e31e9c6a0bcdc60ace7e2e650cb8d719d07e33;hp=1301d34f923725ea583d1ea4fe47403e869fa33c;hpb=05f98d76325dba7c404dbae50ec759b2e7d1a6c8;p=helm.git diff --git a/matita/library/algebra/groups.ma b/matita/library/algebra/groups.ma index 1301d34f9..9ab695239 100644 --- a/matita/library/algebra/groups.ma +++ b/matita/library/algebra/groups.ma @@ -35,24 +35,6 @@ record Group : Type ≝ group_properties:> isGroup pregroup }. -(*notation < "G" -for @{ 'monoid $G }. - -interpretation "Monoid coercion" 'monoid G = - (cic:/matita/algebra/groups/monoid.con G).*) - -notation < "G" -for @{ 'type_of_group $G }. - -interpretation "Type_of_group coercion" 'type_of_group G = - (cic:/matita/algebra/groups/Type_of_Group.con G). - -notation < "G" -for @{ 'magma_of_group $G }. - -interpretation "magma_of_group coercion" 'magma_of_group G = - (cic:/matita/algebra/groups/Magma_of_Group.con G). - notation "hvbox(x \sup (-1))" with precedence 89 for @{ 'ginv $x }. @@ -76,8 +58,8 @@ intros (x y z); rewrite < (e_is_left_unit ? G); rewrite < (e_is_left_unit ? G z); rewrite < (inv_is_left_inverse ? G x); -rewrite > (associative ? (is_semi_group ? ( G))); -rewrite > (associative ? (is_semi_group ? ( G))); +rewrite > (op_associative ? G); +rewrite > (op_associative ? G); apply eq_f; assumption. qed. @@ -90,16 +72,16 @@ unfold right_cancellable; unfold injective; simplify;fold simplify (op G); intros (x y z); -rewrite < (e_is_right_unit ? ( G)); -rewrite < (e_is_right_unit ? ( G) z); +rewrite < (e_is_right_unit ? G); +rewrite < (e_is_right_unit ? G z); rewrite < (inv_is_right_inverse ? G x); -rewrite < (associative ? (is_semi_group ? ( G))); -rewrite < (associative ? (is_semi_group ? ( G))); +rewrite < (op_associative ? G); +rewrite < (op_associative ? G); rewrite > H; reflexivity. qed. -theorem inv_inv: ∀G:Group. ∀x:G. x \sup -1 \sup -1 = x. +theorem eq_inv_inv_x_x: ∀G:Group. ∀x:G. x \sup -1 \sup -1 = x. intros; apply (eq_op_x_y_op_z_y_to_eq ? (x \sup -1)); rewrite > (inv_is_right_inverse ? G); @@ -128,7 +110,7 @@ theorem eq_opxy_z_to_eq_x_opzinvy: ∀G:Group. ∀x,y,z:G. x·y=z → x = z·y \sup -1. intros; apply (eq_op_x_y_op_z_y_to_eq ? y); -rewrite > (associative ? G); +rewrite > (op_associative ? G); rewrite > (inv_is_left_inverse ? G); rewrite > (e_is_right_unit ? G); assumption. @@ -138,9 +120,9 @@ theorem eq_opxy_z_to_eq_y_opinvxz: ∀G:Group. ∀x,y,z:G. x·y=z → y = x \sup -1·z. intros; apply (eq_op_x_y_op_x_z_to_eq ? x); -rewrite < (associative ? G); +rewrite < (op_associative ? G); rewrite > (inv_is_right_inverse ? G); -rewrite > (e_is_left_unit ? (is_monoid ? G)); +rewrite > (e_is_left_unit ? G); assumption. qed. @@ -149,8 +131,8 @@ theorem eq_inv_op_x_y_op_inv_y_inv_x: intros; apply (eq_op_x_y_op_z_y_to_eq ? (x·y)); rewrite > (inv_is_left_inverse ? G); -rewrite < (associative ? G); -rewrite > (associative ? G (y \sup -1)); +rewrite < (op_associative ? G); +rewrite > (op_associative ? G (y \sup -1)); rewrite > (inv_is_left_inverse ? G); rewrite > (e_is_right_unit ? G); rewrite > (inv_is_left_inverse ? G); @@ -173,9 +155,9 @@ interpretation "Morphism image" 'morimage 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 ? G' ?); -rewrite < (f_morph ? ? f); +apply (eq_op_x_y_op_z_y_to_eq ? (f˜1)); +rewrite > (e_is_left_unit ? G'); +rewrite < f_morph; rewrite > (e_is_left_unit ? G); reflexivity. qed. @@ -184,9 +166,9 @@ 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)); +apply (eq_op_x_y_op_z_y_to_eq ? (f˜x)); rewrite > (inv_is_left_inverse ? G'); -rewrite < (f_morph ? ? f); +rewrite < f_morph; rewrite > (inv_is_left_inverse ? G); apply (morphism_to_eq_f_1_1 ? ? f). qed. @@ -199,16 +181,16 @@ record monomorphism (G,G':Group) : Type ≝ (* Subgroups *) record subgroup (G:Group) : Type ≝ - { group: Group; + { group:> Group; embed:> monomorphism group G }. - + notation "hvbox(x \sub H)" with precedence 79 for @{ 'subgroupimage $H $x }. interpretation "Subgroup image" 'subgroupimage H x = (cic:/matita/algebra/groups/image.con _ _ - (cic:/matita/algebra/groups/morphism_of_subgroup.con _ H) x). + (cic:/matita/algebra/groups/morphism_OF_subgroup.con _ H) x). definition member_of_subgroup ≝ λG.λH:subgroup G.λx:G.∃y.x=y \sub H. @@ -216,8 +198,15 @@ definition member_of_subgroup ≝ notation "hvbox(x break ∈ H)" with precedence 79 for @{ 'member_of $x $H }. +notation "hvbox(x break ∉ H)" with precedence 79 +for @{ 'not_member_of $x $H }. + interpretation "Member of subgroup" 'member_of x H = (cic:/matita/algebra/groups/member_of_subgroup.con _ H x). + +interpretation "Not member of subgroup" 'not_member_of x H = + (cic:/matita/logic/connectives/Not.con + (cic:/matita/algebra/groups/member_of_subgroup.con _ H x)). (* Left cosets *) @@ -260,61 +249,78 @@ alias symbol "member_of" (instance 0) = "Member of subgroup". theorem member_of_subgroup_op_inv_x_y_to_left_coset_eq: ∀G.∀x,y.∀H:subgroup G. (x \sup -1 ·y) ∈ H → x*H = y*H. intros; -unfold left_coset_eq; -simplify in ⊢ (? → ? ? ? (? ? % ?)); -simplify in ⊢ (? → ? ? ? (? ? ? (? ? ? (? ? %) ?))); -simplify in ⊢ (? % → ?); -intros; -unfold member_of_left_coset; -simplify in ⊢ (? ? (λy:?.? ? ? (? ? ? (? ? ? (? ? %) ?)))); -simplify in ⊢ (? ? (λy:? %.?)); -simplify in ⊢ (? ? (λy:?.? ? ? (? ? % ?))); +simplify; +intro; unfold member_of_subgroup in H1; elim H1; clear H1; exists; [ apply (a\sup-1 · x1) -| rewrite > (f_morph ? ? (morphism ? ? H)); - rewrite > (eq_image_inv_inv_image ? ? +| rewrite > f_morph; + rewrite > eq_image_inv_inv_image; rewrite < H2; - rewrite > (eq_inv_op_x_y_op_inv_y_inv_x ? ? ? ? H2); + rewrite > eq_inv_op_x_y_op_inv_y_inv_x; + rewrite > eq_inv_inv_x_x; + rewrite < (op_associative ? G); + rewrite < (op_associative ? G); + rewrite > (inv_is_right_inverse ? G); + rewrite > (e_is_left_unit ? G); + reflexivity ]. qed. -(*theorem foo: - \forall G:Group. \forall x1,x2:G. \forall H:subgroup G. - x1*x2^-1 \nin H \to x1*H does_not_overlap x2*H - -theorem foo: - \forall x:G. \forall H:subgroup G. x \in x*H - -definition disjoinct - (T: Type) (n:nat) (S: \forall x:nat. x < n -> {S:Type * (S -> T)}) -:= - \forall i,j:nat. i < n \to j < n \to ... +theorem Not_member_of_subgroup_to_left_coset_disjoint: + ∀G.∀x,y.∀H:subgroup G.(x \sup -1 ·y) ∉ H → x*H ∥ y*H. +intros; +simplify; +unfold Not; +intros (x'); +apply H1; +unfold member_of_subgroup; +elim H2; +apply (ex_intro ? ? (x'·a \sup -1)); +rewrite > f_morph; +apply (eq_op_x_y_op_z_y_to_eq ? (a \sub H)); +rewrite > (op_associative ? G); +rewrite < H3; +rewrite > (op_associative ? G); +rewrite < f_morph; +rewrite > (inv_is_left_inverse ? H); +rewrite < (op_associative ? G); +rewrite > (inv_is_left_inverse ? G); +rewrite > (e_is_left_unit ? G); +rewrite < (f_morph ? ? H); +rewrite > (e_is_right_unit ? H); +reflexivity. +qed. +(*CSC: here the coercion Type_of_Group cannot be omitted. Why? *) +theorem in_x_mk_left_coset_x_H: + ∀G.∀x:Type_OF_Group G.∀H:subgroup G.x ∈ (x*H). +intros; +simplify; +apply (ex_intro ? ? 1); +rewrite > morphism_to_eq_f_1_1; +rewrite > (e_is_right_unit ? G); +reflexivity. +qed. -check - (λG.λH,H':left_coset G.λx:Type_of_Group (group ? (subgrp ? H)). (embed ? (subgrp ? H) x)). +(* Normal Subgroups *) -definition left_coset_eq ≝ - λG.λH,H':left_coset G. - ∀x:group ? (subgrp ? H). - ex (group ? (subgroup ? H')) (λy. - (element ? H)·(embed ? (subgrp ? H) x) = - (element ? H')·(embed ? (subgrp ? H') y)). - -(*record left_coset (G:Group) : Type ≝ - { subgroup: Group; - subgroup_is_subgroup: subgroup ≤ G; - element: G +record normal_subgroup (G:Group) : Type ≝ + { ns_subgroup:> subgroup G; + normal:> ∀x:G.∀y:ns_subgroup.(x·y \sub ns_subgroup·x \sup -1) ∈ ns_subgroup }. -definition left_coset_eq ≝ - λG.λH,H':left_coset G. - ∀x:subgroup ? H. - ex (subgroup ? H') (λy. - (element ? H)·(embed ? ? (subgroup_is_subgroup ? H) ˜ x) = - (element ? H')·(embed ? ? (subgroup_is_subgroup ? H') ˜ y)). +(*CSC: I have not defined yet right cosets +theorem foo: + ∀G.∀H:normal_subgroup G.∀x.x*H=H*x. *) +(* +theorem member_of_left_coset_mk_left_coset_x_H_a_to_member_of_left_coset_mk_left_coset_y_H_b_to_member_of_left_coset_mk_left_coset_op_x_y_H_op_a_b: + ∀G.∀H:normal_subgroup G.∀x,y,a,b. + a ∈ (x*H) → b ∈ (y*H) → (a·b) ∈ ((x·y)*H). +intros; +simplify; +qed. *)