The abstract of the Mizar article:

Categories of Groups

by

Michal Muzalewski

Received October 3, 1991

MML identifier: GRCAT_1

[ Mizar article, MML identifier index ]

environ

 vocabulary CLASSES2, PARTFUN1, RELAT_1, FUNCT_1, MIDSP_1, BOOLE, VECTSP_2,
      FUNCT_2, VECTSP_1, MIDSP_2, RLVECT_1, ARYTM_1, CAT_1, TARSKI, CAT_2,
      PRE_TOPC, ORDINAL4, FUNCOP_1, MOD_1, ENS_1, GRCAT_1, ALGSTR_1;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, MOD_1, RELAT_1, FUNCT_1,
      MCART_1, STRUCT_0, BINOP_1, RLVECT_1, VECTSP_1, VECTSP_2, PARTFUN1,
      CAT_1, CLASSES2, PRE_TOPC, FUNCT_2, CAT_2, ALGSTR_1, MIDSP_1, MIDSP_2;
 constructors BINOP_1, VECTSP_2, CLASSES2, CAT_2, MIDSP_2, TOPS_2, ALGSTR_1,
      CLASSES1, MEMBERED, PARTFUN1, RELAT_2, XBOOLE_0;
 clusters RELSET_1, GROUP_1, STRUCT_0, SUBSET_1, CLASSES2, ALGSTR_1, MIDSP_2,
      MEMBERED, ZFMISC_1, FUNCT_2, PARTFUN1, XBOOLE_0;
 requirements SUBSET, BOOLE;


begin ::  0a. Auxiliary theorems: sets and universums

reserve x, y for set;
reserve D for non empty set;
reserve UN for Universe;

canceled;

theorem :: GRCAT_1:2
 for X,Y,A being set, z being set st z in A & A c= [:X,Y:]
      ex x being Element of X, y being Element of Y st z = [x,y];

theorem :: GRCAT_1:3
 for u1,u2,u3,u4 being Element of UN holds
 [u1,u2,u3] is Element of UN & [u1,u2,u3,u4] is Element of UN;

theorem :: GRCAT_1:4
 for x,y st x in y & y in UN holds x in UN;

::  0b. Auxiliary schemes: partial functions

scheme PartLambda2{X,Y,Z()->set,F(set,set)->set,P[set,set]}:
 ex f being PartFunc of [:X(),Y():],Z()
  st (for x,y holds [x,y] in dom f iff x in X() & y in Y() & P[x,y])
   & (for x,y st [x,y] in dom f holds f.[x,y] = F(x,y))
provided
 for x,y st x in X() & y in Y() & P[x,y] holds F(x,y) in Z();

scheme PartLambda2D{X,Y()->non empty set,Z()->set,F(set,set)->set,
 P[set,set]}: ex f being PartFunc of [:X(),Y():],Z()
  st (for x being Element of X(), y being Element of Y() holds
       [x,y] in dom f iff P[x,y])
   & (for x being Element of X(), y being Element of Y() st [x,y] in
 dom f holds f.[x,y] = F(x,y))
provided
 for x being Element of X(), y being Element of Y() st P[x,y] holds
     F(x,y) in Z();

::  0c. Auxiliary theorems: Trivial Group

theorem :: GRCAT_1:5
 op2.({},{}) = {} & op1.{} = {} & op0 = {};

theorem :: GRCAT_1:6
 {{}} in UN & [{{}},{{}}] in UN & [:{{}},{{}}:] in UN &
  op2 in UN & op1 in UN;

theorem :: GRCAT_1:7
 LoopStr (# {{}},op2,Extract {} #) is midpoint_operator;

definition
 cluster L_Trivial -> midpoint_operator;
end;

theorem :: GRCAT_1:8
     (for x being Element of L_Trivial holds x = {})
  & (for x,y being Element of L_Trivial holds x+y = {})
  & (for x being Element of L_Trivial holds -x = {})
  & 0.L_Trivial = {};

::  0d. Auxiliary theorems: subcategories

reserve C for Category;
reserve O for non empty Subset of the Objects of C;

definition let C,O;
 canceled 4;

 func Morphs(O) -> Subset of the Morphisms of C equals
:: GRCAT_1:def 5
  union{Hom(a,b) where a is Object of C,b is Object of C : a in O & b in O};
end;

definition let C,O;
 cluster Morphs(O) -> non empty;
end;

definition let C,O;
 func dom(O) -> Function of Morphs(O),O equals
:: GRCAT_1:def 6
   (the Dom of C)|Morphs(O);
 func cod(O) -> Function of Morphs(O),O equals
:: GRCAT_1:def 7
   (the Cod of C)|Morphs(O);
 func comp(O) -> PartFunc of [:Morphs(O),(Morphs(O)):],Morphs(O) equals
:: GRCAT_1:def 8
   (the Comp of C)|([:Morphs(O),Morphs(O):] qua set);
 func ID(O) -> Function of O,Morphs(O) equals
:: GRCAT_1:def 9
   (the Id of C)|O;
end;

theorem :: GRCAT_1:9
 CatStr (# O,Morphs(O),dom(O),cod(O),comp(O),ID(O)#)
  is_full_subcategory_of C;

definition let C,O;
 func cat(O) -> Subcategory of C equals
:: GRCAT_1:def 10
   CatStr (# O,Morphs(O),dom(O),cod(O),comp(O),ID(O)#);
end;

definition let C,O;
 cluster cat(O) -> strict;
end;

theorem :: GRCAT_1:10
 the Objects of cat(O) = O;

::  1a. Maps of the carriers of groups

definition let G be 1-sorted;
 func id G -> map of G,G equals
:: GRCAT_1:def 11
   id the carrier of G;
end;

theorem :: GRCAT_1:11
 for G being non empty 1-sorted,
     x being Element of G holds (id G).x = x;

theorem :: GRCAT_1:12
 for G being 1-sorted, H being non empty 1-sorted,
     f being map of G, H holds f*(id G) = f & (id H)*f = f;

definition let G,H be non empty ZeroStr;
 func ZeroMap(G,H) -> map of G,H equals
:: GRCAT_1:def 12
   (the carrier of G) --> 0.H;
end;

definition let G,H be non empty LoopStr; let f be map of G,H;
 attr f is additive means
:: GRCAT_1:def 13
  for x,y being Element of G holds f.(x+y) = f.x+f.y;
end;

theorem :: GRCAT_1:13
  comp L_Trivial = op1;

theorem :: GRCAT_1:14
 for G1,G2,G3 being non empty LoopStr,
   f being map of G1,G2, g being map of G2,G3
      st f is additive & g is additive holds g*f is additive;

theorem :: GRCAT_1:15
  for G being non empty ZeroStr,
      H being non empty LoopStr,
      x being Element of G holds ZeroMap(G,H).x = 0.H;

theorem :: GRCAT_1:16
  for G being non empty LoopStr,
      H being right_zeroed (non empty LoopStr) holds ZeroMap(G,H) is additive;

::  1b. Morphisms of groups

reserve G,H for AddGroup;

definition
  struct GroupMorphismStr (# Dom,Cod -> AddGroup,
                          Fun -> map of the Dom, the Cod #);
end;

definition let f be GroupMorphismStr;
 func dom(f) -> AddGroup equals
:: GRCAT_1:def 14
   the Dom of f;
 func cod(f) -> AddGroup equals
:: GRCAT_1:def 15
   the Cod of f;
end;

definition let f be GroupMorphismStr;
 func fun(f) -> map of dom(f),cod(f) equals
:: GRCAT_1:def 16
   the Fun of f;
end;

theorem :: GRCAT_1:17
  for f being GroupMorphismStr,
          G1,G2 being AddGroup,
          f0 being map of G1,G2 st f = GroupMorphismStr(# G1,G2,f0#)
      holds dom f = G1 & cod f = G2 & fun f = f0;

definition let G,H;
 func ZERO(G,H) -> GroupMorphismStr equals
:: GRCAT_1:def 17
   GroupMorphismStr(# G,H,ZeroMap(G,H)#);
end;

definition let G,H;
 cluster ZERO(G,H) -> strict;
end;

definition let IT be GroupMorphismStr;
 attr IT is GroupMorphism-like means
:: GRCAT_1:def 18
  fun(IT) is additive;
end;

definition
 cluster strict GroupMorphism-like GroupMorphismStr;
end;

definition
 mode GroupMorphism is GroupMorphism-like GroupMorphismStr;
end;

theorem :: GRCAT_1:18
 for F being GroupMorphism holds the Fun of F is additive;

definition let G,H;
 cluster ZERO(G,H) -> GroupMorphism-like;
end;

definition let G,H;
 mode Morphism of G,H -> GroupMorphism means
:: GRCAT_1:def 19
  dom(it) = G & cod(it) = H;
end;

definition let G,H;
 cluster strict Morphism of G,H;
end;

theorem :: GRCAT_1:19
 for f being strict GroupMorphismStr
   st dom(f) = G & cod(f) = H & fun(f) is additive
   holds f is strict Morphism of G,H;

theorem :: GRCAT_1:20
 for f being map of G,H st f is additive
       holds GroupMorphismStr (# G,H,f#) is strict Morphism of G,H;

theorem :: GRCAT_1:21
  for G being non empty LoopStr holds id G is additive;

definition let G;
 func ID G -> Morphism of G,G equals
:: GRCAT_1:def 20
   GroupMorphismStr(# G,G,id G#);
end;

definition let G;
 cluster ID G -> strict;
end;

definition let G,H;
 redefine func ZERO(G,H) -> strict Morphism of G,H;
end;

theorem :: GRCAT_1:22
 for F being Morphism of G,H ex f being map of G,H
       st the GroupMorphismStr of F = GroupMorphismStr(# G,H,f#) &
        f is additive;

theorem :: GRCAT_1:23
 for F being strict Morphism of G,H ex f being map of G,H
       st F = GroupMorphismStr(# G,H,f#);

theorem :: GRCAT_1:24
 for F being GroupMorphism ex G,H st F is Morphism of G,H;

theorem :: GRCAT_1:25
  for F being strict GroupMorphism ex G,H being AddGroup, f being map of G,H
       st F is Morphism of G,H
        & F = GroupMorphismStr(# G,H,f#)
        & f is additive;

theorem :: GRCAT_1:26
 for g,f being GroupMorphism st dom(g) = cod(f)
       ex G1,G2,G3 being AddGroup st g is Morphism of G2,G3
                                   & f is Morphism of G1,G2;

definition let G,F be GroupMorphism;
 assume  dom(G) = cod(F);
 func G*F -> strict GroupMorphism means
:: GRCAT_1:def 21
  for G1,G2,G3 being AddGroup,
           g being map of G2,G3, f being map of G1,G2
       st the GroupMorphismStr of G = GroupMorphismStr(# G2,G3,g#) &
          the GroupMorphismStr of F = GroupMorphismStr(# G1,G2,f#)
       holds it = GroupMorphismStr(# G1,G3,g*f#);
end;

canceled;

theorem :: GRCAT_1:28
 for G1,G2,G3 being AddGroup,
          G being Morphism of G2,G3,
          F being Morphism of G1,G2
      holds G*F is Morphism of G1,G3;

definition let G1,G2,G3 be AddGroup,
               G be Morphism of G2,G3,
               F be Morphism of G1,G2;
 redefine func G*F -> strict Morphism of G1,G3;
end;

theorem :: GRCAT_1:29
 for G1,G2,G3 being AddGroup,
          G being Morphism of G2,G3,
          F being Morphism of G1,G2,
          g being map of G2,G3, f being map of G1,G2
      st G = GroupMorphismStr(# G2,G3,g#) & F = GroupMorphismStr(# G1,G2,f#)
      holds G*F = GroupMorphismStr(# G1,G3,g*f#);

 theorem :: GRCAT_1:30
  for f,g being strict GroupMorphism st dom g = cod f holds
       ex G1,G2,G3 being AddGroup,
          f0 being map of G1,G2, g0 being map of G2,G3
          st f = GroupMorphismStr(# G1,G2,f0#)
           & g = GroupMorphismStr(# G2,G3,g0#)
           & g*f = GroupMorphismStr(# G1,G3,g0*f0#);

 theorem :: GRCAT_1:31
  for f,g being strict GroupMorphism st dom g = cod f holds
     dom(g*f) = dom f & cod (g*f) = cod g;

 theorem :: GRCAT_1:32
  for G1,G2,G3,G4 being AddGroup, f being strict Morphism of G1,G2,
             g being strict Morphism of G2,G3,
             h being strict Morphism of G3,G4
         holds h*(g*f) = (h*g)*f;

 theorem :: GRCAT_1:33
  for f,g,h being strict GroupMorphism
        st dom h = cod g & dom g = cod f holds h*(g*f) = (h*g)*f;

 theorem :: GRCAT_1:34
  dom ID(G) = G
      & cod ID(G) = G
      & (for f being strict GroupMorphism st cod f = G holds (ID G)*f = f)
      & (for g being strict GroupMorphism st dom g = G holds g*(ID G) = g);

::  2. Domains of groups

definition let IT be set;
 attr IT is Group_DOMAIN-like means
:: GRCAT_1:def 22
  for x being set st x in IT holds x is strict AddGroup;
end;

definition
 cluster Group_DOMAIN-like non empty set;
end;

definition
 mode Group_DOMAIN is Group_DOMAIN-like non empty set;
end;

reserve V for Group_DOMAIN;

definition let V;
 redefine mode Element of V -> AddGroup;
end;

definition let V;
 cluster strict Element of V;
end;

::  3. Domains of morphisms

definition let IT be set;
 attr IT is GroupMorphism_DOMAIN-like means
:: GRCAT_1:def 23
   for x being set st x in IT holds x is strict GroupMorphism;
end;

definition
 cluster GroupMorphism_DOMAIN-like non empty set;
end;

definition
 mode GroupMorphism_DOMAIN is GroupMorphism_DOMAIN-like non empty set;
end;

definition let M be GroupMorphism_DOMAIN;
 redefine mode Element of M -> GroupMorphism;
end;

definition let M be GroupMorphism_DOMAIN;
 cluster strict Element of M;
end;

canceled 2;

theorem :: GRCAT_1:37
 for f being strict GroupMorphism holds {f} is GroupMorphism_DOMAIN;

definition let G,H;
 mode GroupMorphism_DOMAIN of G,H -> GroupMorphism_DOMAIN means
:: GRCAT_1:def 24
  for x being Element of it holds x is strict Morphism of G,H;
end;

theorem :: GRCAT_1:38
 D is GroupMorphism_DOMAIN of G,H
       iff for x being Element of D holds x is strict Morphism of G,H;

theorem :: GRCAT_1:39
  for f being strict Morphism of G,H holds {f} is GroupMorphism_DOMAIN of G,H;

definition let G,H be 1-sorted;
 mode MapsSet of G,H means
:: GRCAT_1:def 25
 for x being set st x in it holds x is map of G,H;
end;

definition let G,H be 1-sorted;
 func Maps(G,H) -> MapsSet of G,H equals
:: GRCAT_1:def 26
  Funcs(the carrier of G, the carrier of H);
end;

definition let G be 1-sorted, H be non empty 1-sorted;
 cluster Maps(G,H) -> non empty;
end;

definition let G be 1-sorted, H be non empty 1-sorted;
 cluster non empty MapsSet of G,H;
end;

definition let G be 1-sorted, H be non empty 1-sorted;
           let M be non empty MapsSet of G,H;
 redefine mode Element of M -> map of G,H;
end;

definition let G,H;
 func Morphs(G,H) -> GroupMorphism_DOMAIN of G,H means
:: GRCAT_1:def 27
  x in it iff x is strict Morphism of G,H;
end;

definition let G,H; let M be GroupMorphism_DOMAIN of G,H;
 redefine mode Element of M -> Morphism of G,H;
end;

definition let G,H; let M be GroupMorphism_DOMAIN of G,H;
 cluster strict Element of M;
end;

::  4a. Category of groups - objects

definition let x,y;
 pred GO x,y means
:: GRCAT_1:def 28
  ex x1,x2,x3,x4 being set st x = [x1,x2,x3,x4] &
    ex G being strict AddGroup
    st y = G
    & x1 = the carrier of G
    & x2 = the add of G
    & x3 = comp G
    & x4 = the Zero of G;
end;

theorem :: GRCAT_1:40
 for x,y1,y2 being set st GO x,y1 & GO x,y2 holds y1 = y2;

theorem :: GRCAT_1:41
 ex x st x in UN & GO x,L_Trivial;

definition let UN;
 func GroupObjects(UN) -> set means
:: GRCAT_1:def 29
  for y holds y in it iff ex x st x in UN & GO x,y;
end;

theorem :: GRCAT_1:42
 L_Trivial in GroupObjects(UN);

definition let UN;
 cluster GroupObjects(UN) -> non empty;
end;

theorem :: GRCAT_1:43
 for x being Element of GroupObjects(UN) holds x is strict AddGroup;

definition let UN;
  cluster GroupObjects(UN) -> Group_DOMAIN-like;
end;

::  4b. Category of groups - morphisms

definition let V;
 func Morphs(V) -> GroupMorphism_DOMAIN means
:: GRCAT_1:def 30
  for x holds x in it iff ex G,H being strict Element of V
  st x is strict Morphism of G,H;
end;

      ::
      ::  4c. Category of groups - dom,cod,id
      ::

definition let V; let F be Element of Morphs(V);
redefine func dom(F) -> strict Element of V;
 func cod(F) -> strict Element of V;
end;

definition let V; let G be Element of V;
 func ID(G) -> strict Element of Morphs(V) equals
:: GRCAT_1:def 31
   ID(G);
end;

definition let V;
 func dom(V) -> Function of Morphs(V),V means
:: GRCAT_1:def 32
  for f being Element of Morphs(V) holds it.f = dom(f);
 func cod(V) -> Function of Morphs(V),V means
:: GRCAT_1:def 33
  for f being Element of Morphs(V) holds it.f = cod(f);
 func ID(V) -> Function of V,Morphs(V) means
:: GRCAT_1:def 34
  for G being Element of V holds it.G = ID(G);
 end;

      ::
      ::  4d. Category of groups - superposition
      ::

theorem :: GRCAT_1:44
 for g,f being Element of Morphs(V) st dom(g) = cod(f)
      ex G1,G2,G3 being strict Element of V st g is Morphism of G2,G3
                                      & f is Morphism of G1,G2;

theorem :: GRCAT_1:45
 for g,f being Element of Morphs(V) st dom(g) = cod(f)
      holds g*f in Morphs(V);

definition let V;
 func comp(V) -> PartFunc of [:Morphs(V),Morphs(V):],Morphs(V) means
:: GRCAT_1:def 35

 (for g,f being Element of Morphs(V) holds [g,f] in dom it iff dom(g) = cod(f))
 & (for g,f being Element of Morphs(V) st [g,f] in dom it
    holds it.[g,f] = g*f);
end;

      ::
      ::  4e. Definition of Category of groups
      ::

definition let UN;
 func GroupCat(UN) -> CatStr equals
:: GRCAT_1:def 36
   CatStr(# GroupObjects(UN),Morphs(GroupObjects(UN)),
                   dom(GroupObjects(UN)),cod(GroupObjects(UN)),
                   comp(GroupObjects(UN)),ID(GroupObjects(UN))#);
end;

definition let UN;
 cluster GroupCat(UN) -> strict;
end;

theorem :: GRCAT_1:46
  for f,g being Morphism of GroupCat(UN) holds
        [g,f] in dom(the Comp of GroupCat(UN)) iff dom g = cod f;

theorem :: GRCAT_1:47
  for f  being (Morphism of GroupCat(UN)),
           f' being Element of Morphs(GroupObjects(UN)),
           b  being Object of GroupCat(UN),
           b' being Element of GroupObjects(UN)
       holds f is strict Element of Morphs(GroupObjects(UN))
           & f' is Morphism of GroupCat(UN)
           & b is strict Element of GroupObjects(UN)
           & b' is Object of GroupCat(UN);

theorem :: GRCAT_1:48
  for b  being Object of GroupCat(UN),
           b' being Element of GroupObjects(UN)
       st b = b' holds id b = ID(b');

 theorem :: GRCAT_1:49
  for f  being Morphism of GroupCat(UN)
       for f' being Element of Morphs(GroupObjects(UN))
       st f = f'
       holds dom f = dom f'
           & cod f = cod f';

 theorem :: GRCAT_1:50
  for f,g   being (Morphism of GroupCat(UN)),
           f',g' being Element of Morphs(GroupObjects(UN))
       st f = f' & g = g'
       holds (dom g = cod f iff dom g' = cod f')
           & (dom g = cod f iff [g',f'] in dom comp(GroupObjects(UN)))
           & (dom g = cod f implies g*f = g'*f')
           & (dom f = dom g iff dom f' = dom g')
           & (cod f = cod g iff cod f' = cod g');

definition let UN;
 cluster GroupCat(UN) -> Category-like;
end;

definition let UN;
 func AbGroupObjects(UN) -> Subset of the Objects of GroupCat(UN) equals
:: GRCAT_1:def 37
   {G where G is Element of the Objects of GroupCat(UN)
                 : ex H being AbGroup st G = H};
end;

theorem :: GRCAT_1:51
 L_Trivial in AbGroupObjects(UN);

definition let UN;
 cluster AbGroupObjects(UN) -> non empty;
end;

definition let UN;
 func AbGroupCat(UN) -> Subcategory of GroupCat(UN) equals
:: GRCAT_1:def 38
   cat(AbGroupObjects(UN));
end;

definition let UN;
 cluster AbGroupCat(UN) -> strict;
end;

theorem :: GRCAT_1:52
 the Objects of AbGroupCat(UN) = AbGroupObjects(UN);

::  6. Subcategory of groups with the operator of 1/2

definition let UN;
 func MidOpGroupObjects(UN) -> Subset of the Objects of AbGroupCat(UN) equals
:: GRCAT_1:def 39
   {G where G is Element of the Objects of AbGroupCat(UN)
                 : ex H being midpoint_operator AbGroup st G = H};
end;

definition let UN;
 cluster MidOpGroupObjects(UN) -> non empty;
end;

definition let UN;
 func MidOpGroupCat(UN) -> Subcategory of AbGroupCat(UN) equals
:: GRCAT_1:def 40
  cat(MidOpGroupObjects(UN));
end;

definition let UN;
 cluster MidOpGroupCat(UN) -> strict;
end;

theorem :: GRCAT_1:53
  the Objects of MidOpGroupCat(UN) = MidOpGroupObjects(UN);

theorem :: GRCAT_1:54
  L_Trivial in MidOpGroupObjects(UN);