The abstract of the Mizar article:

Category of Rings

by

Michal Muzalewski

Received December 5, 1991

MML identifier: RINGCAT1

[ Mizar article, MML identifier index ]

environ

 vocabulary CLASSES2, VECTSP_1, PRE_TOPC, INCSP_1, FUNCT_1, CAT_1, FUNCSDOM,
      GRCAT_1, RELAT_1, MIDSP_1, ARYTM_3, ENS_1, FUNCT_2, RLVECT_1, MOD_2,
      TARSKI, PARTFUN1, RINGCAT1;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, MCART_1,
      PARTFUN1, FUNCT_2, STRUCT_0, PRE_TOPC, RLVECT_1, VECTSP_1, GRCAT_1,
      FUNCSDOM, CAT_1, CLASSES2, MOD_2;
 constructors ALGSTR_1, MOD_2, GRCAT_1, TOPS_2, VECTSP_2, MEMBERED, PARTFUN1,
      XBOOLE_0;
 clusters VECTSP_2, MOD_2, RELSET_1, STRUCT_0, GRCAT_1, 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;

               ::
               ::  1a. Maps of the carriers of rings
               ::

definition let G,H be non empty doubleLoopStr;
 let IT be map of G,H;
 canceled;

 attr IT is linear means
:: RINGCAT1:def 2
  (for x,y being Scalar of G holds IT.(x+y) = IT.x+IT.y)
        & (for x,y being Scalar of G holds IT.(x*y) = IT.x*IT.y)
        & IT.(1_ G) = 1_ H;
end;

canceled 2;

theorem :: RINGCAT1:3
for G1,G2,G3 being non empty doubleLoopStr,
        f being map of G1,G2, g being map of G2,G3
      st f is linear & g is linear holds g*f is linear;

                      ::
                      ::  1b. Morphisms of rings
                      ::

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

reserve f for RingMorphismStr;

definition let f;
 func dom(f) -> Ring equals
:: RINGCAT1:def 3
   the Dom of f;
 func cod(f) -> Ring equals
:: RINGCAT1:def 4
   the Cod of f;
 func fun(f) -> map of the Dom of f, the Cod of f equals
:: RINGCAT1:def 5
   the Fun of f;
end;

reserve G,H,G1,G2,G3,G4 for Ring;

definition let G be non empty doubleLoopStr;
  cluster id G -> linear;
end;

definition let IT be RingMorphismStr;
 attr IT is RingMorphism-like means
:: RINGCAT1:def 6
  fun(IT) is linear;
end;

definition
 cluster strict RingMorphism-like RingMorphismStr;
end;

definition
 mode RingMorphism is RingMorphism-like RingMorphismStr;
end;

definition let G;
 func ID G -> RingMorphism equals
:: RINGCAT1:def 7
   RingMorphismStr(# G,G,id G#);
end;

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

reserve F for RingMorphism;

definition let G,H;
 pred G <= H means
:: RINGCAT1:def 8
  ex F being RingMorphism st dom(F) = G & cod(F) = H;
 reflexivity;
end;

definition let G,H;
 assume  G <= H;
 mode Morphism of G,H -> strict RingMorphism means
:: RINGCAT1:def 9
  dom(it) = G & cod(it) = H;
end;

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

definition let G;
 redefine func ID G -> strict Morphism of G,G;
end;

canceled;

theorem :: RINGCAT1:5
for g,f being RingMorphism st dom(g) = cod(f) ex G1,G2,G3 st
        G1 <= G2 & G2 <= G3 &
       the RingMorphismStr of g is Morphism of G2,G3 &
       the RingMorphismStr of f is Morphism of G1,G2;

theorem :: RINGCAT1:6

for F being strict RingMorphism
 holds F is Morphism of dom(F),cod(F) & dom(F) <= cod(F);

theorem :: RINGCAT1:7
  for F being strict RingMorphism
 ex G,H st ex f being map of G,H st
          F is Morphism of G,H
        & F = RingMorphismStr(#G,H,f#)
        & f is linear;

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

theorem :: RINGCAT1:8
 G1 <= G2 & G2 <= G3 implies G1 <= G3;

theorem :: RINGCAT1:9
for G being Morphism of G2,G3, F being Morphism of G1,G2
      st G1 <= G2 & G2 <= G3 holds G*F is Morphism of G1,G3;

definition let G1,G2,G3; let G be Morphism of G2,G3, F be Morphism of G1,G2;
 assume  G1 <= G2 & G2 <= G3;
 func G*'F -> strict Morphism of G1,G3 equals
:: RINGCAT1:def 11
   G*F;
end;

theorem :: RINGCAT1:10
for f,g being strict RingMorphism st dom g = cod f holds
       ex G1,G2,G3 st ex f0 being map of G1,G2, g0 being map of G2,G3
          st f = RingMorphismStr(#G1,G2,f0#)
           & g = RingMorphismStr(#G2,G3,g0#)
           & g*f = RingMorphismStr(#G1,G3,g0*f0#);

 theorem :: RINGCAT1:11
 for f,g being strict RingMorphism st dom g = cod f holds
     dom(g*f) = dom f
   & cod (g*f) = cod g;

 theorem :: RINGCAT1:12
 for f being Morphism of G1,G2, g being Morphism of G2,G3,
          h being Morphism of G3,G4 st G1 <= G2 & G2 <= G3 & G3 <= G4
         holds h*(g*f) = (h*g)*f;

 theorem :: RINGCAT1:13
 for f,g,h being strict RingMorphism st dom h = cod g & dom g = cod f
        holds h*(g*f) = (h*g)*f;

 theorem :: RINGCAT1:14
  dom ID(G) = G
      & cod ID(G) = G
      & (for f being strict RingMorphism st cod f = G holds (ID G)*f = f)
      & (for g being strict RingMorphism st dom g = G holds g*(ID G) = g);

                        ::
                        ::  2. Domains of rings
                        ::

definition let IT be set;
 attr IT is Ring_DOMAIN-like means
:: RINGCAT1:def 12
 for x being Element of IT holds x is strict Ring;
end;

definition
 cluster Ring_DOMAIN-like non empty set;
end;

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

reserve V for Ring_DOMAIN;

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

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

definition let IT be set;
 attr IT is RingMorphism_DOMAIN-like means
:: RINGCAT1:def 13
  for x being set st x in IT holds x is strict RingMorphism;
end;

definition
 cluster RingMorphism_DOMAIN-like (non empty set);
end;

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

definition let M be RingMorphism_DOMAIN;
 redefine mode Element of M -> RingMorphism;
end;

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

canceled 2;

theorem :: RINGCAT1:17
for f being strict RingMorphism holds {f} is RingMorphism_DOMAIN;

definition let G,H;
 mode RingMorphism_DOMAIN of G,H -> RingMorphism_DOMAIN means
:: RINGCAT1:def 14
 for x being Element of it holds x is Morphism of G,H;
end;

theorem :: RINGCAT1:18
 D is RingMorphism_DOMAIN of G,H
  iff for x being Element of D holds x is Morphism of G,H;

theorem :: RINGCAT1:19
  for f being Morphism of G,H holds {f} is RingMorphism_DOMAIN of G,H;

definition let G,H;
 assume  G <= H;
 func Morphs(G,H) -> RingMorphism_DOMAIN of G,H means
:: RINGCAT1:def 15
  x in it iff x is Morphism of G,H;
end;

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

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

                     ::
                     ::  4a. Category of rings  - objects
                     ::

definition let x,y;
 pred GO x,y means
:: RINGCAT1:def 16
  ex x1,x2,x3,x4,x5,x6 being set st x = [[x1,x2,x3,x4],x5,x6] &
  ex G being strict Ring
    st y = G
    & x1 = the carrier of G
    & x2 = the add of G
    & x3 = comp G
    & x4 = the Zero of G
    & x5 = the mult of G
    & x6 = the unity of G;
end;

theorem :: RINGCAT1:20
for x,y1,y2 being set st GO x,y1 & GO x,y2 holds y1 = y2;

theorem :: RINGCAT1:21
 ex x st x in UN & GO x,Z3;

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

theorem :: RINGCAT1:22
 Z3 in RingObjects(UN);

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

theorem :: RINGCAT1:23
for x being Element of RingObjects(UN) holds x is strict Ring;

definition let UN;
  cluster RingObjects(UN) -> Ring_DOMAIN-like;
end;

      ::
      ::  4b. Category of rings  - morphisms
      ::

definition let V;
 func Morphs(V) -> RingMorphism_DOMAIN means
:: RINGCAT1:def 18

  x in it iff ex G,H being Element of V st G <= H & x is Morphism of G,H;
end;

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

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

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

definition let V;
 func dom(V) -> Function of Morphs(V),V means
:: RINGCAT1:def 20
 for f being Element of Morphs(V) holds it.f = dom(f);
 func cod(V) -> Function of Morphs(V),V means
:: RINGCAT1:def 21
 for f being Element of Morphs(V) holds it.f = cod(f);
 func ID(V) -> Function of V,Morphs(V) means
:: RINGCAT1:def 22
 for G being Element of V holds it.G = ID(G);
 end;

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

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

theorem :: RINGCAT1:25
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
:: RINGCAT1:def 23

 (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 rings
             ::

definition let UN;
 func RingCat(UN) -> CatStr equals
:: RINGCAT1:def 24
   CatStr(#RingObjects(UN),Morphs(RingObjects(UN)),
                   dom(RingObjects(UN)),cod(RingObjects(UN)),
                   comp(RingObjects(UN)),ID(RingObjects(UN))#);
end;

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

theorem :: RINGCAT1:26
 for f,g being Morphism of RingCat(UN) holds
        [g,f] in dom(the Comp of RingCat(UN)) iff dom g = cod f;

theorem :: RINGCAT1:27
 for f being (Morphism of RingCat(UN)),
           f' being Element of Morphs(RingObjects(UN)),
           b being Object of RingCat(UN),
           b' being Element of RingObjects(UN)
       holds f is strict Element of Morphs(RingObjects(UN))
           & f' is Morphism of RingCat(UN)
           & b is strict Element of RingObjects(UN)
           & b' is Object of RingCat(UN);

theorem :: RINGCAT1:28
 for b being Object of RingCat(UN),
           b' being Element of RingObjects(UN)
       st b = b' holds id b = ID(b');

 theorem :: RINGCAT1:29
 for f being Morphism of RingCat(UN)
for f' being Element of Morphs(RingObjects(UN))
       st f = f'
       holds dom f = dom f'
           & cod f = cod f';

 theorem :: RINGCAT1:30
 for f,g being (Morphism of RingCat(UN)),
           f',g' being Element of Morphs(RingObjects(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(RingObjects(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 RingCat(UN) -> Category-like;
end;