:: Rings and Modules - Part II
:: by Michal Muzalewski
::
:: Received October 18, 1991
:: Copyright (c) 1991-2019 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;