helm/matita/library/algebra/groups.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 set "baseuri" "cic:/matita/algebra/groups/".
  16
  17 include "algebra/monoids.ma".
  18
  19 record isGroup (M:Monoid) (opp: M -> M) : Prop ≝
  20  { opp_is_left_inverse: is_left_inverse M opp;
  21    opp_is_right_inverse: is_right_inverse M opp
  22  }.
  23
  24 record Group : Type ≝
  25  { monoid: Monoid;
  26    opp: monoid -> monoid;
  27    group_properties: isGroup ? opp
  28  }.
  29
  30 coercion cic:/matita/algebra/groups/monoid.con.
  31
  32 notation "hvbox(x \sup (-1))" with precedence 89
  33 for @{ 'gopp $x }.
  34
  35 interpretation "Group inverse" 'gopp x =
  36  (cic:/matita/algebra/groups/opp.con _ x).
  37
  38 definition left_cancellable :=
  39  \lambda T:Type. \lambda op: T -> T -> T.
  40   \forall x,y,z. op x y = op x z -> y = z.
  41
  42 definition right_cancellable :=
  43  \lambda T:Type. \lambda op: T -> T -> T.
  44   \forall x,y,z. op y x = op z x -> y = z.
  45
  46 theorem eq_op_x_y_op_x_z_to_eq:
  47  \forall G:Group. left_cancellable G (op G).
  48 intros;
  49 unfold left_cancellable;
  50 intros;
  51 rewrite < (e_is_left_unit ? ? (monoid_properties G));
  52 rewrite < (e_is_left_unit ? ? (monoid_properties G) z);
  53 rewrite < (opp_is_left_inverse ? ? (group_properties G) x);
  54 rewrite > (semigroup_properties G);
  55 rewrite > (semigroup_properties G);
  56 apply eq_f;
  57 assumption.
  58 qed.
  59
  60 (*
  61 theorem eq_op_x_y_op_z_y_to_eq:
  62  \forall G:Group. right_cancellable G (op G).
  63 qed.
  64
  65 definition has_cardinality :=
  66  \lambda T:Type. \lambda n:nat.
  67   \exists f. injective T nat f.
  68
  69 definition finite :=
  70  \lambda T:Type.
  71   \exists f: T -> {n|n<
  72 *)