:: Rings and Modules - Part II
::  by Michal Muzalewski
::
:: Received October 18, 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, FUNCSDOM, VECTSP_1, CLASSES2, FUNCT_5, MCART_1,
      STRUCT_0, VECTSP_2, SUPINF_2, ALGSTR_0, SUBSET_1, ARYTM_3, RLVECT_1,
      RELAT_1, MESFUNC1, FUNCT_1, MSSUBFAM, GRCAT_1, GRAPH_1, CAT_1, MIDSP_1,
      ORDINAL1, CARD_1, ARYTM_1, BINOP_1, LATTICES, FUNCT_2, ZFMISC_1, MOD_2,
      UNIALG_1;
 notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, BINOP_1, PARTFUN1,
      ORDINAL1, NUMBERS, FUNCT_2, FUNCT_5, STRUCT_0, ALGSTR_0, RLVECT_1,
      GROUP_1, VECTSP_1, VECTSP_2, CLASSES2, GRCAT_1, FUNCT_3;
 constructors ENUMSET1, PARTFUN1, VECTSP_2, GRCAT_1, FUNCOP_1, ALGSTR_1,
      RELSET_1, CLASSES1, FUNCT_5;
 registrations XBOOLE_0, SUBSET_1, RELSET_1, FUNCT_2, STRUCT_0, VECTSP_1,
      ALGSTR_1, ALGSTR_0, CLASSES2, GRCAT_1;
 requirements SUBSET, BOOLE, NUMERALS;


begin

reserve D,D9 for non empty set;
reserve R for Ring;
reserve G,H,S for non empty ModuleStr over R;
reserve UN for Universe;

definition
  let R;

  func TrivialLMod(R) -> strict LeftMod of R equals
:: MOD_2:def 1
  ModuleStr (#{0},op2,op0,pr2(the carrier of R,{0})#);
end;

theorem :: MOD_2:1
  for x being Vector of TrivialLMod R holds x = 0.TrivialLMod R;

definition
  let R be non empty multMagma;
  let G,H be non empty ModuleStr over R;
  let f be Function of G,H;
  attr f is homogeneous means
:: MOD_2:def 2

  for a being Scalar of R, x being Vector of G holds f.(a*x) = a*f.x;
end;

theorem :: MOD_2:2
  for f being Function of G,H, g being Function of H,S st f is
  homogeneous & g is homogeneous holds g*f is homogeneous;

reserve R for Ring;
reserve G, H for LeftMod of R;

registration let R,G,H;
 cluster ZeroMap(G,H) -> homogeneous;
end;

::
::  Morphisms of Left Modules
::

reserve G1, G2, G3 for LeftMod of R;

definition
  let R;
  struct LModMorphismStr over R (# Dom,Cod -> LeftMod of R, Fun -> Function of
    the Dom, the Cod #);
end;

reserve f for LModMorphismStr over R;

definition
  let R,f;

  func dom(f) -> LeftMod of R equals
:: MOD_2:def 3
  the Dom of f;
  func cod(f) -> LeftMod of R equals
:: MOD_2:def 4
  the Cod of f;
end;

definition
  let R,f;
  func fun(f) -> Function of dom(f),cod(f) equals
:: MOD_2:def 5
  the Fun of f;
end;

theorem :: MOD_2:3
  for f0 being Function of G1,G2 st f = LModMorphismStr(#G1,G2,f0#)
  holds dom f = G1 & cod f = G2 & fun f = f0;

definition
  let R,G,H;
  func ZERO(G,H) -> strict LModMorphismStr over R equals
:: MOD_2:def 6
  LModMorphismStr(# G,H,ZeroMap(G,H)#);
end;

definition
  let R;
  let IT be LModMorphismStr over R;
  attr IT is LModMorphism-like means
:: MOD_2:def 7

  fun(IT) is additive homogeneous;
end;

registration
  let R;
  cluster strict LModMorphism-like for LModMorphismStr over R;
end;

definition
  let R;
  mode LModMorphism of R is LModMorphism-like LModMorphismStr over R;
end;

theorem :: MOD_2:4
  for F being LModMorphism of R holds the Fun of F is additive homogeneous;

registration
  let R,G,H;
  cluster ZERO(G,H) -> LModMorphism-like;
end;

definition
  let R,G,H;
  mode Morphism of G,H -> LModMorphism of R means
:: MOD_2:def 8

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

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

theorem :: MOD_2:5
  for f being LModMorphismStr over R holds dom(f) = G & cod(f) = H
  & fun(f) is additive homogeneous implies f is Morphism of G,H;

theorem :: MOD_2:6
  for f being Function of G,H st f is additive homogeneous
   holds LModMorphismStr
  (#G,H,f#) is strict Morphism of G,H;

registration let R,G;
 cluster id G -> homogeneous;
end;

definition
  let R,G;
  func ID G -> strict Morphism of G,G equals
:: MOD_2:def 9
  LModMorphismStr(# G,G,id G#);
end;

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

theorem :: MOD_2:7
  for F being Morphism of G,H ex f being Function of G,H st the
  LModMorphismStr of F = LModMorphismStr(#G,H,f#) & f is additive homogeneous;

theorem :: MOD_2:8
  for F being strict Morphism of G,H ex f being Function of G,H st
  F = LModMorphismStr(#G,H,f#);

theorem :: MOD_2:9
  for F being LModMorphism of R ex G,H st F is Morphism of G,H;

theorem :: MOD_2:10
  for F being strict LModMorphism of R ex G,H being LeftMod of R, f
being Function of G,H st F is strict Morphism of G,H & F = LModMorphismStr(#G,H
    ,f#) & f is additive homogeneous;

theorem :: MOD_2:11
  for g,f being LModMorphism of R st dom(g) = cod(f) ex G1,G2,G3
  st g is Morphism of G2,G3 & f is Morphism of G1,G2;

definition
  let R;
  let G,F be LModMorphism of R;
  assume
 dom(G) = cod(F);
  func G*F -> strict LModMorphism of R means
:: MOD_2:def 10

  for G1,G2,G3 being
  LeftMod of R, g being Function of G2,G3, f being Function of G1,G2 st the
LModMorphismStr of G = LModMorphismStr(#G2,G3,g#) & the LModMorphismStr of F =
  LModMorphismStr(#G1,G2,f#) holds it = LModMorphismStr(#G1,G3,g*f#);
end;

theorem :: MOD_2:12
  for G being Morphism of G2,G3, F being Morphism of G1,G2 holds G
  *F is strict Morphism of G1,G3;

definition
  let R,G1,G2,G3;
  let G be Morphism of G2,G3;
  let F be Morphism of G1,G2;
  func G*'F -> strict Morphism of G1,G3 equals
:: MOD_2:def 11
  G*F;
end;

theorem :: MOD_2:13
  for G being Morphism of G2,G3, F being Morphism of G1,G2, g
being Function of G2,G3, f being Function of G1,G2 st G = LModMorphismStr(#G2,
G3,g#) & F = LModMorphismStr(#G1,G2,f#) holds G*'F = LModMorphismStr(#G1,G3,g*f
  #) & G*F = LModMorphismStr(# G1,G3,g*f#);

theorem :: MOD_2:14
  for f,g being strict LModMorphism of R st dom g = cod f holds ex
  G1,G2,G3 being LeftMod of R, f0 being Function of G1,G2, g0 being Function of
G2,G3 st f = LModMorphismStr(#G1,G2,f0#) & g = LModMorphismStr(#G2,G3,g0#) & g*
  f = LModMorphismStr(#G1,G3,g0*f0#);

theorem :: MOD_2:15
  for f,g being strict LModMorphism of R st dom g = cod f holds dom(g*f)
  = dom f & cod (g*f) = cod g;

theorem :: MOD_2:16
  for G1,G2,G3,G4 being LeftMod of R, 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 :: MOD_2:17
  for f,g,h being strict LModMorphism of R st dom h = cod g & dom g =
  cod f holds h*(g*f) = (h*g)*f;

theorem :: MOD_2:18
  dom ID(G) = G & cod ID(G) = G & (for f being strict LModMorphism of R
st cod f = G holds (ID G)*f = f) & for g being strict LModMorphism of R st dom
  g = G holds g*(ID G) = g;

theorem :: MOD_2:19
  for u,v,w being Element of UN holds {u,v,w} is Element of UN;

theorem :: MOD_2:20
  for u being Element of UN holds succ u is Element of UN;

theorem :: MOD_2:21
  0 is Element of UN & 1 is Element of UN & 2 is Element of UN;

reserve a,b,c for Element of {0,1,2};

definition
  let a;
  func -a -> Element of {0,1,2} equals
:: MOD_2:def 12

  0 if a = 0, 2 if a = 1, 1 if a
  = 2;
  let b;
  func a+b -> Element of {0,1,2} equals
:: MOD_2:def 13

  b if a = 0, a if b = 0, 2 if a
  = 1 & b = 1, 0 if a = 1 & b = 2, 0 if a = 2 & b = 1, 1 if a = 2 & b = 2;
  func a*b -> Element of {0,1,2} equals
:: MOD_2:def 14

  0 if b = 0, 0 if a = 0, a if b
  = 1, b if a = 1, 1 if a = 2 & b = 2;
end;

definition
  func add3 -> BinOp of {0,1,2} means
:: MOD_2:def 15

  it.(a,b) = a+b;
  func mult3 -> BinOp of {0,1,2} means
:: MOD_2:def 16

  it.(a,b) = a*b;
  func compl3 -> UnOp of {0,1,2} means
:: MOD_2:def 17

  it.a = -a;
  func unit3 -> Element of {0,1,2} equals
:: MOD_2:def 18
  1;
  func zero3 -> Element of {0,1,2} equals
:: MOD_2:def 19
  0;
end;

definition
  func Z_3 -> strict doubleLoopStr equals
:: MOD_2:def 20

  doubleLoopStr (#{0,1,2},add3,mult3,unit3,zero3#);
end;

registration
  cluster Z_3 -> non empty;
end;

registration
  cluster Z_3 -> well-unital;
end;

theorem :: MOD_2:22
  0.Z_3 = 0 & 1.Z_3 = 1 & 0.Z_3 is Element of {0,1,2} & 1.Z_3 is
  Element of {0,1,2} & the addF of Z_3 = add3 & the multF of Z_3 = mult3;

registration
  cluster Z_3 -> add-associative right_zeroed right_complementable;
end;

theorem :: MOD_2:23
  for x,y being Scalar of Z_3, X,Y being Element of {0,1,2} st X=x
  & Y=y holds x+y = X+Y & x*y = X*Y & -x = -X;

theorem :: MOD_2:24
  for x,y,z being Scalar of Z_3, X,Y,Z being Element of {0,1,2} st
X=x & Y=y & Z=z holds (x+y)+z = (X+Y)+Z & x+(y+z) = X+(Y+Z) & (x*y)*z = (X*Y)*Z
  & x*(y*z) = X*(Y*Z);

theorem :: MOD_2:25
  for x,y,z,a,b being Element of {0,1,2} st a = 0 & b = 1 holds x+
y = y+x & (x+y)+z = x+(y+z) & x+a = x & x+(-x) = a & x*y = y*x & (x*y)*z = x*(y
*z) & b*x = x & (x<>a implies ex y be Element of {0,1,2} st x*y = b) & a <> b &
  x*(y+z) = x*y+x*z;

theorem :: MOD_2:26
  for F being non empty doubleLoopStr st for x,y,z being Scalar of
F holds x+y = y+x & (x+y)+z = x+(y+z) & x+(0.F) = x & x+(-x) = (0.F) & x*y = y*
  x & (x*y)*z = x*(y*z) & 1.F*x = x & x*(1.F) = x & (x<>(0.F) implies ex y be
  Scalar of F st x*y = 1.F) & 0.F <> 1.F & x*(y+z) = x*y+x*z holds F is Field;

theorem :: MOD_2:27
  Z_3 is Fanoian Field;

registration
  cluster Z_3 -> Fanoian add-associative right_zeroed right_complementable
Abelian commutative associative well-unital distributive almost_left_invertible
  ;
end;

theorem :: MOD_2:28
  for f being Function of D,D9 st D in UN & D9 in UN holds f in UN;

theorem :: MOD_2:29
  the carrier of Z_3 in UN & the addF of Z_3 in UN & comp Z_3 in UN &
0.Z_3
  in UN & the multF of Z_3 in UN & 1.Z_3 in UN;