:: Category of Rings
::  by Micha{\l} Muzalewski
::
:: Received December 5, 1991
:: Copyright (c) 1991-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies XBOOLE_0, CLASSES2, ALGSTR_0, FUNCT_1, FDIFF_1, MSSUBFAM,
      GROUP_1, RELAT_1, VECTSP_1, ARYTM_3, MOD_2, FUNCSDOM, GRCAT_1, GRAPH_1,
      STRUCT_0, MIDSP_1, XXREAL_0, CAT_1, SUBSET_1, ENS_1, SUPINF_2, MESFUNC1,
      TARSKI, PARTFUN1, ZFMISC_1, RINGCAT1, MONOID_0, RELAT_2, BINOP_1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, MCART_1, RELSET_1,
      PARTFUN1, FUNCT_2, BINOP_1, STRUCT_0, ALGSTR_0, GROUP_1, VECTSP_1,
      GRCAT_1, GRAPH_1, CAT_1, CLASSES2, MOD_2, GROUP_6;
 constructors GRCAT_1, GROUP_6, MOD_2, RELSET_1, XTUPLE_0;
 registrations XBOOLE_0, RELSET_1, FUNCT_2, STRUCT_0, GRCAT_1, MOD_2, VECTSP_1;
 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 Function of G,H;
  attr IT is linear means
:: RINGCAT1:def 1
  IT is additive multiplicative unity-preserving;
end;

registration
  let G,H be non empty doubleLoopStr;
  cluster linear -> additive multiplicative unity-preserving
   for Function of G,H;
  cluster additive multiplicative unity-preserving -> linear
    for Function of G,H;
end;

theorem :: RINGCAT1:1
  for G1,G2,G3 being non empty doubleLoopStr, f being Function of
  G1,G2, g being Function 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 -> Function of the Dom, the
    Cod #);
end;

reserve f for RingMorphismStr;

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

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

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

definition
  let IT be RingMorphismStr;
  attr IT is RingMorphism-like means
:: RINGCAT1:def 5

  fun(IT) is linear;
end;

registration
  cluster strict RingMorphism-like for RingMorphismStr;
end;

definition
  mode RingMorphism is RingMorphism-like RingMorphismStr;
end;

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

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

reserve F for RingMorphism;

definition
  let G,H;
  pred G <= H means
:: RINGCAT1:def 7

  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 8

    dom(it) = G & cod( it) = H;
end;

registration
  let G,H;
  cluster strict for Morphism of G,H;
end;

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

theorem :: RINGCAT1:2
  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:3
  for F being strict RingMorphism holds F is Morphism of dom(F),cod
  (F) & dom(F) <= cod(F);

theorem :: RINGCAT1:4
  for F being strict RingMorphism ex G,H st ex f being Function 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 9

  for G1,G2,G3 for g being
  Function of G2,G3, f being Function 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:5
  G1 <= G2 & G2 <= G3 implies G1 <= G3;

theorem :: RINGCAT1:6
  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 10

  G*F;
end;

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

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

theorem :: RINGCAT1:9
  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:10
  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:11
  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 11

  for x being Element of IT holds x is strict Ring;
end;

registration
  cluster Ring_DOMAIN-like non empty for 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;

registration
  let V;
  cluster strict for Element of V;
end;

definition
  let IT be set;
  attr IT is RingMorphism_DOMAIN-like means
:: RINGCAT1:def 12

  for x being object st x in IT holds x is strict RingMorphism;
end;

registration
  cluster RingMorphism_DOMAIN-like for 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;

registration
  let M be RingMorphism_DOMAIN;
  cluster strict for Element of M;
end;

theorem :: RINGCAT1:12
  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 13

 for x being Element of it holds x is Morphism of G,H;
end;

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

theorem :: RINGCAT1:14
  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 14

  for x being object holds 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;

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

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

definition
  let x,y be object;
  pred GO x,y means
:: RINGCAT1:def 15

  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
  addF of G & x3 = comp G & x4 = 0.G & x5 = the multF of G & x6 = 1.G;
end;

theorem :: RINGCAT1:15
  for x,y1,y2 being object st GO x,y1 & GO x,y2 holds y1 = y2;

theorem :: RINGCAT1:16
  ex x being object st x in UN & GO x,Z_3;

definition
  let UN;
  func RingObjects(UN) -> set means
:: RINGCAT1:def 16

for y being object holds y in it iff ex x st x in UN & GO x,y;
end;

theorem :: RINGCAT1:17
  Z_3 in RingObjects(UN);

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

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

registration
  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 17

  for x being object holds
   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;
  redefine 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 18
   ID(G);
::$CD
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);
::$CD
end;

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

theorem :: RINGCAT1:19
  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:20
  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#);
end;

registration
  let UN;
  cluster RingCat(UN) -> strict non void non empty;
end;

theorem :: RINGCAT1:21
  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:22
  for f being (Morphism of RingCat(UN)), f9 being Element of
  Morphs(RingObjects(UN)), b being Object of RingCat(UN), b9 being Element of
  RingObjects(UN) holds f is strict Element of Morphs(RingObjects(UN)) & f9 is
Morphism of RingCat(UN) & b is strict Element of RingObjects(UN) & b9 is Object
  of RingCat(UN);

::$CT

theorem :: RINGCAT1:24
  for f,g being (Morphism of RingCat(UN)), f9,g9 being Element of
  Morphs(RingObjects(UN)) st f = f9 & g = g9 holds (dom g = cod f iff dom g9 =
  cod f9) & (dom g = cod f iff [g9,f9] in dom comp(RingObjects(UN))) & (dom g =
cod f implies g(*)f = g9*f9) & (dom f = dom g iff dom f9 = dom g9) &
(cod f = cod
  g iff cod f9 = cod g9);

registration
  let UN;
  cluster RingCat(UN) -> Category-like
     transitive associative reflexive;
end;

registration
  let UN;
  cluster RingCat(UN) -> with_identities;
end;

theorem :: RINGCAT1:25
  for a being Object of RingCat(UN), aa being Element of
  RingObjects(UN) st a = aa holds id a = ID aa;