The Mizar article:

Categories of Groups

by
Michal Muzalewski

Received October 3, 1991

Copyright (c) 1991 Association of Mizar Users

MML identifier: GRCAT_1
[ 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;
 theorems BINOP_1, CAT_1, CAT_2, CLASSES2, FUNCOP_1, FUNCT_1, FUNCT_2, MIDSP_2,
      MCART_1, PARTFUN1, VECTSP_1, TARSKI, ZFMISC_1, RLVECT_1, RELAT_1,
      RELSET_1, ORDINAL1, XBOOLE_0, ALGSTR_1;
 schemes FUNCT_2, PARTFUN1, TARSKI, XBOOLE_0;

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

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

canceled;

theorem
Th2: 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]
 proof
   let X,Y,A be set, z be set;
   assume z in A & A c= [:X,Y:];
   then consider x,y such that
   A1: x in X & y in Y & z = [x,y] by ZFMISC_1:103;
   reconsider x as Element of X by A1;
   reconsider y as Element of Y by A1;
   take x,y;
   thus thesis by A1;
 end;

theorem
Th3: 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
 proof
   let u1,u2,u3,u4 be Element of UN;
   A1: [u1,u2,u3] = [[u1,u2],u3] by MCART_1:def 3;
      [u1,u2,u3,u4] = [[u1,u2,u3],u4] by MCART_1:def 4;
   hence thesis by A1,CLASSES2:64;
 end;

theorem
Th4: for x,y st x in y & y in UN holds x in UN
 proof
   let x,y; assume
   A1: x in y & y in UN;
   then y c= UN by ORDINAL1:def 2;
   hence thesis by A1;
 end;

::  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
A1: for x,y st x in X() & y in Y() & P[x,y] holds F(x,y) in Z()
proof
  defpred R[set,set] means $1 in X() & $2 in Y() & P[$1,$2];
  deffunc G(set,set) = F($1,$2);
A2: for x,y st R[x,y] holds G(x,y) in Z() by A1;
  consider f being PartFunc of [:X(),Y():],Z() such that
  A3: (for x,y holds [x,y] in dom f iff x in X() & y in Y() & R[x,y]) and
  A4: (for x,y st [x,y] in dom f holds f.[x,y] = G(x,y)) from LambdaR2(A2);
  take f;
  thus for x,y holds [x,y] in dom f iff x in X() & y in Y() & P[x,y] by A3;
  thus for x,y st [x,y] in dom f holds f.[x,y] = F(x,y) by A4;
end;

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
A1: for x being Element of X(), y being Element of Y() st P[x,y] holds
     F(x,y) in Z()
proof
  defpred R[set,set] means P[$1,$2];
  deffunc G(set,set) = F($1,$2);
A2: for x,y st x in X() & y in Y() & R[x,y] holds G(x,y) in Z() by A1;
  consider f being PartFunc of [:X(),Y():],Z() such that
A3: for x,y holds [x,y] in dom f iff x in X() & y in Y() & R[x,y] and
A4: for x,y st [x,y] in dom f holds f.[x,y] = G(x,y) from PartLambda2(A2);
  take f;
  thus for x being Element of X(), y being Element of Y() holds
       [x,y] in dom f iff P[x,y] by A3;
  thus for x being Element of X(), y being Element of Y() st [x,y] in dom f
       holds f.[x,y] = F(x,y) by A4;
end;

::  0c. Auxiliary theorems: Trivial Group

theorem
Th5: op2.({},{}) = {} & op1.{} = {} & op0 = {}
 proof
   A1: {} in {{}} by TARSKI:def 1;
      [{},{}] in [:{{}},{{}}:] by ZFMISC_1:34;
   then op2.[{},{}] = {} by FUNCT_2:65;
   hence op2.({},{}) = {} by BINOP_1:def 1;
   thus op1.{} = {} by A1,FUNCT_2:65;
   thus op0 = {} by TARSKI:def 1;
 end;

theorem
Th6: {{}} in UN & [{{}},{{}}] in UN & [:{{}},{{}}:] in UN &
  op2 in UN & op1 in UN
 proof
   set D = {{}};
     {} in UN by CLASSES2:62;
   hence A1: D in UN by CLASSES2:63;
   hence [D,D] in UN by CLASSES2:64;
   thus A2: [:D,D:] in UN by A1,CLASSES2:67;
   A3: Funcs(D,D) in UN by A1,CLASSES2:67;
   A4: Funcs([:D,D:],D) in UN by A1,A2,CLASSES2:67;
     op2 in Funcs([:D,D:],D) by FUNCT_2:11;
   hence op2 in UN by A4,Th4;
     op1 in Funcs(D,D) by FUNCT_2:11;
   hence op1 in UN by A3,Th4;
 end;

theorem
Th7: LoopStr (# {{}},op2,Extract {} #) is midpoint_operator
 proof
   set G = LoopStr (# {{}}, op2, Extract {} #);
   A1: for a being Element of G
         ex x being Element of G st Double x = a
    proof
      let a be Element of G;
      consider x being Element of G;
      take x;
      thus Double x = {} by TARSKI:def 1
              .= a by TARSKI:def 1;
    end;
     now
     let a be Element of G;
     assume Double a = 0.G;
     thus a = {} by TARSKI:def 1
           .= 0.G by TARSKI:def 1;end;
   hence thesis by A1,MIDSP_2:def 5;
 end;

definition
 cluster L_Trivial -> midpoint_operator;
 coherence by Th7,ALGSTR_1:def 4;
end;

theorem
     (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 = {} by ALGSTR_1:def 4,TARSKI:def 1;

::  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 :Def5:
  union{Hom(a,b) where a is Object of C,b is Object of C : a in O & b in O};
 coherence by CAT_2:28;
end;

definition let C,O;
 cluster Morphs(O) -> non empty;
 coherence
   proof
    union{Hom(a,b) where a is Object of C,b is Object of C : a in O & b in O}
  = Morphs O by Def5;
    hence thesis by CAT_2:28;
   end;
end;

definition let C,O;
 func dom(O) -> Function of Morphs(O),O equals
 :Def6:  (the Dom of C)|Morphs(O);
 coherence
  proof
    set M = Morphs(O);
      M = union{Hom(a,b) where a is Object of C,b is Object of C: a in O & b in
 O}
 by Def5;
    hence (the Dom of C)|M is Function of M,O by CAT_2:29;
   end;
 func cod(O) -> Function of Morphs(O),O equals
 :Def7:  (the Cod of C)|Morphs(O);
 coherence
  proof
    set M = Morphs(O);
      M = union{Hom(a,b) where a is Object of C,b is Object of C: a in O & b in
 O}
 by Def5;
    hence (the Cod of C)|M is Function of M,O by CAT_2:29;
   end;
 func comp(O) -> PartFunc of [:Morphs(O),(Morphs(O)):],Morphs(O) equals
 :Def8:  (the Comp of C)|([:Morphs(O),Morphs(O):] qua set);
 coherence
  proof
    set M = Morphs(O);
      M = union{Hom(a,b) where a is Object of C,b is Object of C: a in O & b in
 O} by Def5;
    hence (the Comp of C)|([:M,M:] qua set)
            is PartFunc of [:M,M:],M by CAT_2:29;
   end;
 func ID(O) -> Function of O,Morphs(O) equals
 :Def9:  (the Id of C)|O;
 coherence
  proof
    set M = Morphs(O);
      M = union{Hom(a,b) where a is Object of C,b is Object of C: a in O & b in
 O}
 by Def5;
    hence (the Id of C)|O is Function of O,M by CAT_2:29;
   end;
end;

theorem
Th9: CatStr (# O,Morphs(O),dom(O),cod(O),comp(O),ID(O)#)
  is_full_subcategory_of C
 proof
   set M = Morphs(O);
   A1: M = union{Hom(a,b) where a is Object of C,b is Object of C:
     a in O & b in O} by Def5;
   A2: dom(O) = (the Dom of C)|M by Def6;
   A3: cod(O) = (the Cod of C)|M by Def7;
   A4: comp(O) = (the Comp of C)|([:M,M:] qua set) by Def8;
     ID(O) = (the Id of C)|O by Def9;
   hence thesis by A1,A2,A3,A4,CAT_2:30;
 end;

definition let C,O;
 func cat(O) -> Subcategory of C equals
 :Def10:  CatStr (# O,Morphs(O),dom(O),cod(O),comp(O),ID(O)#);
 coherence
  proof
      CatStr (# O,Morphs(O),dom(O),cod(O),comp(O),ID(O)#)
 is_full_subcategory_of C by Th9;
    hence thesis by CAT_2:def 6;
  end;
end;

definition let C,O;
 cluster cat(O) -> strict;
 coherence
  proof
      CatStr (# O,Morphs(O),dom(O),cod(O),comp(O),ID(O)#) = cat O by Def10;
    hence thesis;
  end;
end;

theorem
Th10: the Objects of cat(O) = O
 proof
     cat(O) = CatStr (# O,Morphs(O),dom(O),cod(O),comp(O),ID(O)#) by Def10;
   hence thesis;
 end;

::  1a. Maps of the carriers of groups

definition let G be 1-sorted;
 func id G -> map of G,G equals
 :Def11:  id the carrier of G;
  coherence;
end;

theorem Th11:
 for G being non empty 1-sorted,
     x being Element of G holds (id G).x = x
 proof
   let G be non empty 1-sorted;
   let x be Element of G;
      id G = id the carrier of G by Def11;
   hence thesis by FUNCT_1:35;
 end;

theorem Th12:
 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
 proof
   let G be 1-sorted, H be non empty 1-sorted;
   let f be map of G,H;
   set u = id G, v = id H, X = the carrier of G, Y = the carrier of H;
   A1: u = id X & v = id Y by Def11;
   A2: dom f = X by FUNCT_2:def 1;
     rng f c= Y by RELSET_1:12;
   hence f*u = f & v*f = f by A1,A2,RELAT_1:77,79;
 end;

definition let G,H be non empty ZeroStr;
 func ZeroMap(G,H) -> map of G,H equals
 :Def12:  (the carrier of G) --> 0.H;
 coherence
  proof
   set i = (the carrier of G) --> 0.H;
      dom i = the carrier of G & rng i = {0.H} by FUNCOP_1:14,19;
   then i is Function of the carrier of G, the carrier of H by FUNCT_2:4;
   hence i is map of G,H;
  end;
end;

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

theorem Th13:
  comp L_Trivial = op1
  proof
    reconsider f = comp L_Trivial as Function of {{}}, {{}} by ALGSTR_1:def 4;
      for x being set st x in {{}} holds op1.x = f.x
    proof
      let x be set; assume A1: x in {{}};
      then reconsider x as Element of L_Trivial by ALGSTR_1:def
4;
        x = {} by A1,TARSKI:def 1;
      then op1.x = -x by Th5,ALGSTR_1:def 4,TARSKI:def 1 .= f.x by VECTSP_1:def
25;
      hence thesis;
    end;
    hence thesis by FUNCT_2:18;
  end;

theorem
Th14: 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
 proof
   let G1,G2,G3 be non empty LoopStr,
       f be map of G1,G2, g be map of G2,G3 such that
   A1: f is additive and
   A2: g is additive;
   set h = g*f;
     now let x,y be Element of G1;
     A3: g.(f.x) = h.x & g.(f.y) = h.y by FUNCT_2:21;
     thus h.(x+y) = g.(f.(x+y)) by FUNCT_2:21
                 .= g.(f.x+f.y) by A1,Def13
                 .= h.x+h.y by A2,A3,Def13;end;
   hence thesis by Def13;
 end;

theorem Th15:
  for G being non empty ZeroStr,
      H being non empty LoopStr,
      x being Element of G holds ZeroMap(G,H).x = 0.H
 proof
   let G be non empty ZeroStr,
       H be non empty LoopStr;
   let x be Element of G;
     (ZeroMap(G,H)) = (the carrier of G) --> 0.H by Def12;
   hence thesis by FUNCOP_1:13;
 end;

theorem Th16:
  for G being non empty LoopStr,
      H being right_zeroed (non empty LoopStr) holds ZeroMap(G,H) is additive
 proof
   let G be non empty LoopStr, H be right_zeroed (non empty LoopStr);
   set f = ZeroMap(G,H);
     for x,y being Element of G holds f.(x+y) = f.x+f.y
    proof
      let x,y be Element of G;
        f.(x+y) = 0.H & f.x = 0.H & f.y = 0.H by Th15;
      hence f.(x+y) = f.x+f.y by RLVECT_1:def 7;
    end;
   hence thesis by Def13;
 end;

::  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
 :Def14:  the Dom of f;
 coherence;
 func cod(f) -> AddGroup equals
 :Def15:  the Cod of f;
 coherence;
end;

definition let f be GroupMorphismStr;
 func fun(f) -> map of dom(f),cod(f) equals
 :Def16:  the Fun of f;
 coherence
  proof
     dom(f) = the Dom of f & cod(f) = the Cod of f by Def14,Def15;
   hence the Fun of f is map of dom(f),cod(f);
  end;
end;

theorem
  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 by Def14,Def15,Def16;

definition let G,H;
 func ZERO(G,H) -> GroupMorphismStr equals
 :Def17:  GroupMorphismStr(# G,H,ZeroMap(G,H)#);
  coherence;
end;

definition let G,H;
 cluster ZERO(G,H) -> strict;
  coherence
  proof
      ZERO(G,H) = GroupMorphismStr(# G,H,ZeroMap(G,H)#) by Def17;
    hence thesis;
  end;
end;

Lm1: dom(ZERO(G,H)) = G & cod(ZERO(G,H)) = H
      & fun(ZERO(G,H)) = ZeroMap(G,H)
 proof
     ZERO(G,H) = GroupMorphismStr(# G,H,ZeroMap(G,H)#) by Def17;
   hence thesis by Def14,Def15,Def16;
 end;

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

definition
 cluster strict GroupMorphism-like GroupMorphismStr;
 existence
  proof
    consider G,H;
    set z = ZERO(G,H);
      dom(z) = G & cod(z) = H & fun(z) = ZeroMap(G,H) by Lm1;
    then fun(z) is additive by Th16;
    then z is GroupMorphism-like by Def18;
   hence thesis;
  end;
end;

definition
 mode GroupMorphism is GroupMorphism-like GroupMorphismStr;
end;

theorem
Th18: for F being GroupMorphism holds the Fun of F is additive
 proof
   let F be GroupMorphism;
   A1: the Fun of F = fun(F) by Def16;
     the Dom of F = dom(F) & the Cod of F = cod(F) by Def14,Def15;
   hence thesis by A1,Def18;
 end;

definition let G,H;
 cluster ZERO(G,H) -> GroupMorphism-like;
 coherence
  proof
    set z = ZERO(G,H);
      dom(z) = G & cod(z) = H & fun(z) = ZeroMap(G,H) by Lm1;
    then fun(z) is additive by Th16;
    hence thesis by Def18;
  end;
end;

definition let G,H;
 mode Morphism of G,H -> GroupMorphism means
 :Def19: dom(it) = G & cod(it) = H;
  existence
   proof
     take ZERO(G,H);
     thus thesis by Lm1;
   end;
end;

definition let G,H;
 cluster strict Morphism of G,H;
  existence
   proof
       dom(ZERO(G,H)) = G & cod(ZERO(G,H)) = H by Lm1;
     then ZERO(G,H) is Morphism of G,H by Def19;
    hence thesis;
   end;
end;

theorem
Th19: for f being strict GroupMorphismStr
   st dom(f) = G & cod(f) = H & fun(f) is additive
   holds f is strict Morphism of G,H
 proof
   let f be strict GroupMorphismStr; assume
   A1: dom(f) = G & cod(f) = H & fun(f) is additive;
   then reconsider f' = f as strict GroupMorphism by Def18;
     f' is strict Morphism of G,H by A1,Def19;
   hence thesis;
 end;

theorem
Th20: for f being map of G,H st f is additive
       holds GroupMorphismStr (# G,H,f#) is strict Morphism of G,H
 proof
   let f be map of G,H such that
   A1: f is additive;
   set F = GroupMorphismStr (# G,H,f#);
      dom(F) = G & cod(F) = H & fun(F) = f by Def14,Def15,Def16;
   hence thesis by A1,Th19;
 end;

theorem Th21:
  for G being non empty LoopStr holds id G is additive
proof
  let G be non empty LoopStr;
  set f = id G;
    for x,y being Element of G holds f.(x+y) = f.x+f.y
   proof
     let x,y be Element of G;
        f.(x+y) = x+y & f.x = x & f.y = y by Th11;
     hence f.(x+y) = f.x+f.y;
   end;
  hence thesis by Def13;
end;

definition let G;
 func ID G -> Morphism of G,G equals
 :Def20:  GroupMorphismStr(# G,G,id G#);
  coherence
   proof
     set i = GroupMorphismStr(# G,G,id G#);
     A1: dom(i) = G & cod(i) = G & fun(i) = id G by Def14,Def15,Def16;
       id G is additive by Th21;
     hence i is Morphism of G,G by A1,Th19;
   end;
end;

definition let G;
 cluster ID G -> strict;
  coherence
   proof
       ID G = GroupMorphismStr(# G,G,id G#) by Def20;
     hence thesis;
   end;
end;

definition let G,H;
 redefine func ZERO(G,H) -> strict Morphism of G,H;
  coherence
   proof
     set i = ZERO(G,H);
     A1: dom(i) = G & cod(i) = H & fun(i) = ZeroMap(G,H) by Lm1;
       ZeroMap(G,H) is additive by Th16;
     hence thesis by A1,Th19;
   end;
end;

theorem
Th22: 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
 proof
   let F be Morphism of G,H;
   A1: the Dom of F = dom(F) by Def14
                   .= G by Def19;
   A2: the Cod of F = cod(F) by Def15
                   .= H by Def19;
   then reconsider f = the Fun of F as map of G,H by A1;
   take f;
   thus thesis by A1,A2,Th18;
 end;

theorem
Th23: for F being strict Morphism of G,H ex f being map of G,H
       st F = GroupMorphismStr(# G,H,f#)
 proof
   let F be strict Morphism of G,H;
   consider f being map of G,H such that
   A1: F = GroupMorphismStr(# G,H,f#) & f is additive by Th22;
   take f;
   thus thesis by A1;
 end;

theorem
Th24: for F being GroupMorphism ex G,H st F is Morphism of G,H
 proof
   let F be GroupMorphism;
   take G = the Dom of F,H = the Cod of F;
     dom(F) = G & cod(F) = H by Def14,Def15;
   hence thesis by Def19;
 end;

theorem
  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
 proof
   let F be strict GroupMorphism;
   consider G,H such that
   A1: F is Morphism of G,H by Th24;
   reconsider F' = F as Morphism of G,H by A1;
   consider f being map of G,H such that
   A2: F' = GroupMorphismStr(# G,H,f#) & f is additive by Th22;
   take G,H,f;
   thus thesis by A2;
 end;

theorem
Th26: 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
 proof
   defpred P[GroupMorphism,GroupMorphism] means dom($1) = cod($2);
   let g,f be GroupMorphism such that
   A1: P[g,f];
   consider G2,G3 being AddGroup such that
   A2: g is Morphism of G2,G3 by Th24;
   A3: G2 = dom(g) by A2,Def19;
   consider G1,G2' being AddGroup such that
   A4: f is Morphism of G1,G2' by Th24;
      G2' = cod(f) by A4,Def19;
   hence thesis by A1,A2,A3,A4;
 end;

definition let G,F be GroupMorphism;
 assume A1: dom(G) = cod(F);
 func G*F -> strict GroupMorphism means
 :Def21: 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#);
 existence
  proof
    consider G1',G2',G3' being AddGroup such that
    A2: G is Morphism of G2',G3' and
    A3: F is Morphism of G1',G2' by A1,Th26;
    consider g' being map of G2',G3' such that
    A4: the GroupMorphismStr of G = GroupMorphismStr(# G2',G3',g'#)and
    A5: g' is additive by A2,Th22;
    consider f' being map of G1',G2' such that
    A6: the GroupMorphismStr of F = GroupMorphismStr(# G1',G2',f'#)and
    A7: f' is additive by A3,Th22;
       g'*f' is additive by A5,A7,Th14;
    then reconsider T' = (GroupMorphismStr(# G1',G3',g'*f'#))
 as strict GroupMorphism by Th20;
    take T';
    thus thesis by A4,A6;
  end;
 uniqueness
  proof
    let S1,S2 be strict GroupMorphism such that
    A8: 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 S1 = GroupMorphismStr(# G1,G3,g*f#)and
    A9: 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 S2 = GroupMorphismStr(# G1,G3,g*f#);
    consider G2',G3' being AddGroup such that
    A10: G is Morphism of G2',G3' by Th24;
    reconsider G' = G as Morphism of G2',G3' by A10;
    A11: G2' = dom(G) by A10,Def19;
    consider G1',G2'' being AddGroup such that
    A12: F is Morphism of G1',G2'' by Th24;
    reconsider F' = F as Morphism of G1',G2'' by A12;
    reconsider F' as Morphism of G1',G2' by A1,A11,Def19;
    consider g' being map of G2',G3' such that
    A13: the GroupMorphismStr of G' = GroupMorphismStr(# G2',G3',g'#)
and g' is additive by Th22;
    consider f' being map of G1',G2' such that
    A14: the GroupMorphismStr of F' = GroupMorphismStr(# G1',G2',f'#)
and f' is additive by Th22;
    thus S1 = (GroupMorphismStr(# G1',G3',g'*f'#)) by A8,A13,A14
           .= S2 by A9,A13,A14;
  end;
end;

canceled;

theorem
Th28: 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
 proof
   let G1,G2,G3 be AddGroup,
       G be Morphism of G2,G3, F be Morphism of G1,G2;
   consider g being map of G2,G3 such that
   A1: the GroupMorphismStr of G = GroupMorphismStr(# G2,G3,g#)
and g is additive by Th22;
   consider f being map of G1,G2 such that
   A2: the GroupMorphismStr of F = GroupMorphismStr(# G1,G2,f#)
and f is additive by Th22;
     dom(G) = G2 by Def19
         .= cod(F) by Def19;
   then G*F = GroupMorphismStr(# G1,G3,g*f#) by A1,A2,Def21;
   then dom(G*F) = G1 & cod(G*F) = G3 by Def14,Def15;
   hence thesis by Def19;
 end;

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;
 coherence by Th28;
end;

theorem
Th29: 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#)
proof
  let G1,G2,G3 be AddGroup,
      G be Morphism of G2,G3, F be Morphism of G1,G2,
      g be map of G2,G3, f be map of G1,G2 such that
  A1: G = GroupMorphismStr(# G2,G3,g#) & F = GroupMorphismStr(# G1,G2,f#);
    dom(G) = G2 by Def19
        .= cod(F) by Def19;
  hence thesis by A1,Def21;
end;

 theorem
 Th30: 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#)
  proof
    let f,g be strict GroupMorphism such that
    A1: dom g = cod f;
    set G1 = dom f,G2 = cod f, G3 = cod g;
    reconsider f' = f as strict Morphism of G1,G2 by Def19;
    reconsider g' = g as strict Morphism of G2,G3 by A1,Def19;
    consider f0 being map of G1,G2 such that
    A2: f' = GroupMorphismStr(# G1,G2,f0#) by Th23;
    consider g0 being map of G2,G3 such that
    A3: g' = GroupMorphismStr(# G2,G3,g0#) by Th23;
    take G1,G2,G3,f0,g0;
    thus thesis by A2,A3,Th29;
  end;

 theorem
 Th31: for f,g being strict GroupMorphism st dom g = cod f holds
     dom(g*f) = dom f & cod (g*f) = cod g
 proof
   let f,g be strict GroupMorphism; assume
      dom g = cod f;
   then consider G1,G2,G3 being AddGroup,
   f0 being map of G1,G2, g0 being map of G2,G3 such that
   A1: f = GroupMorphismStr(# G1,G2,f0#)
     & g = GroupMorphismStr(# G2,G3,g0#)
     & g*f = GroupMorphismStr(# G1,G3,g0*f0#) by Th30;
   thus dom(g*f) = G1 by A1,Def14
                .= dom f by A1,Def14;
   thus cod(g*f) = G3 by A1,Def15
                .= cod g by A1,Def15;
 end;

 theorem
 Th32: 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
 proof
   let G1,G2,G3,G4 be AddGroup, f be strict Morphism of G1,G2,
       g be strict Morphism of G2,G3, h be strict Morphism of G3,G4;
   consider f0 being map of G1,G2 such that
   A1: f = GroupMorphismStr(# G1,G2,f0#) by Th23;
   consider g0 being map of G2,G3 such that
   A2: g = GroupMorphismStr(# G2,G3,g0#) by Th23;
   consider h0 being map of G3,G4 such that
   A3: h = GroupMorphismStr(# G3,G4,h0#) by Th23;
   A4: g*f = GroupMorphismStr(# G1,G3,g0*f0#) by A1,A2,Th29;
   A5: h*g = GroupMorphismStr(# G2,G4,h0*g0#) by A2,A3,Th29;
     h*(g*f) = GroupMorphismStr(# G1,G4,h0*(g0*f0)#) by A3,A4,Th29
          .= GroupMorphismStr(# G1,G4,(h0*g0)*f0#) by RELAT_1:55
          .= (h*g)*f by A1,A5,Th29;
   hence thesis;
 end;

 theorem
 Th33: for f,g,h being strict GroupMorphism
        st dom h = cod g & dom g = cod f holds h*(g*f) = (h*g)*f
  proof
    let f,g,h be strict GroupMorphism such that
    A1: dom h = cod g & dom g = cod f;
    set G2 = cod f, G3 = cod g;
    reconsider f' = f as Morphism of (dom f),G2 by Def19;
    reconsider g' = g as Morphism of G2,G3 by A1,Def19;
    reconsider h' = h as Morphism of G3,(cod h) by A1,Def19;
      h'*(g'*f') = (h'*g')*f' by Th32;
    hence thesis;
  end;

 theorem
 Th34: 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)
 proof
   set i = ID G;
   thus dom i = G by Def19;
   thus cod i = G by Def19;
   thus for f being strict GroupMorphism st cod f = G holds i*f = f
    proof
      let f be strict GroupMorphism such that
      A1: cod f = G;
      set H = dom(f);
      reconsider f' = f as Morphism of H,G by A1,Def19;
      A2: dom(i) = G by Def19;
      A3: i = GroupMorphismStr(# G,G,id G#) by Def20;
      consider m being map of H,G such that
      A4: f' = GroupMorphismStr(# H,G,m#) by Th23;
         (id G)*m = m by Th12;
      hence i*f = f by A1,A2,A3,A4,Def21;
    end;
   thus for g being strict GroupMorphism st dom g = G holds g*(ID G) = g
    proof
      let f be strict GroupMorphism such that
      A5: dom f = G;
      set H = cod(f);
      reconsider f' = f as Morphism of G,H by A5,Def19;
      A6: cod(i) = G by Def19;
      A7: i = GroupMorphismStr(# G,G,id G#) by Def20;
      consider m being map of G,H such that
      A8: f' = GroupMorphismStr(# G,H,m#) by Th23;
         m*(id G) = m by Th12;
      hence f*i = f by A5,A6,A7,A8,Def21;
    end;
 end;

::  2. Domains of groups

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

definition
 cluster Group_DOMAIN-like non empty set;
 existence
  proof
    set D = {L_Trivial};
A1: for x be set st x in D holds x is strict AddGroup by TARSKI:def 1;
    take D;
    thus thesis by A1,Def22;
  end;
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;
  coherence by Def22;
end;

definition let V;
 cluster strict Element of V;
  existence
   proof consider v being Element of V;
       v is strict AddGroup by Def22;
    hence thesis;
   end;
end;

::  3. Domains of morphisms

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

definition
 cluster GroupMorphism_DOMAIN-like non empty set;
   existence
    proof
      consider G;
      take {ID G};
        for x being set st x in {ID G} holds x is strict GroupMorphism
 by TARSKI:def 1;
      hence thesis by Def23;
    end;
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;
  coherence by Def23;
end;

definition let M be GroupMorphism_DOMAIN;
 cluster strict Element of M;
  existence
   proof consider m being Element of M;
       m is strict GroupMorphism by Def23;
    hence thesis;
   end;
end;

canceled 2;

theorem
Th37: for f being strict GroupMorphism holds {f} is GroupMorphism_DOMAIN
 proof
   let f be strict GroupMorphism;
     for x being set st x in {f} holds x is strict GroupMorphism by TARSKI:def
1
;
   hence thesis by Def23;
 end;

definition let G,H;
 mode GroupMorphism_DOMAIN of G,H -> GroupMorphism_DOMAIN means
 :Def24: for x being Element of it holds x is strict Morphism of G,H;
  existence
   proof
     reconsider D = {ZERO(G,H)} as GroupMorphism_DOMAIN by Th37;
     take D;
     thus thesis by TARSKI:def 1;
   end;
end;

theorem
Th38: D is GroupMorphism_DOMAIN of G,H
       iff for x being Element of D holds x is strict Morphism of G,H
 proof
   thus D is GroupMorphism_DOMAIN of G,H
    implies for x being Element of D holds x is strict Morphism of G,H
 by Def24;
   thus (for x being Element of D holds x is strict Morphism of G,H)
    implies D is GroupMorphism_DOMAIN of G,H
    proof
      assume A1: for x being Element of D holds x is strict Morphism of G,H;
      then for x being set st x in D holds x is strict GroupMorphism;
      then reconsider D' = D as GroupMorphism_DOMAIN by Def23;
        for x being Element of D' holds x is strict Morphism of G,H by A1;
      hence thesis by Def24;
    end;
 end;

theorem
  for f being strict Morphism of G,H holds {f} is GroupMorphism_DOMAIN of G,H
 proof
   let f be strict Morphism of G,H;
     for x being Element of {f} holds x is strict Morphism of G,H
 by TARSKI:def 1;
   hence thesis by Th38;
 end;

definition let G,H be 1-sorted;
 mode MapsSet of G,H means
:Def25: for x being set st x in it holds x is map of G,H;
 existence
  proof take {};
   thus thesis;
  end;
end;

definition let G,H be 1-sorted;
 func Maps(G,H) -> MapsSet of G,H equals
:Def26:  Funcs(the carrier of G, the carrier of H);
 coherence
  proof let x be set;
   assume x in Funcs(the carrier of G, the carrier of H);
    then x is Function of the carrier of G, the carrier of H by FUNCT_2:121;
   hence thesis;
  end;
end;

definition let G be 1-sorted, H be non empty 1-sorted;
 cluster Maps(G,H) -> non empty;
 coherence
  proof Maps(G,H) = Funcs(the carrier of G, the carrier of H) by Def26;
   hence thesis;
  end;
end;

definition let G be 1-sorted, H be non empty 1-sorted;
 cluster non empty MapsSet of G,H;
 existence
  proof Maps(G,H) is non empty;
   hence thesis;
  end;
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;
 coherence by Def25;
end;

definition let G,H;
 func Morphs(G,H) -> GroupMorphism_DOMAIN of G,H means
 :Def27: x in it iff x is strict Morphism of G,H;
  existence
   proof
     set D = { GroupMorphismStr(# G,H,f#) where f is Element of
                     Maps(G,H) : f is additive };
       ZeroMap(G,H) is Element of
        Funcs(the carrier of G, the carrier of H) by FUNCT_2:11;
     then reconsider f0 = ZeroMap(G,H) as Element of Maps(G,H) by Def26;
       f0 is additive by Th16;
     then GroupMorphismStr(# G,H,f0#) in D;
     then reconsider D as non empty set;
     A1: x in D implies x is strict Morphism of G,H
      proof
        assume x in D;
        then ex f being Element of
         Maps(G,H) st x = GroupMorphismStr (# G,H,f#) & f is additive;
        hence thesis by Th20;
      end;
     then A2: for x being Element of D holds x is strict Morphism of G,H;
A3:      x is strict Morphism of G,H implies x in D
      proof
        assume x is strict Morphism of G,H;
        then reconsider x as strict Morphism of G,H;
          dom(x) = G & cod(x) = H by Def19;
        then A4: the Dom of x = G & the Cod of x = H by Def14,Def15;
        A5: (the Fun of x) is additive by Th18;
        reconsider f = the Fun of x as map of G,H by A4;
          f is Element of Funcs(the carrier of G, the carrier of H)
 by FUNCT_2:11;
        then reconsider g = f as Element of Maps(G,H) by Def26;
          x = GroupMorphismStr(# G,H,g #) by A4;
        hence thesis by A5;
      end;
     reconsider D as GroupMorphism_DOMAIN of G,H by A2,Th38;
     take D;
     thus thesis by A1,A3;
   end;
  uniqueness
   proof
     let D1,D2 be GroupMorphism_DOMAIN of G,H such that
     A6: x in D1 iff x is strict Morphism of G,H and
     A7: x in D2 iff x is strict Morphism of G,H;
       x in D1 iff x in D2
      proof
        thus x in D1 implies x in D2
         proof
           assume x in D1;
           then x is strict Morphism of G,H by A6;
           hence thesis by A7;
         end;
        thus x in D2 implies x in D1
         proof
           assume x in D2;
           then x is strict Morphism of G,H by A7;
           hence thesis by A6;
         end;
      end;
     hence thesis by TARSKI:2;
   end;
end;

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

definition let G,H; let M be GroupMorphism_DOMAIN of G,H;
 cluster strict Element of M;
  existence
   proof consider m being Element of M;
       m is strict Morphism of G,H by Def24;
    hence thesis;
   end;
end;

::  4a. Category of groups - objects

definition let x,y;
 pred GO x,y means
 :Def28: 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
Th40: for x,y1,y2 being set st GO x,y1 & GO x,y2 holds y1 = y2
 proof
   let x,y1,y2 be set such that
   A1: GO x,y1 and
   A2: GO x,y2;
   consider a1,a2,a3,a4 being set such that
     A3: x = [a1,a2,a3,a4]and
     A4: ex G being strict AddGroup st y1 = G
                 & a1 = the carrier of G
                 & a2 = the add of G
                 & a3 = comp G
                 & a4 = the Zero of G by A1,Def28;
   consider b1,b2,b3,b4 being set such that
   A5: x = [b1,b2,b3,b4]and
   A6: ex G being strict AddGroup st y2 = G
               & b1 = the carrier of G
               & b2 = the add of G
               & b3 = comp G
               & b4 = the Zero of G by A2,Def28;
   consider G1 being strict AddGroup such that
   A7: y1 = G1
       & a1 = the carrier of G1
       & a2 = the add of G1
       & a3 = comp G1
       & a4 = the Zero of G1 by A4;
   consider G2 being strict AddGroup such that
   A8: y2 = G2
       & b1 = the carrier of G2
       & b2 = the add of G2
       & b3 = comp G2
       & b4 = the Zero of G2 by A6;
       the carrier of G1 = the carrier of G2
   & the add of G1 = the add of G2
   & comp G1 = comp G2
   & the Zero of G1 = the Zero of G2 by A3,A5,A7,A8,MCART_1:33;
   hence thesis by A7,A8;
 end;

theorem
Th41: ex x st x in UN & GO x,L_Trivial
 proof
    reconsider u = {} as Element of UN by CLASSES2:62;
    set x1 = {u};
      Extract {} = u by ALGSTR_1:def 3;
    then reconsider x4 = Extract {} as Element of UN;
    reconsider x3 = comp L_Trivial as Element of UN by Th6,Th13;
    reconsider x2 = op2 as Element of UN by Th6;
    set x = [x1,x2,x3,x4];
    A1: x is Element of UN by Th3;
    take x;
    thus thesis by A1,Def28,ALGSTR_1:def 4;
 end;

definition let UN;
 func GroupObjects(UN) -> set means
 :Def29: for y holds y in it iff ex x st x in UN & GO x,y;
 existence
  proof
    defpred P[set,set] means GO $1,$2;
A1: for x,y1,y2 being set st P[x,y1] & P[x,y2] holds y1 = y2 by Th40;
    consider Y being set such that
    A2: for y holds y in Y iff ex x st x in UN & P[x,y] from Fraenkel(A1);
    take Y;
    thus thesis by A2;
  end;
 uniqueness
 proof
   defpred P[set] means ex x st x in UN & GO x,$1;
   for X1,X2 being set st
    (for x being set holds x in X1 iff P[x]) &
    (for x being set holds x in X2 iff P[x]) holds X1 = X2 from SetEq;
   hence thesis;
 end;
end;

theorem
Th42: L_Trivial in GroupObjects(UN)
 proof
     ex x st x in UN & GO x,L_Trivial by Th41;
   hence thesis by Def29;
 end;

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

theorem
Th43: for x being Element of GroupObjects(UN) holds x is strict AddGroup
 proof
   let x be Element of GroupObjects(UN);
   consider u being set such that
   A1: u in UN & GO u,x by Def29;
      ex x1,x2,x3,x4 being set st
 u = [x1,x2,x3,x4] & ex G being strict AddGroup
    st x = G
    & x1 = the carrier of G
    & x2 = the add of G
    & x3 = comp G
    & x4 = the Zero of G by A1,Def28;
   hence thesis;
 end;

definition let UN;
  cluster GroupObjects(UN) -> Group_DOMAIN-like;
   coherence
    proof
        for x being set st x in GroupObjects(UN) holds x is strict AddGroup
 by Th43;
      hence thesis by Def22;
    end;
end;

::  4b. Category of groups - morphisms

definition let V;
 func Morphs(V) -> GroupMorphism_DOMAIN means
 :Def30: for x holds x in it iff ex G,H being strict Element of V
  st x is strict Morphism of G,H;
  existence
   proof
     consider G0,H0 being strict Element of V;
     set M = Morphs(G0,H0), S = { Morphs(G,H) where
      G is strict Element of V, H is strict Element of V :
         not contradiction };
     A1: (ZERO(G0,H0)) is Element of M by Def27;
       M in S;
     then reconsider T = union S as non empty set by A1,TARSKI:def 4;
     A2: for x holds x in T iff ex G,H being strict Element of V
          st x is strict Morphism of G,H
      proof
        let x;
        thus x in T implies ex G,H being strict Element of V
                            st x is strict Morphism of G,H
         proof
           assume x in T;
           then consider Y being set such that
           A3: x in Y and
           A4: Y in S by TARSKI:def 4;
           consider G,H being strict Element of V such that
           A5: Y = Morphs(G,H) by A4;
           take G,H;
          thus thesis by A3,A5,Def27;
         end;
        thus (ex G,H being strict Element of V
                  st x is strict Morphism of G,H) implies x in T
         proof
           given G,H being strict Element of V such that
           A6: x is strict Morphism of G,H;
           set M = Morphs(G,H);
           A7: x in M by A6,Def27;
             M in S;
           hence thesis by A7,TARSKI:def 4;
         end;
     end;
       now let x be set;
       assume x in T;
        then ex G,H being strict Element of V st
          x is strict Morphism of G,H by A2;
       hence x is strict GroupMorphism;end;
     then reconsider T' = T as GroupMorphism_DOMAIN by Def23;
     take T';
     thus thesis by A2;
   end;
  uniqueness
   proof
     let D1,D2 be GroupMorphism_DOMAIN such that
     A8: for x holds x in D1 iff ex G,H being strict Element of V
      st x is strict Morphism of G,H and
     A9: for x holds x in D2 iff ex G,H being strict Element of V
      st x is strict Morphism of G,H;
       now let x;
         x in D1 iff
        ex G,H being strict Element of V st x is strict Morphism of G,H
 by A8;
       hence x in D1 iff x in D2 by A9;end;
     hence thesis by TARSKI:2;
   end;
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;
  coherence
   proof
     consider G,H being strict Element of V such that
     A1: F is strict Morphism of G,H by Def30;
     reconsider F' = F as Morphism of G,H by A1;
       dom(F') = G by Def19;
     hence thesis;
   end;
 func cod(F) -> strict Element of V;
  coherence
   proof
     consider G,H being strict Element of V such that
     A2: F is strict Morphism of G,H by Def30;
     reconsider F' = F as Morphism of G,H by A2;
       cod(F') = H by Def19;
     hence thesis;
   end;
end;

definition let V; let G be Element of V;
 func ID(G) -> strict Element of Morphs(V) equals
 :Def31:  ID(G);
 coherence
  proof
    reconsider G' = G as strict Element of V by Def22;
       ID(G') is strict Element of Morphs(V) by Def30;
   hence thesis;
  end;
end;

definition let V;
 func dom(V) -> Function of Morphs(V),V means
 :Def32: for f being Element of Morphs(V) holds it.f = dom(f);
  existence
    proof
      deffunc F(Element of Morphs(V)) = dom $1;
      consider F being Function of Morphs(V),V such that
      A1: for f being Element of Morphs(V) holds F.f = F(f) from LambdaD;
      take F;
      thus thesis by A1;
    end;
  uniqueness
   proof
     let F1,F2 be Function of Morphs(V),V such that
     A2: for f being Element of Morphs(V) holds F1.f = dom(f) and
     A3: for f being Element of Morphs(V) holds F2.f = dom(f);
       now let f be Element of Morphs(V);
         F1.f = dom(f) by A2;
       hence F1.f = F2.f by A3;end;
     hence thesis by FUNCT_2:113;
   end;
 func cod(V) -> Function of Morphs(V),V means
 :Def33: for f being Element of Morphs(V) holds it.f = cod(f);
  existence
    proof
      deffunc F(Element of Morphs(V)) = cod $1;
      consider F being Function of Morphs(V),V such that
      A4: for f being Element of Morphs(V) holds F.f = F(f) from LambdaD;
      take F;
      thus thesis by A4;
    end;
  uniqueness
   proof
     let F1,F2 be Function of Morphs(V),V such that
     A5: for f being Element of Morphs(V) holds F1.f = cod(f) and
     A6: for f being Element of Morphs(V) holds F2.f = cod(f);
       now let f be Element of Morphs(V);
         F1.f = cod(f) by A5;
       hence F1.f = F2.f by A6;end;
     hence thesis by FUNCT_2:113;
   end;
 func ID(V) -> Function of V,Morphs(V) means
 :Def34: for G being Element of V holds it.G = ID(G);
  existence
    proof
      deffunc F(Element of V) = ID $1;
      consider F being Function of V,Morphs(V) such that
      A7: for G being Element of V holds F.G = F(G) from LambdaD;
      take F;
      thus thesis by A7;
    end;
  uniqueness
   proof
     let F1,F2 be Function of V,Morphs(V) such that
     A8: for G being Element of V holds F1.G = ID(G) and
     A9: for G being Element of V holds F2.G = ID(G);
       now let G be Element of V;
         F1.G = ID(G) by A8;
       hence F1.G = F2.G by A9;end;
     hence thesis by FUNCT_2:113;
   end;
 end;

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

theorem
Th44: 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
 proof
   set X = Morphs(V);
   defpred P[Element of X,Element of X] means dom($1) = cod($2);
   let g,f be Element of X such that
   A1: P[g,f];
   consider G2,G3 being strict Element of V such that
   A2: g is strict Morphism of G2,G3 by Def30;
   A3: G2 = dom(g) by A2,Def19;
   consider G1,G2' being strict Element of V such that
   A4: f is strict Morphism of G1,G2' by Def30;
      G2' = cod(f) by A4,Def19;
   hence thesis by A1,A2,A3,A4;
 end;

theorem
Th45: for g,f being Element of Morphs(V) st dom(g) = cod(f)
      holds g*f in Morphs(V)
 proof
   set X = Morphs(V);
   defpred P[Element of X,Element of X] means dom($1) = cod($2);
   let g,f be Element of X; assume
      P[g,f];
   then consider G1,G2,G3 being strict Element of V such that
   A1: g is Morphism of G2,G3 & f is Morphism of G1,G2 by Th44;
   reconsider g' = g as Morphism of G2,G3 by A1;
   reconsider f' = f as Morphism of G1,G2 by A1;
     g'*f' is Morphism of G1,G3;
   hence thesis by Def30;
 end;

definition let V;
 func comp(V) -> PartFunc of [:Morphs(V),Morphs(V):],Morphs(V) means
 :Def35:
 (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);
 existence
  proof
    set X = Morphs(V);
    defpred P[Element of X,Element of X] means dom($1) = cod($2);
    deffunc F(Element of X,Element of X) = $1*$2;
    A1: for g,f being Element of X st P[g,f] holds F(g,f) in X by Th45;
    consider c being PartFunc of [:X,X:],X such that
    A2: for g,f being Element of X holds [g,f] in dom c iff P[g,f] and
    A3: for g,f being Element of X st [g,f] in dom c
        holds c.[g,f] = F(g,f) from PartLambda2D(A1);
    take c;
    thus thesis by A2,A3;
  end;
 uniqueness
  proof
    set X = Morphs(V);
    defpred P[Element of X,Element of X] means dom($1) = cod($2);
    let c1,c2 be PartFunc of [:X,X:],X such that
    A4: for g,f being Element of X holds [g,f] in dom c1 iff P[g,f] and
    A5: for g,f being Element of X st [g,f] in dom c1
         holds c1.[g,f] = g*f and
    A6: for g,f being Element of X holds [g,f] in dom c2 iff P[g,f] and
    A7: for g,f being Element of X st [g,f] in dom c2
         holds c2.[g,f] = g*f;
    A8: dom c1 c= [:X,X:] & dom c2 c= [:X,X:] by RELSET_1:12;
    A9: dom c1 = dom c2
     proof
         now let x; assume
         A10: x in dom c1;
         then consider g,f being Element of X such that
         A11: x = [g,f] by A8,Th2;
           P[g,f] by A4,A10,A11;
         hence x in dom c2 by A6,A11;end;
       then A12: dom c1 c= dom c2 by TARSKI:def 3;
         now let x; assume
         A13: x in dom c2;
         then consider g,f being Element of X such that
         A14: x = [g,f] by A8,Th2;
           P[g,f] by A6,A13,A14;
         hence x in dom c1 by A4,A14;end;
       then dom c2 c= dom c1 by TARSKI:def 3;
       hence thesis by A12,XBOOLE_0:def 10;
     end;
    set V' = dom c1;
      for x,y st [x,y] in V' holds c1.[x,y]=c2.[x,y]
     proof
       let x,y;assume
       A15: [x,y] in V';
       then reconsider x,y as Element of X by A8,ZFMISC_1:106;
         c1.[x,y] = x*y by A5,A15;
       hence thesis by A7,A9,A15;
     end;
    hence thesis by A9,PARTFUN1:35;
  end;
end;

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

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

definition let UN;
 cluster GroupCat(UN) -> strict;
 coherence
 proof
    GroupCat UN = CatStr(# GroupObjects(UN),Morphs(GroupObjects(UN)),
   dom(GroupObjects(UN)),cod(GroupObjects(UN)),
   comp(GroupObjects(UN)),ID(GroupObjects(UN))#) by Def36;
  hence thesis;
 end;
end;

theorem
 Th46: for f,g being Morphism of GroupCat(UN) holds
        [g,f] in dom(the Comp of GroupCat(UN)) iff dom g = cod f
  proof
    set C = GroupCat(UN), V = GroupObjects(UN);
A1:    C = CatStr(# V,Morphs(V),dom(V),cod(V),comp(V),ID(V)#) by Def36;
    let f,g be Morphism of C;
    reconsider f' = f as Element of Morphs(V) by A1;
    reconsider g' = g as Element of Morphs(V) by A1;
    A2: dom g = dom(V).g' by A1,CAT_1:def 2
             .= dom(g') by Def32;
       cod f = cod(V).f' by A1,CAT_1:def 3
             .= cod(f') by Def33;
    hence thesis by A1,A2,Def35;
  end;

theorem
 Th47: 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)
 proof
   set C = GroupCat(UN), V = GroupObjects(UN); set X = Morphs(V);
A1:   C = CatStr(# V,X,dom(V),cod(V),comp(V),ID(V)#) by Def36;
  let f  be (Morphism of C),
      f' be Element of X,
      b  be Object of C,
      b' be Element of V;
     ex G,H being strict Element of V st f is strict Morphism of G,H
 by A1,Def30;
  hence f is strict Element of X by A1;
  thus f' is Morphism of C by A1;
   consider x such that
A2: x in UN & GO x,b by A1,Def29;
     ex x1,x2,x3,x4 being set st
    x = [x1,x2,x3,x4] &
    ex G being strict AddGroup
    st b = G
    & x1 = the carrier of G
    & x2 = the add of G
    & x3 = comp G
    & x4 = the Zero of G by A2,Def28;
  hence b is strict Element of V by A1;
  thus b' is Object of C by A1;
 end;

theorem
 Th48: for b  being Object of GroupCat(UN),
           b' being Element of GroupObjects(UN)
       st b = b' holds id b = ID(b')
 proof
   set C = GroupCat(UN), V = GroupObjects(UN);
A1:   C = CatStr(# V,(Morphs(V)),dom(V),cod(V),comp(V),ID(V)#) by Def36;
   let b  be Object of C, b' be Element of V; assume
      b = b';
   hence id b = (ID(V)).b' by A1,CAT_1:def 5
            .= ID(b') by Def34;
 end;

 theorem
 Th49: 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'
 proof
   set C = GroupCat(UN), V = GroupObjects(UN); set X = Morphs(V);
A1:   C = CatStr(# V,X,dom(V),cod(V),comp(V),ID(V)#) by Def36;
  let f be (Morphism of C), f' be Element of X; assume
  A2: f = f';
  hence dom f = dom(V).f' by A1,CAT_1:def 2
            .= dom f' by Def32;
  thus cod f = cod(V).f' by A1,A2,CAT_1:def 3
            .= cod f' by Def33;
 end;

 theorem
 Th50: 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')
 proof
   set C = GroupCat(UN), V = GroupObjects(UN); set X = Morphs(V);
A1:   C = CatStr(# V,X,dom(V),cod(V),comp(V),ID(V)#) by Def36;
  let f,g be Morphism of C;
  let f',g' be Element of X; assume
  A2: f = f' & g = g';
  then A3: dom g = dom g' by Th49;
  A4: cod f = cod f' by A2,Th49;
  A5: dom f = dom f' by A2,Th49;
  A6: cod g = cod g' by A2,Th49;
  thus dom g = cod f iff dom g' = cod f' by A2,A4,Th49;
  thus A7: dom g = cod f iff [g',f'] in dom comp(V) by A3,A4,Def35;
  thus dom g = cod f implies g*f = g'*f'
   proof
     assume A8: dom g = cod f;
     then [g,f] in dom (the Comp of C) by Th46;
     hence g*f = (comp(V)).[g',f'] by A1,A2,CAT_1:def 4
              .= g'*f' by A7,A8,Def35;
   end;
  thus dom f = dom g iff dom f' = dom g' by A2,A5,Th49;
  thus cod f = cod g iff cod f' = cod g' by A2,A6,Th49;
 end;

 Lm2: for f,g being Morphism of GroupCat(UN) st dom g = cod f holds
     dom(g*f) = dom f
   & cod (g*f) = cod g
  proof set X = Morphs(GroupObjects(UN));
    let f,g be Morphism of GroupCat(UN) such that
    A1: dom g = cod f;
    reconsider f' = f as strict Element of X by Th47;
    reconsider g' = g as strict Element of X by Th47;
    A2: dom g' = cod f' by A1,Th50;
    then A3: dom(g'*f') = dom f'
      & cod (g'*f') = cod g' by Th31;
    reconsider gf = g'*f' as Element of X by A2,Th45;
      gf = g*f by A1,Th50;
    hence thesis by A3,Th50;
 end;

 Lm3: for f,g,h being Morphism of GroupCat(UN)
        st dom h = cod g & dom g = cod f holds h*(g*f) = (h*g)*f
  proof set X = Morphs(
(GroupObjects(UN)));
    let f,g,h be Morphism of (GroupCat(UN)) such that
    A1: dom h = cod g & dom g = cod f;
    reconsider f'=f, g'=g, h'=h as strict Element of X by Th47;
    A2: dom h' = cod g' & dom g' = cod f' by A1,Th50;
    A3: g'*f' = g*f & h'*g' = h*g by A1,Th50;
    reconsider gf = g'*f', hg = h'*g' as Element of X by A2,Th45;
    A4: dom(h) = cod(g*f) by A1,Lm2;
    A5: dom(h*g) = cod(f) by A1,Lm2;
      h*(g*f) = h'*gf by A3,A4,Th50
           .= hg*f' by A2,Th33
           .= (h*g)*f by A3,A5,Th50;
    hence thesis;
  end;

 Lm4: for b being Object of GroupCat(UN) holds
    dom id b = b
  & cod id b = b
  & (for f being Morphism of GroupCat(UN)
       st cod f = b holds (id b)*f = f)
  & (for g being Morphism of GroupCat(UN)
       st dom g = b holds g*(id b) = g)
proof
  set C = GroupCat(UN), V = GroupObjects(UN); set X = Morphs(V);
  let b be Object of C;
  reconsider b' = b as Element of V by Th47;
  reconsider b'' = b' as AddGroup;
  A1: id b = ID(b') by Th48;
  hence A2: dom id b = dom ID(b') by Th49
                   .= dom ID(b'') by Def31
                   .= b by Th34;
  thus A3: cod id b = cod ID(b') by A1,Th49
                   .= cod ID(b'') by Def31
                   .= b by Th34;
  thus for f being Morphism of C st cod f = b holds (id b)*f = f
   proof
     let f be Morphism of C such that
     A4: cod f = b;
     reconsider f1 = f as strict Element of X by Th47;
     reconsider f' = f1 as strict GroupMorphism;
     A5: cod f' = b'' by A4,Th49;
     thus (id b)*f = ID(b')*f' by A1,A2,A4,Th50
                  .= ID(b'')*f' by Def31
                  .= f by A5,Th34;
   end;
  thus for g being Morphism of C st dom g = b holds g*(id b) = g
   proof
     let f be Morphism of C such that
     A6: dom f = b;
     reconsider f1 = f as strict Element of X by Th47;
     reconsider f' = f1 as strict GroupMorphism;
     A7: dom f' = b'' by A6,Th49;
     thus f*(id b) = f'*ID(b') by A1,A3,A6,Th50
                  .= f'*ID(b'') by Def31
                  .= f by A7,Th34;
   end;
end;

definition let UN;
 cluster GroupCat(UN) -> Category-like;
 coherence
  proof
         ( for f,g being Morphism of GroupCat(UN)
          holds [g,f] in dom(the Comp of GroupCat(UN)) iff dom g = cod f )
     & ( for f,g being Morphism of GroupCat(UN) st dom g = cod f
          holds dom(g*f) = dom f & cod (g*f) = cod g )
     & ( for f,g,h being Morphism of GroupCat(UN)
          st dom h = cod g & dom g = cod f holds h*(g*f) = (h*g)*f )
     & ( for b being Object of GroupCat(UN)
          holds dom id b = b & cod id b = b &
           (for f being Morphism of GroupCat(UN)
             st cod f = b holds (id b)*f = f) &
           (for g being Morphism of GroupCat(UN)
             st dom g = b holds g*(id b) = g) ) by Lm2,Lm3,Lm4,Th46;
   hence thesis by CAT_1:29;
  end;
end;

definition let UN;
 func AbGroupObjects(UN) -> Subset of the Objects of GroupCat(UN) equals
 :Def37:  {G where G is Element of the Objects of GroupCat(UN)
                 : ex H being AbGroup st G = H};
 coherence
  proof
    set D2 = the Objects of GroupCat(UN);
      now
      let x be set;
      assume x in {G where G is Element of D2 : ex H being AbGroup st G = H};
      then ex G being Element of D2 st x = G & ex H being AbGroup st G = H;
      hence x in D2;end;
    hence thesis by TARSKI:def 3;
  end;
end;

theorem
Th51: L_Trivial in AbGroupObjects(UN)
 proof
    set D2 = the Objects of GroupCat(UN);
    set T = L_Trivial;
      GroupCat(UN) = CatStr(# GroupObjects(UN),Morphs(GroupObjects(UN)),
                   dom(GroupObjects(UN)),cod(GroupObjects(UN)),
                   comp(GroupObjects(UN)),ID(GroupObjects(UN))#) by Def36;
    then T in D2 by Th42;
    then T in {G where G is Element of D2 : ex H being AbGroup st G = H};
    hence thesis by Def37;
 end;

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

definition let UN;
 func AbGroupCat(UN) -> Subcategory of GroupCat(UN) equals
 :Def38:  cat(AbGroupObjects(UN));
 coherence;
end;

definition let UN;
 cluster AbGroupCat(UN) -> strict;
 coherence
 proof
    AbGroupCat(UN) = cat(AbGroupObjects(UN)) by Def38;
  hence thesis;
 end;
end;

theorem
Th52: the Objects of AbGroupCat(UN) = AbGroupObjects(UN)
 proof
     AbGroupCat(UN) = cat(AbGroupObjects(UN)) by Def38;
   hence thesis by Th10;
 end;

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

definition let UN;
 func MidOpGroupObjects(UN) -> Subset of the Objects of AbGroupCat(UN) equals
 :Def39:  {G where G is Element of the Objects of AbGroupCat(UN)
                 : ex H being midpoint_operator AbGroup st G = H};
 coherence
  proof
    set D2 = the Objects of AbGroupCat(UN);
      now
      let x be set;
      assume x in {G where G is Element of D2
               : ex H being midpoint_operator AbGroup st G = H};
      then ex G being Element of D2 st
 x = G & ex H being midpoint_operator AbGroup st G = H;
      hence x in D2;end;
    hence thesis by TARSKI:def 3;
  end;
end;

definition let UN;
 cluster MidOpGroupObjects(UN) -> non empty;
 coherence
  proof
    set D2 = the Objects of AbGroupCat(UN);
    set D1 = {G where G is Element of D2
               : ex H being midpoint_operator AbGroup st G = H};
    set T = L_Trivial;
      D2 = AbGroupObjects(UN) by Th52;
    then T in D2 by Th51;
    then T in D1;
    then reconsider D1 as non empty set;
      now
      let x be set;
      assume x in D1;
      then ex G being Element of D2 st
 x = G & ex H being midpoint_operator AbGroup st G = H;
      hence x in D2;end;
    hence thesis by Def39;
  end;
end;

definition let UN;
 func MidOpGroupCat(UN) -> Subcategory of AbGroupCat(UN) equals
 :Def40: cat(MidOpGroupObjects(UN));
 coherence;
end;

definition let UN;
 cluster MidOpGroupCat(UN) -> strict;
 coherence
 proof
     MidOpGroupCat(UN) = cat(MidOpGroupObjects(UN)) by Def40;
   hence thesis;
 end;
end;

theorem
  the Objects of MidOpGroupCat(UN) = MidOpGroupObjects(UN)
 proof
     MidOpGroupCat(UN) = cat(MidOpGroupObjects(UN)) by Def40;
   hence thesis by Th10;
 end;

theorem
  L_Trivial in MidOpGroupObjects(UN)
 proof
    set D2 = the Objects of AbGroupCat(UN);
    set T = L_Trivial;
      D2 = AbGroupObjects(UN) by Th52;
    then T in D2 by Th51;
    then T in {G where G is Element of D2
               : ex H being midpoint_operator AbGroup st G = H};
    hence thesis by Def39;
 end;

Back to top