1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/algebra/groups/".
17 include "algebra/monoids.ma".
18 include "nat/le_arith.ma".
20 record PreGroup : Type ≝
21 { premonoid:> PreMonoid;
22 opp: premonoid -> premonoid
25 record isGroup (G:PreGroup) : Prop ≝
26 { is_monoid: isMonoid G;
27 opp_is_left_inverse: is_left_inverse (mk_Monoid ? is_monoid) (opp G);
28 opp_is_right_inverse: is_right_inverse (mk_Monoid ? is_monoid) (opp G)
32 { pregroup:> PreGroup;
33 group_properties:> isGroup pregroup
39 interpretation "Monoid coercion" 'monoid G =
40 (cic:/matita/algebra/groups/monoid.con G).*)
43 for @{ 'type_of_group $G }.
45 interpretation "Type_of_group coercion" 'type_of_group G =
46 (cic:/matita/algebra/groups/Type_of_Group.con G).
49 for @{ 'magma_of_group $G }.
51 interpretation "magma_of_group coercion" 'magma_of_group G =
52 (cic:/matita/algebra/groups/Magma_of_Group.con G).
54 notation "hvbox(x \sup (-1))" with precedence 89
57 interpretation "Group inverse" 'gopp x =
58 (cic:/matita/algebra/groups/opp.con _ x).
60 definition left_cancellable ≝
61 λT:Type. λop: T -> T -> T.
62 ∀x. injective ? ? (op x).
64 definition right_cancellable ≝
65 λT:Type. λop: T -> T -> T.
66 ∀x. injective ? ? (λz.op z x).
68 theorem eq_op_x_y_op_x_z_to_eq:
69 ∀G:Group. left_cancellable G (op G).
71 unfold left_cancellable;
74 rewrite < (e_is_left_unit ? (is_monoid ? (group_properties G)));
75 rewrite < (e_is_left_unit ? (is_monoid ? (group_properties G)) z);
76 rewrite < (opp_is_left_inverse ? (group_properties G) x);
77 rewrite > (associative ? (is_semi_group ? (is_monoid ? (group_properties G))));
78 rewrite > (associative ? (is_semi_group ? (is_monoid ? (group_properties G))));
84 theorem eq_op_x_y_op_z_y_to_eq:
85 ∀G:Group. right_cancellable G (op G).
87 unfold right_cancellable;
89 simplify;fold simplify (op G);
91 rewrite < (e_is_right_unit ? (is_monoid ? (group_properties G)));
92 rewrite < (e_is_right_unit ? (is_monoid ? (group_properties G)) z);
93 rewrite < (opp_is_right_inverse ? (group_properties G) x);
94 rewrite < (associative ? (is_semi_group ? (is_monoid ? (group_properties G))));
95 rewrite < (associative ? (is_semi_group ? (is_monoid ? (group_properties G))));
101 record finite_enumerable (T:Type) : Type ≝
105 index_of_sur: ∀x.index_of x ≤ order;
106 index_of_repr: ∀n. n≤order → index_of (repr n) = n;
107 repr_index_of: ∀x. repr (index_of x) = x
110 notation "hvbox(C \sub i)" with precedence 89
111 for @{ 'repr $C $i }.
113 (* CSC: multiple interpretations in the same file are not considered in the
115 interpretation "Finite_enumerable representation" 'repr C i =
116 (cic:/matita/algebra/groups/repr.con C _ i).*)
118 notation "hvbox(|C|)" with precedence 89
121 interpretation "Finite_enumerable order" 'card C =
122 (cic:/matita/algebra/groups/order.con C _).
124 record finite_enumerable_SemiGroup : Type ≝
125 { semigroup:> SemiGroup;
126 is_finite_enumerable:> finite_enumerable semigroup
130 for @{ 'semigroup_of_finite_enumerable_semigroup $S }.
132 interpretation "Semigroup_of_finite_enumerable_semigroup"
133 'semigroup_of_finite_enumerable_semigroup S
135 (cic:/matita/algebra/groups/semigroup.con S).
138 for @{ 'magma_of_finite_enumerable_semigroup $S }.
140 interpretation "Magma_of_finite_enumerable_semigroup"
141 'magma_of_finite_enumerable_semigroup S
143 (cic:/matita/algebra/groups/Magma_of_finite_enumerable_SemiGroup.con S).
146 for @{ 'type_of_finite_enumerable_semigroup $S }.
148 interpretation "Type_of_finite_enumerable_semigroup"
149 'type_of_finite_enumerable_semigroup S
151 (cic:/matita/algebra/groups/Type_of_finite_enumerable_SemiGroup.con S).
153 interpretation "Finite_enumerable representation" 'repr S i =
154 (cic:/matita/algebra/groups/repr.con S
155 (cic:/matita/algebra/groups/is_finite_enumerable.con S) i).
157 notation "hvbox(ι e)" with precedence 60
158 for @{ 'index_of_finite_enumerable_semigroup $e }.
160 interpretation "Index_of_finite_enumerable representation"
161 'index_of_finite_enumerable_semigroup e
163 (cic:/matita/algebra/groups/index_of.con _
164 (cic:/matita/algebra/groups/is_finite_enumerable.con _) e).
167 ∀G:finite_enumerable_SemiGroup.
168 left_cancellable ? (op G) →
169 right_cancellable ? (op G) →
170 ∃e:G. isMonoid (mk_PreMonoid G e).
172 letin f ≝ (λn.ι(G \sub O · G \sub n));
173 cut (∀n.n ≤ order ? (is_finite_enumerable G) → ∃m.f m = n);
174 [ letin EX ≝ (Hcut O ?);
181 letin HH ≝ (eq_f ? ? (repr ? (is_finite_enumerable G)) ? ? H2);
183 rewrite > (repr_index_of ? (is_finite_enumerable G)) in HH;
184 apply (ex_intro ? ? (G \sub a));
185 letin GOGO ≝ (refl_eq ? (repr ? (is_finite_enumerable G) O));
187 rewrite < HH in GOGO;
188 rewrite < HH in GOGO:(? ? % ?);
189 rewrite > (associative ? G) in GOGO;
190 letin GaGa ≝ (H ? ? ? GOGO);
195 apply (semigroup_properties G)
196 | unfold is_left_unit; intro;
197 letin GaxGax ≝ (refl_eq ? (G \sub a ·x));
199 rewrite < GaGa in GaxGax:(? ? % ?);
200 rewrite > (associative ? (semigroup_properties G)) in GaxGax;
201 apply (H ? ? ? GaxGax)
202 | unfold is_right_unit; intro;
203 letin GaxGax ≝ (refl_eq ? (x·G \sub a));
205 rewrite < GaGa in GaxGax:(? ? % ?);
206 rewrite < (associative ? (semigroup_properties G)) in GaxGax;
207 apply (H1 ? ? ? GaxGax)