Journal of Formalized Mathematics
Volume 3, 1991
University of Bialystok
Copyright (c) 1991 Association of Mizar Users

### Rings and Modules --- Part II

by
Michal Muzalewski

MML identifier: MOD_2
[ Mizar article, MML identifier index ]

```environ

vocabulary FUNCSDOM, VECTSP_1, CLASSES2, GRCAT_1, RLVECT_1, BOOLE, MIDSP_1,
VECTSP_2, FUNCT_3, FUNCT_1, PRE_TOPC, INCSP_1, ORDINAL4, CAT_1, RELAT_1,
ARYTM_3, ORDINAL1, ARYTM_1, BINOP_1, LATTICES, FUNCT_2, MOD_2, ALGSTR_1;
notation TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, BINOP_1, FUNCT_2,
STRUCT_0, ORDINAL1, RLVECT_1, VECTSP_1, FUNCSDOM, VECTSP_2, CLASSES2,
PRE_TOPC, ALGSTR_1, MIDSP_1, GRCAT_1, FUNCT_3;
constructors ENUMSET1, BINOP_1, VECTSP_2, GRCAT_1, TOPS_2, ALGSTR_1, MIDSP_1,
MEMBERED, PARTFUN1, XBOOLE_0;
clusters VECTSP_1, STRUCT_0, RELSET_1, SUBSET_1, ALGSTR_1, MEMBERED, ZFMISC_1,
XBOOLE_0;
requirements SUBSET, BOOLE;

begin

reserve x,y,z for set;
reserve D,D' for non empty set;
reserve R for Ring;
reserve G,H,S for non empty VectSpStr over R;

reserve UN for Universe;

definition let R;
canceled;

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

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

definition let R be non empty doubleLoopStr;
let G,H be non empty VectSpStr over R; let f be map of G,H;
canceled 2;

attr f is linear means
:: MOD_2:def 5
(for x,y being Vector of G holds f.(x+y) = f.x+f.y)
& for a being Scalar of R, x being Vector of G holds f.(a*x) = a*f.x;
end;

canceled 2;

theorem :: MOD_2:4
for f being map of G,H st f is linear holds f is additive;

canceled;

theorem :: MOD_2:6
for f being map of G,H, g being map of H,S
st f is linear & g is linear holds g*f is linear;

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

canceled;

theorem :: MOD_2:8
ZeroMap(G,H) is linear;

::
::  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 -> map 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 6
the Dom of f;
func cod(f) -> LeftMod of R equals
:: MOD_2:def 7
the Cod of f;
end;

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

theorem :: MOD_2:9
for f0 being map 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 9
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 10
fun(IT) is linear;
end;

definition let R;
cluster strict LModMorphism-like LModMorphismStr over R;
end;

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

theorem :: MOD_2:10
for F being LModMorphism of R holds the Fun of F is linear;

definition 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 11
dom(it) = G & cod(it) = H;
end;

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

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

theorem :: MOD_2:12
for f being map of G,H st f is linear
holds LModMorphismStr (#G,H,f#) is strict Morphism of G,H;

theorem :: MOD_2:13
id G is linear;

definition let R,G;
func ID G -> strict Morphism of G,G equals
:: MOD_2:def 12
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:14
for F being Morphism of G,H ex f being map of G,H
st the LModMorphismStr of F = LModMorphismStr(#G,H,f#) & f is linear;

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

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

theorem :: MOD_2:17
for F being strict LModMorphism of R
ex G,H being LeftMod of R, f being map of G,H
st F is strict Morphism of G,H
& F = LModMorphismStr(#G,H,f#)
& f is linear;

theorem :: MOD_2:18
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 13
for G1,G2,G3 being LeftMod of R,
g being map of G2,G3, f being map 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;

canceled;

theorem :: MOD_2:20
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 14
G*F;
end;

theorem :: MOD_2:21
for 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 = 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:22
for f,g being strict LModMorphism of R st dom g = cod f holds
ex G1,G2,G3 being LeftMod of R,
f0 being map of G1,G2, g0 being map of G2,G3
st f = LModMorphismStr(#G1,G2,f0#)
& g = LModMorphismStr(#G2,G3,g0#)
& g*f = LModMorphismStr(#G1,G3,g0*f0#);

theorem :: MOD_2:23
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:24
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:25
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:26
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);

definition let x,y,z;
cluster {x,y,z} -> non empty;
end;

canceled;

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

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

theorem :: MOD_2:30
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 15
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 16
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 17
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 18
it.(a,b) = a+b;
func mult3 -> BinOp of {0,1,2} means
:: MOD_2:def 19
it.(a,b) = a*b;
func compl3 -> UnOp of {0,1,2} means
:: MOD_2:def 20
it.a = -a;
func unit3 -> Element of {0,1,2} equals
:: MOD_2:def 21
1;
func zero3 -> Element of {0,1,2} equals
:: MOD_2:def 22
0;
end;

definition
func Z3 -> strict doubleLoopStr equals
:: MOD_2:def 23
end;

definition
cluster Z3 -> non empty;
end;

canceled;

theorem :: MOD_2:32
0.Z3 = 0
& 1_ Z3 = 1
& 0.Z3 is Element of {0,1,2}
& 1_ Z3 is Element of {0,1,2}
& the mult of Z3 = mult3;

definition
cluster Z3 -> add-associative right_zeroed right_complementable;
end;

theorem :: MOD_2:33
for x,y being Scalar of Z3, 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:34
for x,y,z being Scalar of Z3, 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:35
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:36
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<>(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:37
Z3 is Fanoian Field;

definition
cluster Z3 -> Fanoian add-associative right_zeroed right_complementable
Abelian commutative associative left_unital distributive Field-like;
end;

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

canceled;

theorem :: MOD_2:40
the carrier of Z3 in UN & the add of Z3 is Element of UN &
comp Z3 is Element of UN & the Zero of Z3 is Element of UN &
the mult of Z3 is Element of UN & the unity of Z3 is Element of UN;
```