The abstract of the Mizar article:

Category of Left Modules

by

Michal Muzalewski

Received December 12, 1991

MML identifier: MODCAT_1

[ Mizar article, MML identifier index ]

environ

 vocabulary CLASSES2, FUNCSDOM, VECTSP_2, MOD_2, CAT_1, MIDSP_1, GRCAT_1,
      ENS_1, INCSP_1, ORDINAL4, FUNCT_2, RELAT_1, PRE_TOPC, VECTSP_1, BOOLE,
      FUNCT_3, FUNCT_1, TARSKI, ARYTM_3, PARTFUN1, MODCAT_1, RLVECT_1,
      ALGSTR_1;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, STRUCT_0, RELAT_1, FUNCT_1,
      FUNCT_2, PARTFUN1, RLVECT_1, VECTSP_1, FUNCSDOM, VECTSP_2, CAT_1,
      FRAENKEL, CLASSES2, PRE_TOPC, ALGSTR_1, GRCAT_1, MOD_2, FUNCT_3, MIDSP_1;
 constructors GRCAT_1, MOD_2, MIDSP_1, VECTSP_2, ALGSTR_1, MEMBERED, XBOOLE_0;
 clusters VECTSP_2, CAT_1, GRCAT_1, MOD_2, RELSET_1, STRUCT_0, SUBSET_1,
      MEMBERED, ZFMISC_1, XBOOLE_0;
 requirements SUBSET, BOOLE;


begin

reserve x,y for set;
reserve D for non empty set;
reserve UN for Universe;
reserve R for Ring;
reserve G,H for LeftMod of R;

      ::
      ::  2. Domains of left modules
      ::

definition let R;
 mode LeftMod_DOMAIN of R -> non empty set means
:: MODCAT_1:def 1
  for x being Element of it holds x is strict LeftMod of R;
end;

reserve V for LeftMod_DOMAIN of R;

definition let R,V;
 redefine mode Element of V -> LeftMod of R;
end;

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

definition let R;
 mode LModMorphism_DOMAIN of R -> non empty set means
:: MODCAT_1:def 2
   for x being Element of it holds x is strict LModMorphism of R;
end;

definition let R; let M be LModMorphism_DOMAIN of R;
 redefine mode Element of M -> LModMorphism of R;
end;

definition let R; let M be LModMorphism_DOMAIN of R;
 cluster strict Element of M;
end;

canceled 2;

theorem :: MODCAT_1:3
 for f being strict LModMorphism of R
        holds {f} is LModMorphism_DOMAIN of R;

definition let R,G,H;
 mode LModMorphism_DOMAIN of G,H -> LModMorphism_DOMAIN of R means
:: MODCAT_1:def 3
  for x being Element of it holds x is strict Morphism of G,H;
end;

theorem :: MODCAT_1:4
 D is LModMorphism_DOMAIN of G,H
       iff for x being Element of D holds x is strict Morphism of G,H;

theorem :: MODCAT_1:5
  for f being strict Morphism of G,H holds {f} is LModMorphism_DOMAIN of G,H;

definition let R,G,H;
 func Morphs(G,H) -> LModMorphism_DOMAIN of G,H means
:: MODCAT_1:def 4
  x in it iff x is strict Morphism of G,H;
end;

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

      ::
      ::  4a. Category of left modules - objects
      ::

definition let x,y,R;
 pred GO x,y,R means
:: MODCAT_1:def 5
  ex x1,x2 being set st x = [x1,x2] &
    ex G being strict LeftMod of R st y = G
    & x1 = the LoopStr of G
    & x2 = the lmult of G;
end;

theorem :: MODCAT_1:6
 for x,y1,y2 being set st GO x,y1,R & GO x,y2,R holds y1 = y2;

theorem :: MODCAT_1:7
 for UN ex x st x in {[G,f] where G is Element of GroupObjects(UN),
   f is Element of Funcs([:the carrier of R,{{}}:],{{}}) : not contradiction}
      & GO x,TrivialLMod(R),R;

definition let UN,R;
 func LModObjects(UN,R) -> set means
:: MODCAT_1:def 6
  for y holds y in it iff ex x st
    x in {[G,f] where G is Element of GroupObjects(UN),
     f is Element of Funcs([:the carrier of R,{{}}:],{{}}) : not contradiction}
  & GO x,y,R;
end;

theorem :: MODCAT_1:8
TrivialLMod(R) in LModObjects(UN,R);

definition let UN,R;
 cluster LModObjects(UN,R) -> non empty;
end;

theorem :: MODCAT_1:9
 for x being Element of LModObjects(UN,R)
        holds x is strict LeftMod of R;

definition let UN,R;
  redefine func LModObjects(UN,R) -> LeftMod_DOMAIN of R;
end;

      ::
      ::  4b. Category of left modules - morphisms
      ::

definition let R,V;
 func Morphs(V) -> LModMorphism_DOMAIN of R means
:: MODCAT_1:def 7
  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 left modules - dom,cod,id
      ::


definition let R,V; let F be Element of Morphs(V);
 func dom'(F) -> Element of V equals
:: MODCAT_1:def 8
   dom(F);
 func cod'(F) -> Element of V equals
:: MODCAT_1:def 9
   cod(F);
end;

definition let R,V; let G be Element of V;
 func ID(G) -> strict Element of Morphs(V) equals
:: MODCAT_1:def 10
   ID(G);
end;

definition let R,V;
 func dom(V) -> Function of Morphs(V),V means
:: MODCAT_1:def 11
  for f being Element of Morphs(V) holds it.f = dom'(f);
 func cod(V) -> Function of Morphs(V),V means
:: MODCAT_1:def 12
  for f being Element of Morphs(V) holds it.f = cod'(f);
 func ID(V) -> Function of V,Morphs(V) means
:: MODCAT_1:def 13
  for G being Element of V holds it.G = ID(G);
 end;

      ::
      ::  4d. Category of left modules - superposition
      ::

theorem :: MODCAT_1:10
 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 :: MODCAT_1:11
 for g,f being Element of Morphs(V) st dom'(g) = cod'(f)
      holds g*f in Morphs(V);

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

definition let R,V;
 func comp(V) -> PartFunc of [:Morphs(V),Morphs(V):],Morphs(V) means
:: MODCAT_1:def 14

   (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;

theorem :: MODCAT_1:13
 for g,f being Element of Morphs(V) holds
       [g,f] in dom comp(V) iff dom(g) = cod(f);

      ::
      ::  4e. Definition of Category of left modules
      ::

definition let UN,R;
 func LModCat(UN,R) -> strict CatStr equals
:: MODCAT_1:def 15
   CatStr(#LModObjects(UN,R),Morphs(LModObjects(UN,R)),
                   dom(LModObjects(UN,R)),cod(LModObjects(UN,R)),
                   comp(LModObjects(UN,R)),ID(LModObjects(UN,R))#);
end;

theorem :: MODCAT_1:14
  for f,g being Morphism of LModCat(UN,R) holds
        [g,f] in dom(the Comp of LModCat(UN,R)) iff dom g = cod f;

theorem :: MODCAT_1:15
  for f  being (Morphism of LModCat(UN,R)),
           f' being Element of Morphs(LModObjects(UN,R)),
           b  being Object of LModCat(UN,R),
           b' being Element of LModObjects(UN,R)
       holds f is strict Element of Morphs(LModObjects(UN,R))
           & f' is Morphism of LModCat(UN,R)
           & b is strict Element of LModObjects(UN,R)
           & b' is Object of LModCat(UN,R);

theorem :: MODCAT_1:16
  for b  being Object of LModCat(UN,R),
           b' being Element of LModObjects(UN,R)
       st b = b' holds id b = ID(b');

 theorem :: MODCAT_1:17
  for f  being Morphism of LModCat(UN,R)
       for f' being Element of Morphs(LModObjects(UN,R))
       st f = f'
       holds dom f = dom f'
           & cod f = cod f';

 theorem :: MODCAT_1:18
  for f,g   being (Morphism of LModCat(UN,R)),
           f',g' being Element of Morphs(LModObjects(UN,R))
       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(LModObjects(UN,R)))
           & (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,R;
 cluster LModCat(UN,R) -> Category-like;
end;