when more than one structure is in use at once).
2. The first definitions and theorems over groups.
set "baseuri" "cic:/matita/algebra/groups/".
+include "algebra/monoids.ma".
+
+record isGroup (M:Monoid) (opp: M -> M) : Prop ≝
+ { opp_is_left_inverse: is_left_inverse M opp;
+ opp_is_right_inverse: is_right_inverse M opp
+ }.
+
+record Group : Type ≝
+ { monoid: Monoid;
+ opp: monoid -> monoid;
+ group_properties: isGroup ? opp
+ }.
+
+coercion cic:/matita/algebra/groups/monoid.con.
+
+notation "hvbox(x \sup (-1))" with precedence 89
+for @{ 'gopp $x }.
+
+interpretation "Group inverse" 'gopp x =
+ (cic:/matita/algebra/groups/opp.con _ x).
+
+definition left_cancellable :=
+ \lambda T:Type. \lambda op: T -> T -> T.
+ \forall x,y,z. op x y = op x z -> y = z.
+
+definition right_cancellable :=
+ \lambda T:Type. \lambda op: T -> T -> T.
+ \forall x,y,z. op y x = op z x -> y = z.
+
+theorem eq_op_x_y_op_x_z_to_eq:
+ \forall G:Group. left_cancellable G (op G).
+intros;
+unfold left_cancellable;
+intros;
+rewrite < (e_is_left_unit ? ? (monoid_properties G));
+fold simplify (e G);
+rewrite < (e_is_left_unit ? ? (monoid_properties G) z);
+fold simplify (e G);
+rewrite < (opp_is_left_inverse ? ? (group_properties G) x);
+fold simplify (opp G);
+rewrite > (semigroup_properties G);
+fold simplify (op G);
+rewrite > (semigroup_properties G);
+fold simplify (op G);
+apply eq_f;
+assumption.
+qed.
+
+(*
+theorem eq_op_x_y_op_z_y_to_eq:
+ \forall G:Group. right_cancellable G (op G).
+qed.
+
+definition has_cardinality :=
+ \lambda T:Type. \lambda n:nat.
+ \exists f. injective T nat f.
+
+definition finite :=
+ \lambda T:Type.
+ \exists f: T -> {n|n<
+*)
record Monoid : Type ≝
{ semigroup: SemiGroup;
e: semigroup;
- properties: isMonoid ? e
+ monoid_properties: isMonoid ? e
}.
coercion cic:/matita/algebra/monoids/semigroup.con.
-notation "hvbox(! \sub S)"
+(* too ugly
+notation "hvbox(1 \sub S)" with precedence 89
for @{ 'munit $S }.
interpretation "Monoid unit" 'munit S =
- (cic:/matita/algebra/monoids/e.con S).
-
+ (cic:/matita/algebra/monoids/e.con S). *)
+
+notation "1" with precedence 89
+for @{ 'munit }.
+
+interpretation "Monoid unit" 'munit =
+ (cic:/matita/algebra/monoids/e.con _).
+
notation < "M"
for @{ 'semigroup $M }.
definition is_left_inverse ≝
λM:Monoid.
λopp: M → M.
- ∀x:M. op M (opp x) x = ! \sub M.
-
+ ∀x:M. op M (opp x) x = 1.
+
definition is_right_inverse ≝
λM:Monoid.
λopp: M → M.
- ∀x:M. op M x (opp x) = ! \sub M.
+ ∀x:M. op M x (opp x) = 1.
theorem is_left_inverse_to_is_right_inverse_to_eq:
- ∀M:Monoid. ∀oppL,oppR.
- is_left_inverse M oppL → is_right_inverse M oppR →
- ∀x:M. oppL x = oppR x.
+ ∀M:Monoid. ∀l,r.
+ is_left_inverse M l → is_right_inverse M r →
+ ∀x:M. l x = r x.
intros;
generalize in match (H x); intro;
- generalize in match (eq_f ? ? (λy. op M y (oppR x)) ? ? H2);
+ generalize in match (eq_f ? ? (λy. op M y (r x)) ? ? H2);
simplify; fold simplify (op M);
intro; clear H2;
- generalize in match (properties (semigroup M));
+ generalize in match (semigroup_properties M);
fold simplify (Type_of_Monoid M);
intro;
unfold isSemiGroup in H2; unfold associative in H2;
rewrite > H2 in H3; clear H2;
rewrite > H1 in H3;
- rewrite > (e_is_left_unit ? ? (properties M)) in H3;
- rewrite > (e_is_right_unit ? ? (properties M)) in H3;
+ rewrite > (e_is_left_unit ? ? (monoid_properties M)) in H3;
+ rewrite > (e_is_right_unit ? ? (monoid_properties M)) in H3;
assumption.
qed.
-
record SemiGroup : Type ≝
{ carrier: Type;
op: carrier → carrier → carrier;
- properties: isSemiGroup carrier op
+ semigroup_properties: isSemiGroup carrier op
}.
coercion cic:/matita/algebra/semigroups/carrier.con.
-notation "hvbox(a break * \sub S b)"
+notation "hvbox(a break \middot \sub S b)"
left associative with precedence 55
for @{ 'ptimes $S $a $b }.
-interpretation "Semigroup operation" 'times a b =
+notation "hvbox(a break \middot b)"
+ left associative with precedence 55
+for @{ 'ptimesi $a $b }.
+
+interpretation "Semigroup operation" 'ptimesi a b =
(cic:/matita/algebra/semigroups/op.con _ a b).
+(* too ugly
interpretation "Semigroup operation" 'ptimes S a b =
- (cic:/matita/algebra/semigroups/op.con S a b).
+ (cic:/matita/algebra/semigroups/op.con S a b). *)
definition is_left_unit ≝
- λS:SemiGroup. λe:S. ∀x:S. e * x = x.
+ λS:SemiGroup. λe:S. ∀x:S. e·x = x.
definition is_right_unit ≝
- λS:SemiGroup. λe:S. ∀x:S. x * e = x.
+ λS:SemiGroup. λe:S. ∀x:S. x·e = x.
theorem is_left_unit_to_is_right_unit_to_eq:
- ∀S:SemiGroup. ∀e1,e2:S.
- is_left_unit ? e1 → is_right_unit ? e2 → e1=e2.
+ ∀S:SemiGroup. ∀e,e':S.
+ is_left_unit ? e → is_right_unit ? e' → e=e'.
intros;
- rewrite < (H e2);
- rewrite < (H1 e1) in \vdash (? ? % ?);
+ rewrite < (H e');
+ rewrite < (H1 e) in \vdash (? ? % ?);
reflexivity.
-qed.
\ No newline at end of file
+qed.