:: Ring of {E}ndomorphisms \& {M}odules over a {R}ing
:: by Yasushige Watase
::
:: Received September 30, 2022
:: Copyright (c) 2022-2026 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 FUNCSDOM, VECTSP_1, STRUCT_0, XBOOLE_0, VECTSP_2, SUBSET_1,
FUNCT_1, RELAT_1, FUNCT_2, FUNCOP_1, UNIALG_1, GRCAT_1, ARYTM_3, GROUP_6,
ALGSTR_0, RLVECT_1, MSSUBFAM, RMOD_2, SUPINF_2, BINOP_1, ZFMISC_1,
PARTFUN1, ARYTM_1, MESFUNC1, LMOD_7, GROUP_1, PRALG_1, MOD_4, LATTICES,
QUOFIELD, REALSET1, FUNCT_5, FDIFF_1, CAT_4, FIB_NUM, CAT_1, CONLAT_1,
VECTSP10, ALTCAT_1, NATTRA_1, LMOD_XX1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, RELSET_1, FUNCT_1,
PARTFUN1, FUNCT_2, BINOP_1, DOMAIN_1, FUNCT_3, FUNCOP_1, REALSET1,
FUNCT_5, STRUCT_0, ALGSTR_0, RLVECT_1, GROUP_1, VECTSP_1, FUNCSDOM,
VECTSP_2, GRCAT_1, MOD_2, GROUP_6, RINGCAT1, MOD_4, VECTSP10, QUOFIELD,
ZMODUL01;
constructors RELSET_1, REALSET1, FUNCT_5, VECTSP_2, GRCAT_1, RINGCAT1,
MODCAT_1, RING_2;
registrations STRUCT_0, RELSET_1, SUBSET_1, GRCAT_1, MOD_2, FUNCT_2, FUNCOP_1,
VECTSP_1, VECTSP_2, ALGSTR_0, FUNCT_1;
requirements SUBSET, BOOLE;
definitions ALGSTR_0;
equalities XBOOLE_0, ALGSTR_0, STRUCT_0, BINOP_1, FUNCOP_1, VECTSP_1,
REALSET1, VECTSP10, VECTSP_2;
expansions STRUCT_0, VECTSP_1, RLVECT_1, BINOP_1, FUNCT_2, GROUP_1, ALGSTR_0,
MOD_2, FUNCT_1, RINGCAT1;
theorems TARSKI, FUNCT_2, VECTSP_1, VECTSP_4, RELAT_1, GRCAT_1, FUNCT_1,
FUNCOP_1, RLVECT_1, ALGSTR_1, ZFMISC_1, FUNCT_3, MOD_2, ALGSTR_0,
GROUP_6, LOPBAN_8, XBOOLE_1;
schemes BINOP_1, FUNCT_1, FUNCT_2;
begin :: Construct the ring of Endomorphism of Abelian group M
definition
let M,N be AbGroup;
func ADD(M,N) -> BinOp of Funcs(the carrier of M,the carrier of N)
means :Def1:
for f,g being Element of Funcs(the carrier of M,the carrier of N) holds
it.(f,g) = (the addF of N).:(f,g);
existence
proof
deffunc F(Element of Funcs(the carrier of M,the carrier of N),
Element of Funcs(the carrier of M,the carrier of N))
= (the addF of N).:($1,$2);
consider F1 being BinOp of Funcs(the carrier of M,the carrier of N)
such that
A1: for x,y being Element of Funcs(the carrier of M,the carrier of N)
holds F1.(x,y) = F(x,y) from BINOP_1:sch 4;
take F1;
let f,g be Element of Funcs(the carrier of M,the carrier of N);
thus thesis by A1;
end;
uniqueness
proof
let it1,it2 be BinOp of Funcs(the carrier of M,the carrier of N) such that
A2: for f,g being Element of Funcs(the carrier of M,the carrier of N) holds
it1.(f,g) = (the addF of N).:(f,g) and
A3: for f,g being Element of Funcs(the carrier of M,the carrier of N) holds
it2.(f,g) = (the addF of N).:(f,g);
now
let f,g be Element of Funcs(the carrier of M,the carrier of N);
thus it1.(f,g) = (the addF of N).:(f,g) by A2 .= it2.(f,g) by A3;
end;
hence thesis;
end;
end;
Lm1:
for M,N be AbGroup for x being Element of M,
f being Function of M, N holds x in dom f
proof
let M,N be AbGroup;
let x be Element of M,
f be Function of M,N;
x in the carrier of M;
hence thesis by FUNCT_2:def 1;
end;
theorem Th1:
for M,N be AbGroup,
f,g,h be Element of Funcs(the carrier of M, the carrier of N) holds
h = ADD(M,N).(f,g) iff
for x being Element of the carrier of M holds h.x = f.x + g.x
proof
let M,N be AbGroup,
f,g,h be Element of Funcs(the carrier of M, the carrier of N);
hereby
assume
A1: h = ADD(M,N).(f,g);
let x be Element of the carrier of M;
A2: x in dom ((the addF of N).:(f,g)) by Lm1;
thus h.x = ((the addF of N).:(f,g)).x by A1,Def1
.= f.x + g.x by A2,FUNCOP_1:22;
end;
assume
A3: for x being Element of M holds h.x = f.x + g.x;
now
let x be Element of M;
A4: x in dom ((the addF of N).:(f,g)) by Lm1;
thus (ADD(M,N).(f,g)).x = ((the addF of N).:(f,g)).x by Def1
.= f.x + g.x by A4,FUNCOP_1:22 .= h.x by A3;
end;
hence h = (ADD(M,N)).(f,g);
end;
Lm2:
for M,N be AbGroup
for f,g, h be Element of Funcs(the carrier of M, the carrier of N) holds
(ADD(M,N)).(f,(ADD(M,N)).(g,h)) = (ADD(M,N)).((ADD(M,N)).(f,g),h)
proof
let M,N be AbGroup;
let f,g,h be Element of Funcs(the carrier of M, the carrier of N);
set M1 = the carrier of M, N1 = the carrier of N;
reconsider fg=(ADD(M,N)).(f,g), gh=(ADD(M,N)).(g,h) as Element of Funcs(M1,N1);
set F1 = (ADD(M,N)).(f,gh);
set F2 = (ADD(M,N)).(fg,h);
for x being Element of M holds F1.x = F2.x
proof
let x be Element of M;
A1: gh.x = g.x + h.x by Th1;
A2: fg.x = f.x + g.x by Th1;
F1.x = f.x + (g.x + h.x) by A1,Th1 .= fg.x + h.x by A2,RLVECT_1:def 3
.= F2.x by Th1;
hence thesis;
end;
hence thesis;
end;
theorem Th2:
for M,N be AbGroup
for f,g be Homomorphism of M,N holds ADD(M,N).(f,g) is Homomorphism of M,N
proof
let M,N be AbGroup;
let f,g be Homomorphism of M,N;
reconsider f,g
as Element of Funcs(the carrier of M, the carrier of N) by FUNCT_2:8;
reconsider F = ADD(M,N).(f,g)
as Element of Funcs(the carrier of M, the carrier of N);
for x,y being Element of the carrier of M holds F.(x+y) = F.x + F.y
proof
let x,y be Element of the carrier of M;
reconsider z = x + y as Element of the carrier of M;
F.(x+y) = f.(x+y) + g.(x+y) by Th1
.= f.x+ f.y + g.(x+y) by VECTSP_1:def 20
.= f.x+ f.y + (g.x+ g.y) by VECTSP_1:def 20
.= f.x+ (f.y + (g.x+ g.y)) by RLVECT_1:def 3
.= f.x+ ((f.y + g.x) + g.y) by RLVECT_1:def 3
.= (f.x+ (g.x + f.y)) + g.y by RLVECT_1:def 3
.= ((f.x+ g.x) + f.y) + g.y by RLVECT_1:def 3
.= (F.x + f.y) + g.y by Th1
.= F.x + (f.y + g.y) by RLVECT_1:def 3 .= F.x + F.y by Th1;
hence thesis;
end; then
F is additive;
hence thesis;
end;
definition
let M be AbGroup;
func set_End(M) -> non empty Subset of
Funcs(the carrier of M,the carrier of M) equals
{f where f is Function of M,M : f is Endomorphism of M };
coherence
proof
set z = ZeroMap(M,M);
set H = {f where f is Function of M,M : f is Endomorphism of M };
A1: now
let u be object;
assume u in H; then
ex z being Function of M,M st u = z & z is Endomorphism of M;
hence u in Funcs(the carrier of M,the carrier of M) by FUNCT_2:8;
end;
z in H;
hence thesis by A1,TARSKI:def 3;
end;
end;
::Endomorphism of M
Lm3:
for M be AbGroup
for f be object st f in set_End(M) holds f is Endomorphism of M
proof
let M be AbGroup;
let f be object;
assume f in set_End(M); then
consider f1 be Function of M,M such that
A2: f1 = f & f1 is Endomorphism of M;
thus thesis by A2;
end;
definition
let M be AbGroup;
func add_End(M) -> BinOp of set_End(M) equals
(ADD(M,M))|[:set_End(M),set_End(M):];
correctness
proof
set V = Funcs(the carrier of M,the carrier of M);
set V1 = set_End(M);
A1: dom(ADD(M,M)) = [:V,V:] by FUNCT_2:def 1;
A2: for z be object st z in [:V1,V1:] holds ((ADD(M,M))|[:V1,V1:]).z in V1
proof
let z be object;
assume
A3: z in [:V1,V1:]; then
consider f,g be object such that
A4: f in V1 & g in V1 and
A5: z=[f,g] by ZFMISC_1:def 2;
reconsider g1=g,f1=f as Element of V by A4;
[f,g] in dom((ADD(M,M))|[:V1,V1:]) by A1,A3,A5,RELAT_1:62,ZFMISC_1:96;
then
A6: ((ADD(M,M))|[:V1,V1:]).z = (ADD(M,M)).(f1,g1) by A5,FUNCT_1:47;
reconsider f1,g1 as additive Function
of the carrier of M,the carrier of M by A4,Lm3;
(ADD(M,M)).(f1,g1) is additive
Function of the carrier of M,the carrier of M by Th2;
hence thesis by A6;
end;
dom((ADD(M,M))|[:V1,V1:]) =[:V1,V1:] by A1,RELAT_1:62,ZFMISC_1:96;
hence thesis by A2,FUNCT_2:3;
end;
end;
theorem Th3:
for M be AbGroup
for f,g be Endomorphism of M holds
f in Funcs(the carrier of M,the carrier of M) &
g in Funcs(the carrier of M,the carrier of M) &
(add_End(M)).[f,g] = (ADD(M,M)).(f,g) &
(ADD(M,M)).(f,g) is Endomorphism of M
proof
let M be AbGroup;
let f,g be Endomorphism of M;
f in set_End(M) & g in set_End(M);
hence thesis by Th2,ZFMISC_1:87,FUNCT_1:49;
end;
reserve M,N for AbGroup;
definition
let M be AbGroup,f,g be Element of Funcs(the carrier of M,the carrier of M);
redefine func g*f -> Element of Funcs(the carrier of M,the carrier of M); :: redefines * (FUNCT_1, synonym) → * (RELAT_1, synonym) → (#) (RELAT_1, definition)
coherence
proof
reconsider f,g as Function of M,M;
g*f in Funcs(the carrier of M,the carrier of M) by FUNCT_2:9;
hence thesis;
end;
end;
::$INSERT prepare Composition of Homomorphisms
definition
let M be AbGroup;
func FuncComp(M) -> BinOp of Funcs(the carrier of M,the carrier of M) means
:Def4:
for f, g being Element of Funcs(the carrier of M,the carrier of M)
holds it.(f,g) = f*g;
existence
proof
deffunc F(Element of Funcs(the carrier of M,the carrier of M),
Element of Funcs(the carrier of M,the carrier of M)) = $1*$2;
consider F being BinOp of Funcs(the carrier of M,the carrier of M)
such that
A1: for x,y being Element of Funcs(the carrier of M,the carrier of M)
holds F.(x,y) = F(x,y) from BINOP_1:sch 4;
take F;
let f,g be Element of Funcs(the carrier of M,the carrier of M);
thus thesis by A1;
end;
uniqueness
proof
let it1,it2 be BinOp of Funcs(the carrier of M,the carrier of M) such that
A2: for f,g being Element of Funcs(the carrier of M,the carrier of M) holds
it1.(f,g) = f*g and
A3: for f,g being Element of Funcs(the carrier of M,the carrier of M)
holds it2.(f,g) = f*g;
now
let f,g be Element of Funcs(the carrier of M,the carrier of M);
thus it1.(f,g) = f*g by A2 .= it2.(f,g) by A3;
end;
hence thesis;
end;
end;
theorem Th4:
for M,N be AbGroup
for f,g be Element of Funcs(the carrier of M, the carrier of N)
holds (ADD(M,N)).(f,g) = (ADD(M,N)).(g,f)
proof
let M,N be AbGroup;
let f,g be Element of Funcs(the carrier of M, the carrier of N);
for x being Element of M holds ((ADD(M,N)).(f,g)).x = ((ADD(M,N)).(g,f)).x
proof
let x be Element of M;
((ADD(M,N)).(f,g)).x = f.x + g.x by Th1 .= ((ADD(M,N)).(g,f)).x by Th1;
hence thesis;
end;
hence thesis;
end;
::$N Endomorphism of M is closed under Composition
theorem Th5:
for M be AbGroup
for f,g be Endomorphism of M holds (FuncComp(M)).(f,g) is Endomorphism of M
proof
let M be AbGroup;
let f,g be Endomorphism of M;
reconsider f, g as Element of Funcs(the carrier of M, the carrier of M)
by FUNCT_2:8;
reconsider F = (FuncComp(M)).(f,g)
as Element of Funcs(the carrier of M, the carrier of M);
F is additive
proof
for x,y being Element of the carrier of M holds F.(x+y) = F.x + F.y
proof
let x,y be Element of the carrier of M;
reconsider z = x + y as Element of the carrier of M;
A1: F.y = (f*g).y by Def4;
F.(x+y) = (f*g).z by Def4
.= f.(g.(x+y)) by FUNCT_2:15 .= f.(g.x+g.y) by VECTSP_1:def 20
.= f.(g.x)+ f.(g.y) by VECTSP_1:def 20
.= (f*g).x + f.(g.y) by FUNCT_2:15 .= (f*g).x + (f*g).y by FUNCT_2:15
.= F.x + F.y by Def4,A1;
hence thesis;
end;
hence thesis;
end;
hence thesis;
end;
definition
let M be AbGroup;
func mult_End(M) -> BinOp of set_End(M) equals
(FuncComp(M))|[:set_End(M),set_End(M):];
correctness
proof
set V = Funcs(the carrier of M,the carrier of M);
set V1 = set_End(M);
A1: dom(FuncComp(M)) = [:V,V:] by FUNCT_2:def 1;
A2: for z be object st z in [:V1,V1:] holds ((FuncComp(M))|[:V1,V1:]).z in V1
proof
let z be object;
assume
A3: z in [:V1,V1:];
then consider f,g be object such that
A4: f in V1 & g in V1 and
A5: z=[f,g] by ZFMISC_1:def 2;
reconsider g1=g,f1=f as Element of V by A4;
[f,g] in dom((FuncComp(M))|[:V1,V1:]) by A1,A3,A5,RELAT_1:62,ZFMISC_1:96;
then
A6: ((FuncComp(M))|[:V1,V1:]).z = (FuncComp(M)).(f1,g1) by A5,FUNCT_1:47;
reconsider f1,g1 as
additive Function of the carrier of M,the carrier of M by A4,Lm3;
(FuncComp(M)).(f1,g1) is additive
Function of the carrier of M,the carrier of M by Th5;
hence thesis by A6;
end;
dom((FuncComp(M))|[:V1,V1:]) =[:V1,V1:] by A1,RELAT_1:62,ZFMISC_1:96;
hence thesis by A2,FUNCT_2:3;
end;
end;
theorem Th6:
for M be AbGroup for f,g be Endomorphism of M holds
f in Funcs(the carrier of M,the carrier of M) &
g in Funcs(the carrier of M,the carrier of M) &
(mult_End(M)).[f,g] = (FuncComp(M)).(f,g) &
(FuncComp(M)).(f,g) is Endomorphism of M
proof
let M be AbGroup;
let f,g be Endomorphism of M;
f in set_End(M) & g in set_End(M);
hence thesis by Th5,ZFMISC_1:87,FUNCT_1:49;
end;
definition
let M be AbGroup;
func 0_End(M) -> Element of set_End(M) equals ZeroMap(M,M);
correctness
proof
ZeroMap(M,M) in set_End(M);
hence thesis;
end;
func 1_End(M) -> Element of set_End(M) equals id M;
correctness
proof
id M in set_End(M);
hence thesis;
end;
end;
definition
let M be AbGroup;
let f be Element of set_End(M);
func Inv(f) -> Element of set_End(M) means :Def8:
for x being Element of M holds it.x = f.(-x);
existence
proof
deffunc F(Element of M) =f.( -$1);
consider g being Function such that
A1: dom g = the carrier of M & for x be Element of M holds g.x = F(x)
from FUNCT_1:sch 4;
f in set_End(M); then
consider f1 be Function of M,M such that
A2: f1 = f & f1 is Endomorphism of M;
g in set_End(M)
proof
A3: for o be object st o in the carrier of M holds g.o in the carrier of M
proof
let o be object;
assume o in the carrier of M; then
reconsider o as Element of the carrier of M;
g.o = f1.(-o) by A1,A2;
hence thesis;
end;
reconsider g as Function of the carrier of M,the carrier of M
by A3,A1,FUNCT_2:3;
for x,y be Element of the carrier of M
holds g.(x+y) = (g.x) + (g.y)
proof
let x,y be Element of M;
reconsider z = x+y as Element of M;
A5: f1.(-x) = g.x & f1.(-y) = g.y by A1,A2;
A6: -z = -x - y by VECTSP_1:17 .= (-x) + (-y);
g.(x+y) = f1.((-x) + (-y)) by A1,A2,A6
.= g.x + g.y by A5,A2,VECTSP_1:def 20;
hence thesis;
end; then
g is additive;
hence thesis;
end; then
reconsider g as Element of set_End(M);
take g;
thus thesis by A1;
end;
uniqueness
proof
let g1, g2 be Element of set_End(M);
assume that
A7: for x being Element of M holds g1.x = f.(-x) and
A8: for x being Element of M holds g2.x = f.(-x);
A9: g1 in set_End(M) & g2 in set_End(M); then
consider gg1 be Function of M,M such that
A10: gg1 = g1 & gg1 is Endomorphism of M;
consider gg2 be Function of M,M such that
A11: gg2 = g2 & gg2 is additive Function of M,M by A9;
A12: dom gg2 = the carrier of M by FUNCT_2:def 1;
for x be object st x in dom g1 holds g1.x = g2.x
proof
let x be object;
assume x in dom g1; then
reconsider x0 = x as Element of M by FUNCT_2:def 1,A10;
g1.x = f.(-x0) by A7 .= g2.x by A8;
hence thesis;
end;
hence thesis by FUNCT_2:def 1,A12,A10,A11;
end;
end;
theorem Th7:
for M be AbGroup
for f be Element of set_End(M) holds (ADD(M,M)).(f,Inv(f)) = ZeroMap(M,M)
proof
let M be AbGroup;
let f be Element of set_End(M);
f in set_End(M); then
consider f1 be Function of the carrier of M, the carrier of M such that
A1: f1 = f & f1 is Endomorphism of M;
Inv(f) in set_End(M); then
consider g1 be Function of the carrier of M, the carrier of M such that
A2: g1 = Inv(f) &
g1 is Endomorphism of M;
reconsider f1, g1 as Element of Funcs(the carrier of M, the carrier of M)
by FUNCT_2:8;
for x being Element of the carrier of M holds ((ADD(M,M)).(f1,g1)).x
= (ZeroMap(M,M)).x
proof
let x be Element of the carrier of M;
A3: g1.x = f1.(-x) by A1,A2,Def8;
A4: f1.0.M + f1.0.M = f1.(0.M + 0.M) by A1,VECTSP_1:def 20
.= f1.0.M by ALGSTR_1:7 .= f1.0.M + 0.M by ALGSTR_1:7;
((ADD(M,M)).(f1,g1)).x
= f1.x + f1.(-x) by Th1,A3 .= f1.(x + (-x)) by A1,VECTSP_1:def 20
.= f1.(0.M) by VECTSP_1:19
.=((the carrier of M) --> 0.M).x by A4,RLVECT_1:8
.= (ZeroMap(M,M)).x by GRCAT_1:def 7;
hence thesis;
end;
hence thesis by A1,A2;
end;
::$INSERT Define the Ring of Endomorphism of M as a structure.
definition
let M be AbGroup;
func End_Ring(M) -> strict non empty doubleLoopStr equals
doubleLoopStr(# set_End(M), add_End(M), mult_End(M), 1_End(M),0_End(M) #);
coherence;
end;
Lm4:
for M be AbGroup
for f be Element of Funcs(the carrier of M,the carrier of M) holds
(ADD(M,M)).(f,ZeroMap(M,M)) = f
proof
let M be AbGroup;
let f be Element of Funcs(the carrier of M,the carrier of M);
reconsider z = ZeroMap(M,M)
as Element of Funcs(the carrier of M,the carrier of M) by FUNCT_2:8;
for x being Element of M holds ((ADD(M,M)).(f,z)).x = f.x
proof
let x be Element of M;
((ADD(M,M)).(f,z)).x = f.x + z.x by Th1
.= f.x + ((the carrier of M) --> 0.M).x by GRCAT_1:def 7 .= f.x + 0.M;
hence thesis by RLVECT_1:def 4;
end; then
(ADD(M,M)).(f,z) = f;
hence thesis;
end;
Lm5:
for M be AbGroup holds End_Ring(M) is Abelian
proof
let M be AbGroup;
for f,g being Element of End_Ring(M) holds f + g = g + f
proof
let f,g be Element of End_Ring(M);
f in set_End(M); then
consider f1 be Function of the carrier of M, the carrier of M such that
A1: f1 = f & f1 is Endomorphism of M;
g in set_End(M); then
consider g1 be Function of the carrier of M, the carrier of M such that
A2: g1 = g & g1 is Endomorphism of M;
reconsider f1,g1 as Element of Funcs(the carrier of M,the carrier of M)
by FUNCT_2:9;
f + g = (ADD(M,M)).(f1,g1) by A1,A2,Th3 .= (ADD(M,M)).(g1,f1) by Th4
.= g + f by A1,A2,Th3;
hence thesis;
end;
hence thesis;
end;
Lm6:
for M be AbGroup holds End_Ring(M) is add-associative
proof
let M be AbGroup;
for f,g,h being Element of End_Ring(M) holds f+(g+h) = (f+g)+h
proof
let f, g, h be Element of End_Ring(M);
reconsider fg = f+g, gh = g+h as Element of set_End(M);
reconsider f1=f, g1=g, h1=h, fg1=fg, gh1=gh as Endomorphism of M
by Lm3;
reconsider f1,g1,h1,fg1,gh1 as Element of
Funcs(the carrier of M, the carrier of M) by Th3;
A1: (ADD(M,M)).(f1,g1) = fg by Th3;
A2: (ADD(M,M)).(g1,h1) = gh by Th3;
(f + g)+ h = (ADD(M,M)).(fg1,h1) by Th3
.= (ADD(M,M)).(f1,gh1) by A2,A1,Lm2 .= f + (g + h) by Th3;
hence thesis;
end;
hence thesis;
end;
Lm7:
for M be AbGroup holds End_Ring(M) is right_zeroed
proof
let M be AbGroup;
for f being Element of End_Ring(M) holds
(add_End(M)).(f,0_End(M)) = f
proof
let f be Element of End_Ring(M);
f in set_End(M); then
consider f1 be Function of the carrier of M, the carrier of M such that
A1: f1 = f & f1 is Endomorphism of M;
reconsider f1 = f, z1 = 0_End(M) as Endomorphism of M by A1;
reconsider f1,z1 as Element of Funcs(the carrier of M,the carrier of M) by Th3;
thus (add_End(M)).(f,0_End(M)) = ADD(M,M).(f1,z1) by Th3 .= f by Lm4;
end;
hence thesis;
end;
Lm8:
for M be AbGroup holds End_Ring(M) is right_complementable
proof
let M be AbGroup;
for f being Element of End_Ring(M) holds f is right_complementable
proof
let f be Element of End_Ring(M);
reconsider f0 = f as Element of set_End(M);
reconsider g = Inv(f0) as Element of End_Ring(M);
g in set_End(M); then
consider g1 be Function of the carrier of M, the carrier of M such that
A1: g1 = g & g1 is Endomorphism of M;
f in set_End(M); then
consider f1 be Function of the carrier of M, the carrier of M such that
A2: f1 = f & f1 is Endomorphism of M;
reconsider z1 = 0_End(M) as additive Function of
the carrier of M,the carrier of M;
reconsider f1, z1 as Element of
Funcs(the carrier of M, the carrier of M) by A2,Th3;
A3: f + g = (ADD(M,M)).(f0,Inv(f0)) by A2,A1,Th3 .= 0_End(M) by Th7;
take g;
thus thesis by A3;
end;
hence thesis;
end;
Lm9:
for M be AbGroup holds End_Ring(M) is distributive
proof
let M be AbGroup;
A1: for f, g, v being Element of End_Ring(M) holds v * (f+g) = v * f + v * g
proof
let f, g, v be Element of End_Ring(M);
f in set_End(M); then
consider f1 be Function of the carrier of M, the carrier of M such that
A2: f1 = f & f1 is Endomorphism of M;
g in set_End(M); then
consider g1 be Function of the carrier of M, the carrier of M such that
A3: g1 = g & g1 is Endomorphism of M;
v in set_End(M); then
consider v1 be Function of the carrier of M, the carrier of M such that
A4: v1 = v & v1 is Endomorphism of M;
reconsider fg1 = (ADD(M,M)).(f1,g1) as Endomorphism of M by A2,A3,Th3;
A5: f+g = (ADD(M,M)).(f1,g1) by A2,A3,Th3;
v*f in set_End(M); then
consider vf1 be Function of the carrier of M, the carrier of M such that
A6: vf1=v*f & vf1 is Endomorphism of M;
v*g in set_End(M); then
consider vg1 be Function of the carrier of M, the carrier of M such that
A7: vg1=v*g & vg1 is Endomorphism of M;
A8: vf1 = (FuncComp(M)).(v1,f1) by A2,A4,A6,Th6;
A9: vg1 = (FuncComp(M)).(v1,g1) by A3,A4,A7,Th6;
reconsider f1,g1,v1,vf1,vg1
as Element of Funcs(the carrier of M,the carrier of M) by FUNCT_2:9;
A10: for x be Element of M holds
((FuncComp(M)).(v1,fg1)).x = ((ADD(M,M)).(vf1,vg1)).x
proof
let x be Element of the carrier of M;
A11: ((ADD(M,M)).(f1,g1)).x = f1.x + g1.x by Th1;
A12: (v1*f1).x = v1.(f1.x) & (v1*g1).x = v1.(g1.x) by FUNCT_2:15;
A13: ((FuncComp(M)).(v1,f1)).x = (v1*f1).x &
((FuncComp(M)).(v1,g1)).x = (v1*g1).x by Def4;
fg1 in Funcs(the carrier of M,the carrier of M) by FUNCT_2:9; then
((FuncComp(M)).(v1,fg1)).x = (v1*fg1).x by Def4
.= v1.(f1.x + g1.x) by A11,FUNCT_2:15
.= (vf1).x + (vg1).x by A8,A9,A13,A12,A4,VECTSP_1:def 20
.= (ADD(M,M).(vf1,vg1)).x by Th1;
hence thesis;
end;
reconsider F = (FuncComp(M)).(v1,fg1) as Function of
the carrier of M,the carrier of M by A4,Th6;
reconsider G = (ADD(M,M)).(vf1,vg1) as Function of
the carrier of M,the carrier of M;
v*(f+g) = F by A4,A5,Th6 .= G by A10 .= v*f + v*g by A6,A7,Th3;
hence thesis;
end;
for f, g, v being Element of End_Ring(M) holds (f + g)*v = f*v + g*v
proof
let f, g, v be Element of End_Ring(M);
f in set_End(M); then
consider f1 be Function of the carrier of M, the carrier of M such that
A14: f1 = f & f1 is Endomorphism of M;
g in set_End(M); then
consider g1 be Function of the carrier of M, the carrier of M such that
A15: g1 = g & g1 is Endomorphism of M;
v in set_End(M); then
consider v1 be Function of the carrier of M, the carrier of M such that
A16: v1 = v & v1 is Endomorphism of M;
A17: f+g = (ADD(M,M)).(f1,g1) by A14,A15,Th3;
reconsider fg1 = (ADD(M,M)).(f1,g1) as Endomorphism of M by A14,A15,Th3;
f*v in set_End(M); then
consider fv1 be Function of the carrier of M, the carrier of M such that
A18: fv1=f*v & fv1 is Endomorphism of M;
g*v in set_End(M); then
consider gv1 be Function of the carrier of M, the carrier of M such that
A19: gv1=g*v & gv1 is Endomorphism of M;
reconsider f1,g1,v1,fv1,gv1
as Element of Funcs(the carrier of M,the carrier of M) by FUNCT_2:9;
A20: fv1 = (FuncComp(M)).(f1,v1) by A14,A16,A18,Th6;
A21: gv1 = (FuncComp(M)).(g1,v1) by A15,A16,A19,Th6;
A22: for x be Element of M holds
((FuncComp(M)).(fg1,v1)).x = ((ADD(M,M)).(fv1,gv1)).x
proof
let x be Element of M;
A23: (f1*v1).x = f1.(v1.x) & (g1*v1).x = g1.(v1.x)by FUNCT_2:15;
A24: ((FuncComp(M)).(f1,v1)).x = (f1*v1).x &
((FuncComp(M)).(g1,v1)).x = (g1*v1).x by Def4;
fg1 in Funcs(the carrier of M,the carrier of M) by FUNCT_2:9; then
((FuncComp(M)).(fg1,v1)).x = (fg1*v1).x by Def4
.= ((ADD(M,M)).(f1,g1)).(v1.x) by FUNCT_2:15
.= (fv1).x + (gv1).x by A20,A21,A24,A23,Th1
.= (ADD(M,M).(fv1,gv1)).x by Th1;
hence thesis;
end;
reconsider F = (FuncComp(M)).(fg1,v1) as Function of
the carrier of M,the carrier of M by A16,Th6;
reconsider G = (ADD(M,M)).(fv1,gv1) as Function of
the carrier of M,the carrier of M;
(f+g)*v = F by A16,A17,Th6 .= G by A22 .= f*v + g*v by A18,A19,Th3;
hence thesis;
end;
hence thesis by A1;
end;
Lm10:
for M be AbGroup holds End_Ring(M) is associative
proof
let M be AbGroup;
for f, g, h being Element of End_Ring(M) holds (f*g)*h = f*(g*h)
proof
let f, g, h be Element of End_Ring(M);
f in set_End(M); then
consider f1 be Function of the carrier of M,the carrier of M such that
A1: f1 = f & f1 is Endomorphism of M;
g in set_End(M); then
consider g1 be Function of the carrier of M,the carrier of M such that
A2: g1 = g & g1 is Endomorphism of M;
h in set_End(M); then
consider h1 be Function of the carrier of M,the carrier of M such that
A3: h1 = h & h1 is Endomorphism of M;
f*g in set_End(M); then
consider fg1 be Function of the carrier of M,the carrier of M such that
A4: fg1=f*g & fg1 is Endomorphism of M;
g*h in set_End(M); then
consider gh1 be Function of the carrier of M,the carrier of M such that
A5: gh1=g*h & gh1 is Endomorphism of M;
A6: f*g = (FuncComp(M)).(f1,g1) by A1,A2,Th6;
A7: g*h = (FuncComp(M)).(g1,h1) by A2,A3,Th6;
reconsider f1,g1,h1,fg1,gh1 as Element of
Funcs(the carrier of M,the carrier of M) by FUNCT_2:9;
A8: for x be Element of M holds
((FuncComp(M)).(fg1,h1)).x = ((FuncComp(M)).(f1,gh1)).x
proof
let x be Element of the carrier of M;
A9: g1.(h1.x) = (g1*h1).x by FUNCT_2:15
.= gh1.x by A5,A7,Def4;
((FuncComp(M)).(fg1,h1)).x = (fg1*h1).x by Def4
.= ((FuncComp(M)).(f1,g1)).(h1.x) by A4,A6,FUNCT_2:15
.= (f1*g1).(h1.x) by Def4
.= f1.(gh1.x) by A9,FUNCT_2:15
.= (f1*gh1).x by FUNCT_2:15
.= ((FuncComp(M)).(f1,gh1)).x by Def4;
hence thesis;
end;
reconsider F = (FuncComp(M)).(fg1,h1)
as Function of the carrier of M,the carrier of M;
reconsider G = (FuncComp(M)).(f1,gh1)
as Function of the carrier of M,the carrier of M;
(f*g)*h = F by A3,A4,Th6 .= G by A8 .= f*(g*h) by A1,A5,Th6;
hence thesis;
end;
hence thesis;
end;
::::well-unital
Lm11:
for M be AbGroup holds End_Ring(M) is well-unital
proof
let M be AbGroup;
for f being Element of End_Ring(M)
holds f * 1.End_Ring(M) = f & 1.End_Ring(M) * f = f
proof
let f be Element of End_Ring(M);
f in set_End(M); then
consider f1 be Function of the carrier of M, the carrier of M such that
A1: f1 = f & f1 is Endomorphism of M;
reconsider f1 as Element of Funcs(the carrier of M,the carrier of M)
by FUNCT_2:9;
reconsider I1 = id M as Element of Funcs(the carrier of M,the carrier of M)
by FUNCT_2:9;
A2: for x be Element of the carrier of M holds
((FuncComp(M)).(f1,I1)).x = f1.x & ((FuncComp(M)).(I1,f1)).x = f1.x
proof
let x be Element of the carrier of M;
A3: ((FuncComp(M)).(f1,I1)).x = (f1*(I1)).x by Def4
.= f1.(I1.x) by FUNCT_2:15 .= f1.x;
((FuncComp(M)).(I1,f1)).x = (I1*(f1)).x by Def4
.= I1.(f1.x) by FUNCT_2:15 .= f1.x;
hence thesis by A3;
end;
A4: f * 1.End_Ring(M) = (FuncComp(M)).(f1,I1) by A1,Th6
.= f1 by A2 .= f by A1;
1.End_Ring(M) * f = (FuncComp(M)).(I1,f1) by A1,Th6
.= f1 by A2 .= f by A1;
hence thesis by A4;
end;
hence thesis;
end;
::$N the structure of End_Ring(M) turns to be a Ring.
theorem
for M be AbGroup holds End_Ring(M) is Ring
by Lm5,Lm6,Lm7,Lm8,Lm9,Lm10,Lm11;
registration
let M be AbGroup;
cluster End_Ring(M) -> Abelian add-associative right_zeroed
right_complementable associative well-unital distributive;
coherence by Lm5,Lm6,Lm7,Lm8,Lm9,Lm10,Lm11;
end;
registration
let M be AbGroup;
cluster End_Ring(M) -> strict;
coherence;
end;
reserve R for Ring;
reserve r for Element of R;
::$N the Def. of \cite{MOD_4.abs} cannot be applied since no ring-hom. is used.
definition
let R;
let M,N be LeftMod of R;
mode Homomorphism of R,M,N -> Function of M,N means :Def10:
it is additive & it is homogeneous;
existence
proof
take ZeroMap(M,N);
thus thesis;
end;
end;
theorem Th9:
for M,N be LeftMod of R, f be Homomorphism of R,M,N holds
f is one-to-one onto implies
f" is Homomorphism of R,N,M
proof
let M,N be LeftMod of R, f be Homomorphism of R,M,N;
assume
A1: f is one-to-one onto;
reconsider g = f" as Function of N,M by A1,FUNCT_2:25;
for a,b being Element of the carrier of N holds g.(a+b) = g.a + g.b
proof
let a,b be Element of N;
consider x being object such that
A2: x in the carrier of M & a = f.x by A1,FUNCT_2:11;
reconsider x as Element of M by A2;
consider y being object such that
A3: y in the carrier of M & b = f.y by A1,FUNCT_2:11;
reconsider y as Element of M by A3;
g.a + g.b = x + g.(f.y) by A1,A2,A3,FUNCT_2:26
.= x + y by A1,FUNCT_2:26
.= g.(f.(x+y)) by A1,FUNCT_2:26
.= g.(a+b) by A2,A3,VECTSP_1:def 20,Def10;
hence thesis;
end; then
A4: g is additive;
for r be Element of R, a being Element of the carrier of N holds
g.(r*a) = r*g.a
proof
let r be Element of R, a be Element of the carrier of N;
consider x being object such that
A5: x in the carrier of M & a = f.x by A1,FUNCT_2:11;
reconsider x as Element of M by A5;
g.(r*a) = g.(f.(r*x)) by A5, MOD_2:def 2,Def10
.= r*x by A1,FUNCT_2:26 .= r*(g.a) by A1,A5,FUNCT_2:26;
hence thesis;
end;then
g is homogeneous;
hence thesis by A4,Def10;
end;
definition
let R;
let M,N be LeftMod of R;
pred M ~= N means
ex f be Homomorphism of R,M,N st f is one-to-one onto;
end;
definition
let R;
let M be LeftMod of R;
mode Endomorphism of R,M is Homomorphism of R,M,M;
end;
theorem Tref:
for M be LeftMod of R holds M ~= M
proof
let M be LeftMod of R;
A1: id M is Endomorphism of R,M by Def10;
id M is onto by RELAT_1:45;
hence thesis by A1;
end;
theorem Tsym:
for M,N be LeftMod of R holds M ~= N implies N ~= M
proof
let M,N be LeftMod of R;
assume M ~= N; then
consider f be Homomorphism of R,M,N such that
A2: f is one-to-one onto;
reconsider g = f" as Function of N,M by A2,FUNCT_2:25;
A3: g is Homomorphism of R,N,M by A2,Th9;
g*f = id(dom f) by A2,FUNCT_1:39 .= id M by FUNCT_2:def 1; then
g is onto by FUNCT_2:23;
hence thesis by A3,A2;
end;
definition
let R;
let M,N be LeftMod of R;
redefine pred M ~= N; :: redefines ~= (LMOD_XX1, definition)
reflexivity by Tref;
symmetry by Tsym;
end;
theorem
for L,M,N be LeftMod of R holds L ~= M & M ~= N implies L ~= N
proof
let L,M,N be LeftMod of R;
assume
A1: L ~= M & M ~= N; then
consider f be Homomorphism of R,L,M such that
A2: f is one-to-one onto;
consider g be Homomorphism of R,M,N such that
A3: g is one-to-one onto by A1;
reconsider G = g*f as Function of L,N;
for x,y be Element of L holds G.(x+y) = G.x + G.y
proof
let x,y be Element of L;
A4: G.x = g.(f.x) by FUNCT_2:15;
A5: G.y = g.(f.y) by FUNCT_2:15;
G.(x+y) = g.(f.(x+y)) by FUNCT_2:15
.= g.(f.x+f.y) by Def10,VECTSP_1:def 20
.= G.x + G.y by A4,A5,Def10,VECTSP_1:def 20;
hence thesis;
end; then
A6: G is additive;
for x be Element of L, a be Element of R holds G.(a*x) = a*G.x
proof
let x be Element of L, a be Element of R;
A7: G.x = g.(f.x) by FUNCT_2:15;
G.(a*x) = g.(f.(a*x)) by FUNCT_2:15
.= g.(a*f.x) by Def10,MOD_2:def 2
.= a*G.x by A7,Def10,MOD_2:def 2;
hence thesis;
end; then
G is homogeneous; then
A8: G is Homomorphism of R,L,N by A6,Def10;
G is one-to-one onto by A2,A3,FUNCT_2:27;
hence thesis by A8;
end;
theorem Th13:
for M,N be LeftMod of R, f be Homomorphism of R,M,N holds
f is one-to-one iff ker(f) = {0.M}
proof
let M,N be LeftMod of R, f be Homomorphism of R,M,N;
A1: f.0.M = f.(0.M+0.M) by RLVECT_1:4 .= f.0.M + f.0.M
by Def10,VECTSP_1:def 20; then
A2: f.0.M = 0.N by RLVECT_1:9;
A3: 0.M in ker f by A2;
thus f is one-to-one implies ker(f) = {0.M}
proof
assume
A5: f is one-to-one;
for x being object holds x in ker f iff x in {0.M}
proof
let x be object;
x in ker f implies x in {0.M}
proof
assume x in ker f; then
consider x1 be Element of M such that
A7: x1 = x & f.x1 = 0.N;
A8: f.x1 = f.0.M by A1,A7,RLVECT_1:9;
dom f = the carrier of M by FUNCT_2:def 1; then
x = 0.M by A5,A8,A7;
hence thesis by TARSKI:def 1;
end;
hence thesis by A3,TARSKI:def 1;
end;
hence thesis by TARSKI:2;
end;
assume
A10: ker(f) = {0.M};
for x1,x2 be object st x1 in dom f & x2 in dom f & f.x1 = f.x2
holds x1 = x2
proof
let x1,x2 be object;
assume
A11: x1 in dom f & x2 in dom f & f.x1 = f.x2; then
reconsider x1,x2 as Element of M;
A12: -(f.x2) = (-1.R)*(f.x2) by VECTSP_1:14
.=f.((-1.R)*x2) by Def10,MOD_2:def 2 .= f.(-x2) by VECTSP_1:14;
0.N = f.x1 + (f.-x2) by A12,A11,RLVECT_1:5
.= f.(x1+(-x2)) by Def10,VECTSP_1:def 20; then
x1 - x2 in ker f; then
x1 - x2 = 0.M by A10,TARSKI:def 1;
hence thesis by VECTSP_1:19;
end;
hence thesis;
end;
definition
let R;
let M be AbGroup, s be Function of R,End_Ring(M);
func LModlmult(M,s) ->
Function of [:the carrier of R, the carrier of M:], the carrier of M
means
:Def12:
for x be Element of the carrier of R,
y be Element of the carrier of M holds ex h be Endomorphism of M st
h = s.x & it.(x,y) = h.y;
existence
proof
defpred P[Element of the carrier of R, Element of the carrier of M,
Element of the carrier of M] means
ex h be additive Function of the carrier of M,the carrier of M st
h = s.$1 & $3 = h.$2;
A1: for x be Element of the carrier of R, y be Element of the carrier of M
ex z being Element of the carrier of M st P[x,y,z]
proof
let x be Element of the carrier of R, y be Element of the carrier of M;
s.x in set_End(M); then
consider h be Function of the carrier of M, the carrier of M such that
A2: h = s.x & h is Endomorphism of M;
reconsider z = h.y as Element of the carrier of M;
take z;
thus thesis by A2;
end;
consider f being Function of
[:the carrier of R, the carrier of M:], the carrier of M such that
A3: for x be Element of the carrier of R, y be Element of the carrier of M
holds P[x,y,f.(x,y)] from BINOP_1:sch 3(A1);
take f;
let x be Element of the carrier of R, y be Element of the carrier of M;
thus thesis by A3;
end;
uniqueness
proof
let F1,F2 be Function of
[:the carrier of R, the carrier of M:], the carrier of M;
assume that
A4: for x be Element of the carrier of R, y be Element of the carrier of M
holds ex h be Endomorphism of M st
h = s.x & F1.(x,y) = h.y
and
A5: for x be Element of the carrier of R, y be Element of the carrier of M
holds ex h be Endomorphism of M st h = s.x & F2.(x,y) = h.y;
now
let x be Element of the carrier of R, y be Element of the carrier of M;
consider h1 be Endomorphism of M such that
A6: h1 = s.x & F1.(x,y) = h1.y by A4;
consider h2 be Endomorphism of M such that
A7: h2 = s.x & F2.(x,y) = h2.y by A5;
thus F1.(x,y) = F2.(x,y) by A6,A7;
end;
hence thesis;
end;
end;
definition
let R;
let M be AbGroup, s be Function of R,End_Ring(M);
func AbGrLMod(M,s) -> strict non empty ModuleStr over R equals
ModuleStr(# the carrier of M, the addF of M, 0.M, LModlmult(M,s) #);
coherence;
end;
Lm12:
for R for M be AbGroup, s be Function of R,End_Ring(M),
a be Element of R, x,y be Element of AbGrLMod(M,s)
holds a*(x+y) = a*x + a*y
proof
let R;
let M be AbGroup, s be Function of R,End_Ring(M),
a be Element of R, x,y be Element of AbGrLMod(M,s);
consider h be Endomorphism of M such that
A1: h = s.a & a*x = h.x by Def12;
consider h1 be Endomorphism of M such that
A2: h1 = s.a & a*y = h1.y by Def12;
consider h2 be Endomorphism of M such that
A3: h2 = s.a & (LModlmult(M,s)).(a,x+y) = h2.(x+y) by Def12;
reconsider x1 = x, y1 =y as Element of M;
a*(x+y) = h.(x1+y1) by A1,A3
.= h.x1 + h.y1 by VECTSP_1:def 20
.= a*x + a*y by A1, A2;
hence thesis;
end;
Lm13: ::::h = s.a + s.b requires s is ringhom
for R for M be AbGroup, s be Function of R,End_Ring(M),
a,b be Element of R, x be Element of AbGrLMod(M,s)
st s is RingHomomorphism
holds (a+b)*x = a*x+b*x
proof
let R;
let M be AbGroup, s be Function of R,End_Ring(M),
a,b be Element of R, x be Element of AbGrLMod(M,s);
assume
A1: s is RingHomomorphism;
consider h be Endomorphism of M such that
A2: h = s.(a+b) & (a+b)*x = h.x by Def12;
s.a in set_End(M); then
consider ha be Function of the carrier of M, the carrier of M such that
A3: ha = s.a & ha is Endomorphism of M;
s.b in set_End(M); then
consider hb be Function of the carrier of M, the carrier of M such that
A4: hb = s.b & hb is Endomorphism of M;
consider h1 be Endomorphism of M such that
A5: h1 = s.a & a*x = h1.x by Def12;
consider h2 be Endomorphism of M such that
A6: h2 = s.b & b*x = h2.x by Def12;
reconsider x1=x as Element of the carrier of M;
A7: h = s.a + s.b by A2,VECTSP_1:def 20, A1
.= (ADD(M,M)).(ha,hb) by A3,A4,Th3;
reconsider h, ha,hb as Element of
Funcs(the carrier of M,the carrier of M) by FUNCT_2:9;
(a+b)*x = h.x by A2 .= ha.x1 + hb.x1 by A7,Th1
.= a*x + b*x by A3,A5, A4,A6;
hence thesis;
end;
Lm14: ::::A5: h = (s.a)*(s.b) requires s is ringhom
for R for M be AbGroup, s be Function of R,End_Ring(M),
a,b be Element of R, x be Element of AbGrLMod(M,s) st
s is RingHomomorphism holds (a*b)*x = a*(b*x)
proof
let R;
let M be AbGroup, s be Function of R,End_Ring(M),
a,b be Element of R, x be Element of AbGrLMod(M,s);
assume
A1: s is RingHomomorphism;
consider h be Endomorphism of M such that
A2: h = s.(a*b) & (a*b)*x = h.x by Def12;
consider h2 be Endomorphism of M such that
A3: h2 = s.b & b*x = h2.x by Def12;
consider h3 be Endomorphism of M such that
A4: h3 = s.a & a*(b*x) = h3.(b*x) by Def12;
s.a in set_End(M); then
consider ha be Function of the carrier of M, the carrier of M such that
A5: ha = s.a & ha is Endomorphism of M;
s.b in set_End(M); then
consider hb be Function of the carrier of M, the carrier of M such that
A6: hb = s.b & hb is Endomorphism of M;
A7: h = (s.a)*(s.b) by A2,A1, GROUP_6:def 6
.= (FuncComp(M)).(ha,hb) by A5,A6,Th6;
reconsider h, ha,hb as Element of Funcs(the carrier of M,the carrier of M)
by FUNCT_2:9;
reconsider x1=x as Element of the carrier of M;
(a*b)*x = (ha*hb).x1 by Def4,A2,A7
.= a*(b*x) by A4,A5,A3,A6,FUNCT_2:15;
hence thesis;
end;
theorem Th14:
for R for M be AbGroup, s be Function of R,End_Ring(M) st
s is RingHomomorphism holds AbGrLMod(M,s) is LeftMod of R
proof
let R; let M be AbGroup,
s be Function of R,End_Ring(M);
assume
A1: s is RingHomomorphism;
A2: AbGrLMod(M,s) is Abelian
proof
for x,y be Element of AbGrLMod(M,s) holds x+y = y+x
proof
let x, y be Element of AbGrLMod(M,s);
reconsider x1 = x, y1 = y as Element of M;
x + y = x1 + y1 .= y1 + x1 .= y + x;
hence thesis;
end;
hence thesis;
end;
A3: AbGrLMod(M,s) is add-associative
proof
for x,y,z be Element of AbGrLMod(M,s) holds (x+y) +z = x +(y+z)
proof
let x, y, z be Element of AbGrLMod(M,s);
reconsider x1 = x, y1 = y, z1 = z as Element of M;
reconsider xy = x+y as Element of AbGrLMod(M,s);
reconsider xy1 = xy, yz1 = y + z as Element of M;
reconsider yh = y1 + y1 as Element of M;
(x+y)+z = (x1+y1)+z1 .= x1+(y1+z1) by ALGSTR_1:7
.= x + (y+z);
hence thesis;
end;
hence thesis;
end;
A4: AbGrLMod(M,s) is right_zeroed
proof
for x be Element of AbGrLMod(M,s) holds x + 0.AbGrLMod(M,s) = x
proof
let x be Element of AbGrLMod(M,s);
reconsider x1 = x as Element of M;
x + 0.AbGrLMod(M,s) = x1 + 0.M .= x by ALGSTR_1:7;
hence thesis;
end;
hence thesis;
end;
A5: AbGrLMod(M,s) is right_complementable
proof
for x being Element of AbGrLMod(M,s) holds x is right_complementable
proof
let x be Element of AbGrLMod(M,s);
reconsider x1 = x as Element of M;
consider y1 be Element of M such that
A6: x1 + y1 = 0.M by ALGSTR_1:7;
reconsider y = y1 as Element of AbGrLMod(M,s);
take y;
thus thesis by A6;
end;
hence thesis;
end;
AbGrLMod(M,s) is scalar-unital
proof
for x be Element of AbGrLMod(M,s) holds 1.R * x = x
proof
let x be Element of AbGrLMod(M,s);
reconsider x1 = x as Element of M;
consider h be additive Function of the carrier of M,the carrier of M
such that
A7: h = s.(1.R) & 1.R * x = h.x by Def12;
s is unity-preserving by A1;
hence thesis by A7;
end;
hence thesis;
end; then
AbGrLMod(M,s) is Abelian add-associative right_zeroed
right_complementable vector-distributive scalar-distributive
scalar-associative scalar-unital by A2,A3,A4,A5,A1,Lm12,Lm13,Lm14;
hence thesis;
end;
::$N the set of all functions from R-module M, to R-module N form R-module.
reserve M,N for LeftMod of R;
definition
let R,M,N;
func 0_Funcs(M,N) -> Element of Funcs(the carrier of M,the carrier of N)
equals
ZeroMap(M,N);
correctness by FUNCT_2:8;
end;
definition
let R,M,N;
func ADD(M,N) -> BinOp of Funcs(the carrier of M,the carrier of N)
means :Def15:
for f,g being Element of Funcs(the carrier of M,the carrier of N) holds
it.(f,g) = (the addF of N).:(f,g);
existence
proof
deffunc F(Element of Funcs(the carrier of M,the carrier of N),
Element of Funcs(the carrier of M,the carrier of N))
= (the addF of N).:($1,$2);
consider F1 being BinOp of Funcs(the carrier of M,the carrier of N)
such that
A1: for x,y being Element of Funcs(the carrier of M,the carrier of N)
holds F1.(x,y) = F(x,y) from BINOP_1:sch 4;
take F1;
let f,g be Element of Funcs(the carrier of M,the carrier of N);
thus thesis by A1;
end;
uniqueness
proof
let it1,it2 be BinOp of Funcs(the carrier of M,the carrier of N) such that
A2: for f,g being Element of Funcs(the carrier of M,the carrier of N) holds
it1.(f,g) = (the addF of N).:(f,g) and
A3: for f,g being Element of Funcs(the carrier of M,the carrier of N) holds
it2.(f,g) = (the addF of N).:(f,g);
now
let f,g be Element of Funcs(the carrier of M,the carrier of N);
thus it1.(f,g) = (the addF of N).:(f,g) by A2 .= it2.(f,g) by A3;
end;
hence thesis;
end;
end;
Lm15:
for M,N be LeftMod of R for x being Element of M,
f being Function of M, N holds x in dom f
proof
let M,N be LeftMod of R;
let x be Element of M,
f be Function of M,N;
x in the carrier of M;
hence thesis by FUNCT_2:def 1;
end;
reserve f,g,h for Element of Funcs(the carrier of M, the carrier of N);
theorem Th15:
for R,M,N,f,g,h holds
h = ADD(M,N).(f,g) iff for x being Element of the carrier of M
holds h.x = f.x + g.x
proof
let R,M,N,f,g,h;
hereby
assume
A1: h = ADD(M,N).(f,g);
let x be Element of the carrier of M;
A2: x in dom ((the addF of N).:(f,g)) by Lm15;
thus h.x = ((the addF of N).:(f,g)).x by A1,Def15
.= f.x + g.x by A2,FUNCOP_1:22;
end;
assume
A3: for x being Element of M holds h.x=f.x + g.x;
now
let x be Element of M;
A4: x in dom ((the addF of N).:(f,g)) by Lm15;
thus (ADD(M,N).(f,g)).x = ((the addF of N).:(f,g)).x by Def15
.= f.x + g.x by A4,FUNCOP_1:22 .= h.x by A3;
end;
hence h = (ADD(M,N)).(f,g);
end;
definition
let R,M,N;
let F be Function of [:the carrier of R,the carrier of N:], the carrier of N;
let a be Element of the carrier of R;
let f be Function of M,N;
redefine func F[;](a,f) -> :: redefines [;] (FUNCOP_1, definition)
Element of Funcs(the carrier of M, the carrier of N);
coherence
proof
A1: dom f = the carrier of M by FUNCT_2:def 1;
reconsider g = <:dom f --> a, f:> as Function of M,
[:the carrier of R, the carrier of N:] by A1,FUNCT_3:58;
F[;](a,f) = F * g;
hence thesis by FUNCT_2:8;
end;
end;
definition
let R,M,N;
func LMULT(M,N) ->
Function of [:the carrier of R,Funcs(the carrier of M,the carrier of N):],
Funcs(the carrier of M,the carrier of N) means
:Def16:
for a being Element of the carrier of R, f being Element of
Funcs(the carrier of M,the carrier of N),
x being Element of the carrier of M holds (it.[a,f]).x = a*(f.x);
existence
proof
deffunc F(Element of the carrier of R,Element of
Funcs(the carrier of M,the carrier of N)) = ((the lmult of N)[;]($1,$2));
consider F1 being
Function of [:the carrier of R,Funcs(the carrier of M,the carrier of N):],
Funcs(the carrier of M,the carrier of N)
such that
A1: for a be Element of the carrier of R,
f being Element of Funcs(the carrier of M,the carrier of N) holds
F1.(a,f) = F(a,f) from BINOP_1:sch 4;
take F1;
let a be Element of the carrier of R,
f be Element of Funcs(the carrier of M,the carrier of N),
x be Element of the carrier of M;
A2: dom (F1.[a,f]) = the carrier of M by FUNCT_2:92;
F1.(a,f) = ((the lmult of N)[;](a,f)) by A1;
hence thesis by A2,FUNCOP_1:32;
end;
uniqueness
proof
let it1,it2 be Function of
[:the carrier of R,Funcs(the carrier of M,the carrier of N):],
Funcs(the carrier of M,the carrier of N) such that
A4: for a being Element of the carrier of R,
f being Element of Funcs(the carrier of M,the carrier of N),
x being Element of the carrier of M holds (it1.[a,f]).x = a*(f.x) and
A5: for a being Element of the carrier of R,
f being Element of Funcs(the carrier of M,the carrier of N),
x being Element of the carrier of M holds (it2.[a,f]).x = a*(f.x);
now
let a be Element of the carrier of R,
f be Element of Funcs(the carrier of M,the carrier of N);
now
let x be Element of the carrier of M;
thus (it1.[a,f]).x = a*(f.x) by A4 .= (it2.[a,f]).x by A5;
end;
hence it1.[a,f] = it2.[a,f];
end;
hence thesis;
end;
end;
definition
let R,M,N;
func Func_Mod(R,M,N) -> non empty ModuleStr over R equals
ModuleStr(# Funcs(the carrier of M,the carrier of N),
ADD(M,N), 0_Funcs(M,N), LMULT(M,N) #);
coherence;
end;
theorem Th16:
for R,M,N holds
for a be Element of the carrier of R,
f,h be Element of Funcs(the carrier of M, the carrier of N) holds
h = (LMULT(M,N)).[a,f] iff for x being Element of M holds h.x = a*(f.x)
proof
let R,M,N;
let a be Element of the carrier of R,
f,h be Element of Funcs(the carrier of M, the carrier of N);
thus
h = (LMULT(M,N)).[a,f] implies for x being Element of the carrier of M
holds h.x = a*(f.x) by Def16;
now
assume
A1: for x being Element of the carrier of M holds h.x = a*(f.x);
for x being Element of the carrier of M holds h.x = (LMULT(M,N).[a,f]).x
proof
let x be Element of the carrier of M;
thus h.x = a*(f.x) by A1 .= ((LMULT(M,N)).[a,f]).x by Def16;
end;
hence h = (LMULT(M,N)).[a,f];
end;
hence thesis;
end;
Lm16:
for R,M,N
for f,g holds (ADD(M,N)).(f,g) = (ADD(M,N)).(g,f)
proof
let R,M,N;
let f,g;
for x being Element of M holds ((ADD(M,N)).(f,g)).x = ((ADD(M,N)).(g,f)).x
proof
let x be Element of M;
((ADD(M,N)).(f,g)).x = g.x + f.x by Th15
.= ((ADD(M,N)).(g,f)).x by Th15;
hence thesis;
end;
hence thesis;
end;
Lm17:
for R,M,N for f,g,h holds
(ADD(M,N)).(f,(ADD(M,N)).(g,h)) = (ADD(M,N)).((ADD(M,N)).(f,g),h)
proof
let R,M,N,f,g,h;
set M1 = the carrier of M, N1 = the carrier of N;
reconsider fg=(ADD(M,N)).(f,g), gh=(ADD(M,N)).(g,h) as Element of Funcs(M1,N1);
set F1 = (ADD(M,N)).(f,gh);
set F2 = (ADD(M,N)).(fg,h);
for x being Element of M holds F1.x = F2.x
proof
let x be Element of M;
A1: gh.x = g.x + h.x by Th15;
A2: fg.x = f.x + g.x by Th15;
F1.x = f.x + (g.x + h.x) by Th15,A1 .= fg.x + h.x by A2,RLVECT_1:def 3
.= F2.x by Th15;
hence thesis;
end;
hence thesis;
end;
Lm18:
(ADD(M,N)).(f,0_Funcs(M,N)) = f
proof
set F1 = (ADD(M,N)).(f,0_Funcs(M,N));
for x being Element of M holds F1.x = f.x
proof
let x be Element of M;
F1.x = f.x + (0_Funcs(M,N)).x by Th15
.= f.x + ((the carrier of M) --> 0.N).x by GRCAT_1:def 7 .= f.x + 0.N;
hence thesis by RLVECT_1:def 4;
end;
hence thesis;
end;
Lm19:
for R,M,N for f holds (ADD(M,N)).(f,LMULT(M,N).[-1.R,f]) = 0_Funcs(M,N)
proof
let R,M,N,f;
set g = (LMULT(M,N)).[-1.R,f];
set F1 = ADD(M,N).(f,g);
for x being Element of M holds F1.x = 0_Funcs(M,N).x
proof
let x be Element of M;
g.x = (-1.R)*(f.x) by Th16 .= -f.x by VECTSP_1:14; then
F1.x = f.x + (-f.x) by Th15
.= ((the carrier of M) --> 0.N).x by VECTSP_1:19
.=(0_Funcs(M,N)).x by GRCAT_1:def 7;
hence thesis;
end;
hence thesis;
end;
::vector-distributive
reserve a,b for Element of the carrier of R;
Lm20:
for R,M,N for f,g for a holds
LMULT(M,N).[a,(ADD(M,N)).(f,g)]
= (ADD(M,N)).(LMULT(M,N).[a,f],LMULT(M,N).[a,g])
proof
let R; let M,N; let f,g; let a;
set af = (LMULT(M,N)).[a,f], ag = (LMULT(M,N)).[a,g], fg = ADD(M,N).(f,g),
F1=ADD(M,N).(LMULT(M,N).[a,f],LMULT(M,N).[a,g]),
F2=LMULT(M,N).[a,(ADD(M,N)).(f,g)];
for x being Element of M holds F1.x = F2.x
proof
let x be Element of M;
A1: ((LMULT(M,N)).[a,g]).x = a*(g.x) by Th16;
A2: fg.x = f.x + g.x by Th15;
F1.x = (af).x + (ag).x by Th15
.= a*(f.x) + a*(g.x) by Th16,A1
.= a*(fg.x) by A2,VECTSP_1:def 14
.= ((LMULT(M,N)).[a,fg]).x by Th16;
hence thesis;
end;
hence thesis;
end;
::scalar-distributive (a + b) * v = a * v + b * v
Lm21:
for R for M,N for f for a,b holds
LMULT(M,N).[a+b,f] = (ADD(M,N)).(LMULT(M,N).[a,f],LMULT(M,N).[b,f])
proof
let R,M,N,f,a,b;
set af = (LMULT(M,N)).[a,f], bf =(LMULT(M,N)).[b,f], abf =(LMULT(M,N)).[a+b,f],
F1 = LMULT(M,N).[a+b,f],
F2=ADD(M,N).(LMULT(M,N).[a,f],LMULT(M,N).[b,f]);
for x being Element of M holds F1.x = F2.x
proof
let x be Element of M;
A1: ((LMULT(M,N)).[b,f]).x = b*(f.x) by Th16;
F1.x = (a+b)*(f.x) by Th16
.= a*(f.x) + b*(f.x) by VECTSP_1:def 15
.= af.x + bf.x by Th16,A1.= ((ADD(M,N)).(af,bf)).x by Th15;
hence thesis;
end;
hence thesis;
end;
Lm22:
for R for M,N for f for a,b holds
LMULT(M,N).[a*b,f] = LMULT(M,N).[a,LMULT(M,N).[b,f]]
proof
let R; let M,N; let f; let a,b;
set bf =(LMULT(M,N)).[b,f],abf =(LMULT(M,N)).[a*b,f];
for x being Element of M holds
(LMULT(M,N).[a*b,f]).x = (LMULT(M,N).[a,LMULT(M,N).[b,f]]).x
proof
let x be Element of M;
(LMULT(M,N).[a*b,f]).x = (a*b)*(f.x) by Th16
.= a*(b*f.x) by VECTSP_1:def 16
.= a*(bf.x) by Th16
.= (LMULT(M,N).[a,bf]).x by Th16;
hence thesis;
end;
hence thesis;
end;
Lm23:
for R for M,N for f holds LMULT(M,N).[1.R,f] = f
proof
let R; let M,N; let f;
for x being Element of M holds (LMULT(M,N).[1.R,f]).x = f.x
proof
let x be Element of M;
(LMULT(M,N).[1.R,f]).x = 1.R*(f.x) by Th16 .= f.x;
hence thesis;
end;
hence thesis;
end;
Lm24:
Func_Mod(R,M,N) is right_complementable
proof
let f be Element of Func_Mod(R,M,N);
reconsider g = LMULT(M,N).[-1.R,f]
as Element of Func_Mod(R,M,N) by FUNCT_2:5;
take g;
thus f + g = 0.Func_Mod(R,M,N) by Lm19;
end;
registration
let R, M,N;
cluster Func_Mod(R,M,N) -> Abelian add-associative right_zeroed
right_complementable vector-distributive scalar-distributive
scalar-associative scalar-unital;
coherence by Lm16,Lm17,Lm18,Lm20,Lm21,Lm23,Lm22,Lm24;
end;
theorem
for R for M,N holds Func_Mod(R,M,N) is LeftMod of R;
reserve R for comRing;
reserve M,M1,N,N1 for LeftMod of R;
::$N Hom(M,N) the set of all R Homomorphisms form left R-Module
theorem Th18:
for R,M,N
for f,g be Homomorphism of R,M,N holds
ADD(M,N).(f,g) is Homomorphism of R,M,N
proof
let R,M,N;
let f,g be Homomorphism of R,M,N;
reconsider f,g as Element of Funcs(the carrier of M, the carrier of N)
by FUNCT_2:8;
reconsider F = ADD(M,N).(f,g)
as Element of Funcs(the carrier of M, the carrier of N);
A1: for x,y being Element of the carrier of M holds F.(x+y) = F.x + F.y
proof
let x,y be Element of the carrier of M;
reconsider z = x + y as Element of the carrier of M;
F.(x+y) = f.(x+y) + g.(x+y) by Th15
.= f.x+ f.y + g.(x+y) by Def10,VECTSP_1:def 20
.= f.x+ f.y + (g.x+ g.y) by Def10,VECTSP_1:def 20
.= f.x+ (f.y + (g.x+ g.y)) by RLVECT_1:def 3
.= f.x+ ((f.y + g.x) + g.y) by RLVECT_1:def 3
.= (f.x+ (g.x + f.y)) + g.y by RLVECT_1:def 3
.= ((f.x+ g.x) + f.y) + g.y by RLVECT_1:def 3
.= (F.x + f.y) + g.y by Th15
.= F.x + (f.y + g.y) by RLVECT_1:def 3
.= F.x + F.y by Th15;
hence thesis;
end;
for a be Element of R, x being Element of the carrier of M holds
F.(a*x) = a*F.x
proof
let a be Element of R, x be Element of the carrier of M;
reconsider z = a*x as Element of the carrier of M;
F.z = f.(a*x) + g.(a*x) by Th15
.= a*f.x + g.(a*x) by Def10,MOD_2:def 2
.= a*f.x + a*g.x by Def10,MOD_2:def 2
.= a*(f.x + g.x) by VECTSP_1:def 14
.= a*F.x by Th15;
hence thesis;
end; then
F is homogeneous;
hence thesis by A1, Def10,VECTSP_1:def 20;
end;
definition
let R,M1,M,N;
let f be Element of Funcs(the carrier of M1,the carrier of M),
g be Element of Funcs(the carrier of M,the carrier of N);
redefine func g*f -> Element of Funcs(the carrier of M1,the carrier of N); :: redefines * (FUNCT_1, synonym) → * (RELAT_1, synonym) → (#) (RELAT_1, definition)
coherence by FUNCT_2:128;
end;
Lm25:
for M,N,M1
for f,g be Element of Funcs(the carrier of M, the carrier of N),
u be Element of Funcs(the carrier of M1, the carrier of M) holds
(ADD(M,N).(f,g))*u = ADD(M1,N).(f*u, g*u)
proof
let M,N,M1;
let f,g be Element of Funcs(the carrier of M, the carrier of N),
u be Element of Funcs(the carrier of M1, the carrier of M);
reconsider fg = ADD(M,N).(f,g)
as Element of Funcs(the carrier of M, the carrier of N);
reconsider fu = f*u, gu = g*u
as Element of Funcs(the carrier of M1, the carrier of N);
for x be Element of the carrier of M1 holds (fg*u).x=(ADD(M1,N).(fu,gu)).x
proof
let x be Element of the carrier of M1;
A1: fu.x = f.(u.x) & gu.x = g.(u.x) by FUNCT_2:15;
reconsider ux = u.x as Element of the carrier of M;
(fg*u).x = fg.ux by FUNCT_2:15
.= fu.x + gu.x by A1,Th15
.=((ADD(M1,N)).(fu,gu)).x by Th15;
hence thesis;
end;
hence thesis;
end;
Lm26:
for M,N,N1
for f,g be Element of Funcs(the carrier of M, the carrier of N),
u be Element of Funcs(the carrier of N, the carrier of N1)
st u is additive holds u*(ADD(M,N).(f,g)) = ADD(M,N1).(u*f, u*g)
proof
let M,N,N1;
let f,g be Element of Funcs(the carrier of M, the carrier of N),
u be Element of Funcs(the carrier of N, the carrier of N1);
assume
A1: u is additive;
reconsider fg = ADD(M,N).(f,g)
as Element of Funcs(the carrier of M, the carrier of N);
reconsider uf = u*f as Element of Funcs(the carrier of M, the carrier of N1);
reconsider ug = u*g as Element of Funcs(the carrier of M, the carrier of N1);
for x be Element of the carrier of M holds (u*fg).x =(ADD(M,N1).(uf,ug)).x
proof
let x be Element of the carrier of M;
A2: uf.x = u.(f.x) & ug.x = u.(g.x) by FUNCT_2:15;
reconsider fx = f.x, gx = g.x as Element of the carrier of N;
(u*fg).x = u.((ADD(M,N).(f,g)).x) by FUNCT_2:15
.= u.(f.x + g.x) by Th15
.= uf.x + ug.x by A1,A2
.=((ADD(M,N1)).(uf,ug)).x by Th15;
hence thesis;
end;
hence thesis;
end;
Lm27:
for M,N,M1 be LeftMod of R, a be Element of R,
f be Element of Funcs(the carrier of M, the carrier of N),
u be Element of Funcs(the carrier of M1, the carrier of M) holds
((LMULT(M,N)).[a,f])*u = (LMULT(M1,N)).[a,f*u]
proof
let M,N,M1 be LeftMod of R, a be Element of R,
f be Element of Funcs(the carrier of M, the carrier of N),
u be Element of Funcs(the carrier of M1, the carrier of M);
reconsider af = (LMULT(M,N)).[a,f]
as Element of Funcs(the carrier of M, the carrier of N);
reconsider fu = f*u, afu = (LMULT(M1,N)).[a,f*u]
as Element of Funcs(the carrier of M1, the carrier of N);
for x be Element of the carrier of M1 holds (af*u).x = afu.x
proof
let x be Element of the carrier of M1;
reconsider ux = u.x as Element of the carrier of M;
A1: fu.x = f.ux by FUNCT_2:15;
(af*u).x = af.ux by FUNCT_2:15
.= a*((f*u).x) by A1,Th16
.= afu.x by Th16;
hence thesis;
end;
hence thesis;
end;
Lm28:
for M,N,N1 be LeftMod of R, a be Element of R,
f be Element of Funcs(the carrier of M, the carrier of N),
u be Element of Funcs(the carrier of N, the carrier of N1)
st u is homogeneous holds
u*((LMULT(M,N)).[a,f]) = (LMULT(M,N1)).[a,u*f]
proof
let M,N,N1 be LeftMod of R, a be Element of R,
f be Element of Funcs(the carrier of M, the carrier of N),
u be Element of Funcs(the carrier of N, the carrier of N1);
assume
A1: u is homogeneous;
reconsider af = (LMULT(M,N)).[a,f]
as Element of Funcs(the carrier of M, the carrier of N);
reconsider auf = (LMULT(M,N1)).[a,u*f]
as Element of Funcs(the carrier of M, the carrier of N1);
for x be Element of the carrier of M holds (u*af).x = auf.x
proof
let x be Element of the carrier of M;
reconsider fx = f.x as Element of the carrier of N;
(u*af).x = u.(af.x) by FUNCT_2:15
.= u.(a*fx) by Th16
.= a*(u.fx) by A1
.= a*((u*f).x) by FUNCT_2:15 .= auf.x by Th16;
hence thesis;
end;
hence thesis;
end;
theorem Th19:
for M,N,M1 be LeftMod of R,
f be Homomorphism of R,M,N, u be Homomorphism of R,M1,M holds
f*u is Homomorphism of R,M1,N
proof
let M,N,M1 be LeftMod of R,
f be Homomorphism of R,M,N,
u be Homomorphism of R,M1,M;
A1: for x1,y1 be Element of the carrier of M1, a be Element of R holds
(f*u).(x1+y1) = (f*u).x1 + (f*u).y1 & a*(f*u).x1 = a*((f*u).x1)
proof
let x1,y1 be Element of the carrier of M1, a be Element of R;
reconsider ux1 = u.x1, uy1 = u.y1 as Element of the carrier of M;
(f*u).(x1+y1) = f.(u.(x1+y1)) by FUNCT_2:15
.= f.(ux1+uy1) by Def10,VECTSP_1:def 20
.= f.(ux1)+ f.(uy1) by Def10,VECTSP_1:def 20
.= (f*u).x1 + f.(u.y1) by FUNCT_2:15
.= (f*u).x1 + (f*u).y1 by FUNCT_2:15;
hence thesis;
end;
for x1 be Element of the carrier of M1, a be Element of R holds
(f*u).(a*x1) = a*((f*u).x1)
proof
let x1 be Element of the carrier of M1, a be Element of R;
reconsider ux1 = u.x1 as Element of the carrier of M;
(f*u).(a*x1) = f.(u.(a*x1)) by FUNCT_2:15
.= f.(a*ux1) by Def10,MOD_2:def 2
.= a*f.(ux1) by Def10,MOD_2:def 2
.= a*(f*u).x1 by FUNCT_2:15;
hence thesis;
end; then
f*u is homogeneous;
hence thesis by A1,Def10,VECTSP_1:def 20;
end;
::$N commutativity matters (r*a)*g.x .= (a*r)*g.x by VECTSP_1:def 16
theorem Th20:
for R,M,N
for a be Element of the carrier of R, g be Homomorphism of R,M,N holds
LMULT(M,N).[a,g] is Homomorphism of R,M,N
proof
let R,M,N;
let a be Element of the carrier of R, g be Homomorphism of R,M,N;
reconsider g as Element of Funcs(the carrier of M, the carrier of N)
by FUNCT_2:8;
reconsider F = LMULT(M,N).[a,g]
as Element of Funcs(the carrier of M, the carrier of N);
A1: for x,y being Element of the carrier of M holds F.(x+y) = F.x + F.y
proof
let x,y be Element of the carrier of M;
reconsider z = x + y as Element of the carrier of M;
F.z = a*(g.(x+y)) by Def16
.= a*(g.x +g.y) by Def10,VECTSP_1:def 20
.= a*g.x + a*g.y by VECTSP_1:def 14 .= F.x + a*g.y by Def16
.= F.x + F.y by Def16;
hence thesis;
end;
for b be Element of R, x being Element of the carrier of M holds
F.(b*x) = b*F.x
proof
let b be Element of R, x being Element of the carrier of M;
reconsider z = b*x as Element of the carrier of M;
F.z = a*(g.(b*x))by Def16
.= a*(b*g.x) by Def10,MOD_2:def 2
.= (a*b)*g.x by VECTSP_1:def 16
.= b*(a*g.x) by VECTSP_1:def 16 .= b*F.x by Def16;
hence thesis;
end;then
F is homogeneous;
hence thesis by A1,Def10,VECTSP_1:def 20;
end;
definition
let R,M,N;
func set_Hom(M,N) -> non empty Subset of
Funcs(the carrier of M,the carrier of N) equals
{f where f is Function of M,N : f is Homomorphism of R,M,N };
coherence
proof
set z = ZeroMap(M,N);
set H = {f where f is Function of M,N : f is Homomorphism of R,M,N };
A1: now
let u be object;
assume u in H; then
ex z being Function of M,N st u = z & z is Homomorphism of R,M,N;
hence u in Funcs(the carrier of M,the carrier of N) by FUNCT_2:8;
end;
z is Homomorphism of R,M,N by Def10; then
z in H;
hence thesis by A1,TARSKI:def 3;
end;
end;
Lm29: :::::Hom(R,M,N) parts
for R,M,N
for f be object holds f in set_Hom(M,N) iff f is Homomorphism of R,M,N
proof
let R,M,N;
let f be object;
f in set_Hom(M,N) implies f is Homomorphism of R,M,N
proof
assume f in set_Hom(M,N); then
consider f1 be Function of M,N such that
A3: f1 = f & f1 is Homomorphism of R,M,N;
thus thesis by A3;
end;
hence thesis;
end;
definition
let R,M,N;
func add_Hom(M,N) -> BinOp of set_Hom(M,N) equals
(ADD(M,N))|[:set_Hom(M,N),set_Hom(M,N):];
correctness
proof
set V = Funcs(the carrier of M,the carrier of N);
set V1 = set_Hom(M,N);
A1: dom(ADD(M,N)) = [:V,V:] by FUNCT_2:def 1;
A2: for z be object st z in [:V1,V1:] holds ((ADD(M,N))|[:V1,V1:]).z in V1
proof
let z be object;
assume
A3: z in [:V1,V1:];
then consider f,g be object such that
A4: f in V1 & g in V1 and
A5: z = [f,g] by ZFMISC_1:def 2;
reconsider g1=g,f1=f as Element of V by A4;
[f,g] in dom((ADD(M,N))|[:V1,V1:]) by A1,A3,A5,RELAT_1:62,ZFMISC_1:96;
then
A6: ((ADD(M,N))|[:V1,V1:]).z = (ADD(M,N)).(f1,g1) by A5,FUNCT_1:47;
reconsider f1,g1 as Homomorphism of R,M,N by A4,Lm29;
(ADD(M,N)).(f1,g1) is Homomorphism of R,M,N by Th18;
hence thesis by A6;
end;
dom((ADD(M,N))|[:V1,V1:]) =[:V1,V1:] by A1,RELAT_1:62,ZFMISC_1:96;
hence thesis by A2,FUNCT_2:3;
end;
end;
definition
let R,M,N;
let F be Function of [:the carrier of R,the carrier of N:], the carrier of N;
let a be Element of the carrier of R;
let f be Function of M,N;
redefine func F[;](a,f) -> :: redefines [;] (FUNCOP_1, definition)
Element of Funcs(the carrier of M, the carrier of N);
coherence
proof
A1: dom f = the carrier of M by FUNCT_2:def 1;
reconsider g = <:dom f --> a, f:> as Function of M,
[:the carrier of R, the carrier of N:] by A1,FUNCT_3:58;
F[;](a,f) = F * g;
hence thesis;
end;
end;
definition
let R,M,N;
func lmult_Hom(M,N) ->
Function of [:the carrier of R,set_Hom(M,N):], set_Hom(M,N) equals
(LMULT(M,N))|[:the carrier of R,set_Hom(M,N):];
correctness
proof
set CR = the carrier of R, V = Funcs(the carrier of M,the carrier of N),
V1 = set_Hom(M,N);
A1: dom(LMULT(M,N)) = [:CR,V:] by FUNCT_2:def 1;
A2: for z be object st z in [:CR,V1:] holds ((LMULT(M,N))|[:CR,V1:]).z in V1
proof
let z be object;
assume
A3: z in [:CR,V1:];
then consider a,g be object such that
A4: a in CR & g in V1 and
A5: z=[a,g] by ZFMISC_1:def 2;
reconsider a1=a as Element of the carrier of R by A4;
reconsider g1=g as Element of V by A4;
[a1,g1] in dom((LMULT(M,N))|[:CR,V1:])
by A1,A3,A5,RELAT_1:62,ZFMISC_1:96; then
A6: ((LMULT(M,N))|[:CR,V1:]).z = (LMULT(M,N)).(a1,g1) by A5,FUNCT_1:47;
reconsider g1 as Homomorphism of R,M,N by A4,Lm29;
(LMULT(M,N)).(a1,g1) is Homomorphism of R,M,N by Th20;
hence thesis by A6;
end;
dom((LMULT(M,N))|[:CR,V1:]) =[:CR,V1:] by A1,RELAT_1:62,ZFMISC_1:96;
hence thesis by A2,FUNCT_2:3;
end;
end;
definition
let R,M,N;
func 0_Hom(M,N) -> Element of set_Hom(M,N) equals
ZeroMap(M,N);
correctness
proof
ZeroMap(M,N) is Homomorphism of R,M,N by Def10; then
ZeroMap(M,N) in set_Hom(M,N);
hence thesis;
end;
end;
definition
let R,M,N;
func Hom(R,M,N) -> non empty ModuleStr over R equals
ModuleStr(# set_Hom(M,N), add_Hom(M,N), 0_Hom(M,N), lmult_Hom(M,N) #);
coherence;
end;
registration
let R,M,N;
cluster Hom(R,M,N) -> non empty;
coherence;
end;
theorem Th21:
for f,g be Homomorphism of R,M,N holds
f in Funcs(the carrier of M,the carrier of N) &
g in Funcs(the carrier of M,the carrier of N) &
(add_Hom(M,N)).[f,g] = (ADD(M,N)).(f,g) &
(ADD(M,N)).(f,g) is Homomorphism of R,M,N
proof
let f,g be Homomorphism of R,M,N;
f in set_Hom(M,N) & g in set_Hom(M,N);
hence thesis by ZFMISC_1:87,FUNCT_1:49,Th18;
end;
theorem Th22:
for a be Element of the carrier of R,
f be Homomorphism of R,M,N holds
(lmult_Hom(M,N)).[a,f] = (LMULT(M,N)).[a,f] &
(LMULT(M,N)).[a,f] is Homomorphism of R,M,N
proof
let a be Element of the carrier of R,
f be Homomorphism of R,M,N;
a in the carrier of R & f in set_Hom(M,N);
hence thesis by ZFMISC_1:87,FUNCT_1:49,Th20;
end;
theorem Th23:
for R,M,N
for f1,g1 be Element of Func_Mod(R,M,N),
f,g be Element of Hom(R,M,N) st f1=f & g1= g holds f + g = f1 + g1
proof
let R,M,N;
let f1,g1 be Element of Func_Mod(R,M,N), f,g be Element of Hom(R,M,N);
assume
A1: f1=f & g1= g;
reconsider f0 = f as Homomorphism of R,M,N by Lm29;
reconsider g0 = g as Homomorphism of R,M,N by Lm29;
f+g = (ADD(M,N)).(f0,g0) by Th21 .= f1+g1 by A1;
hence thesis;
end;
Lm30:
for R,M,N
for a be Element of R, f1 be Element of Func_Mod(R,M,N),
f be Element of Hom(R,M,N) st f1=f holds a*f = a*f1
proof
let R,M,N;
let a be Element of R, f1 be Element of Func_Mod(R,M,N),
f be Element of Hom(R,M,N);
assume
A1: f1=f;
reconsider f0 = f as Homomorphism of R,M,N by Lm29;
a*f = (LMULT(M,N)).(a,f0) by Th22 .= a*f1 by A1;
hence thesis;
end;
theorem Th24:
for R for M,N holds Hom(R,M,N) is LeftMod of R
proof
let R,M,N;
A1: Hom(R,M,N) is Abelian
proof
for v,w being Element of Hom(R,M,N) holds v + w = w + v
proof
let f, g be Element of Hom(R,M,N);
f in Hom(R,M,N) & g in Hom(R,M,N); then
reconsider f1=f, g1=g as Element of Func_Mod(R,M,N);
f + g = f1 + g1 by Th23 .= g + f by Th23;
hence thesis;
end;
hence thesis;
end;
A2: Hom(R,M,N) is add-associative
proof
for f,g,h being Element of Hom(R,M,N) holds (f + g) + h = f + (g + h)
proof
let f, g, h be Element of Hom(R,M,N);
f in Hom(R,M,N) & g in Hom(R,M,N) & h in Hom(R,M,N); then
reconsider f1 = f, g1 = g, h1 = h as Element of Func_Mod(R,M,N);
A3: g + h = g1 + h1 by Th23;
f + g = f1 + g1 by Th23; then
(f + g) + h = (f1 + g1) + h1 by Th23
.= f1 + (g1 + h1) by Lm17 .= f + (g + h) by A3,Th23;
hence thesis;
end;
hence thesis;
end;
A4: Hom(R,M,N) is right_zeroed
proof
for f being Element of Hom(R,M,N) holds f + 0.Hom(R,M,N) = f
proof
let f be Element of Hom(R,M,N);
f in Hom(R,M,N); then
reconsider f1 = f as Element of Func_Mod(R,M,N);
f + 0.Hom(R,M,N) = f1 + 0.Func_Mod(R,M,N) by Th23 .= f by Lm18;
hence thesis;
end;
hence thesis;
end;
A5: Hom(R,M,N) is right_complementable
proof
let f be Element of Hom(R,M,N);
f in Hom(R,M,N); then
reconsider f1=f as Element of Func_Mod(R,M,N);
reconsider r = -1.R as Element of R;
r*f = r*f1 by Lm30; then
f + r*f = f1 + r*f1 by Th23
.= 0.Hom(R,M,N) by Lm19;
hence thesis;
end;
A6: Hom(R,M,N) is vector-distributive
proof
for a being Element of R for v,w being Element of Hom(R,M,N)
holds a*(v+w) = a*v+a*w
proof
let a be Element of R; let v,w be Element of Hom(R,M,N);
v in Hom(R,M,N) & w in Hom(R,M,N); then
reconsider v1=v,w1=w as Element of Func_Mod(R,M,N);
A7: v+w = v1+w1 by Th23;
A8: a*v = a*v1 & a*w =a*w1 by Lm30;
a*(v+w) = a*(v1+w1) by A7,Lm30 .= a*v1 + a*w1 by Lm20
.= a*v + a*w by A8,Th23;
hence thesis;
end;
hence thesis;
end;
A9: Hom(R,M,N) is scalar-distributive
proof
for a,b being Element of R for f being Element of Hom(R,M,N) holds
(a+b)*f = a*f+b*f
proof
let a,b be Element of R;
let f being Element of Hom(R,M,N);
f in Hom(R,M,N); then
reconsider f1=f as Element of Func_Mod(R,M,N);
A10: a*f = a*f1 & b*f = b*f1 by Lm30;
(a+b)*f = (a+b)*f1 by Lm30 .= a*f1 + b*f1 by Lm21
.= a*f + b*f by A10,Th23;
hence thesis;
end;
hence thesis;
end;
A11: Hom(R,M,N) is scalar-associative
proof
for a,b being Element of R for f being Element of Hom(R,M,N) holds
(a*b)*f = a*(b*f)
proof
let a,b being Element of R;
let f being Element of Hom(R,M,N);
f in Hom(R,M,N); then
reconsider f1=f as Element of Func_Mod(R,M,N);
A12: (a*b)*f = (a*b)*f1 & b*f = b*f1 by Lm30;
(a*b)*f = (a*b)*f1 by Lm30 .= a*(b*f1) by Lm22 .=a*(b*f) by A12,Lm30;
hence thesis;
end;
hence thesis;
end;
Hom(R,M,N) is scalar-unital
proof
for f being Element of Hom(R,M,N) holds (1.R)*f = f
proof
let f be Element of Hom(R,M,N);
f in Hom(R,M,N); then
reconsider f1=f as Element of Func_Mod(R,M,N);
1.R*f = 1.R*f1 by Lm30 .= f;
hence thesis;
end;
hence thesis;
end;
hence thesis by A1,A2,A4,A5,A6,A9,A11;
end;
registration
let R,M,N;
cluster Hom(R,M,N) -> Abelian add-associative right_zeroed
right_complementable vector-distributive scalar-distributive
scalar-associative scalar-unital;
coherence by Th24;
end;
definition
let R,M1,M,N;
let u be Homomorphism of R,M1,M;
func tau(N,u) -> Function of Hom(R,M,N), Hom(R,M1,N) means
:Def23:
for f be Element of Hom(R,M,N) holds
ex f1 be Homomorphism of R,M,N st f = f1 & it.f =f1*u;
existence
proof
defpred P[object,object] means
ex f1 be Homomorphism of R,M,N st f1 = $1 & $2 = f1*u;
A1: for y be Element of Hom(R,M,N)
ex z be Element of Hom(R,M1,N) st P[y,z]
proof
let y be Element of Hom(R,M,N);
reconsider f1=y as Homomorphism of R,M,N by Lm29;
reconsider f1u = f1*u as Homomorphism of R,M1,N by Th19;
f1u in set_Hom(M1,N); then
reconsider z = f1u as Element of Hom(R,M1,N);
P[y,z];
hence thesis;
end;
consider h be Function of Hom(R,M,N), Hom(R,M1,N) such that
A2: for y be Element of Hom(R,M,N) holds P[y,h.y] from FUNCT_2:sch 3 (A1);
reconsider h as Function of Hom(R,M,N), Hom(R,M1,N);
take h;
let f be Element of Hom(R,M,N);
thus thesis by A2;
end;
uniqueness
proof
let h1,h2 be Function of Hom(R,M,N), Hom(R,M1,N) such that
A3: for f be Element of Hom(R,M,N) holds
ex f1 be Homomorphism of R,M,N st f = f1 & h1.f =f1*u
and
A4: for f be Element of Hom(R,M,N) holds
ex f1 be Homomorphism of R,M,N st f = f1 & h2.f =f1*u;
now
let y be Element of Hom(R,M,N);
consider f1 be Homomorphism of R,M,N such that
A5: y = f1 & h1.y =f1*u by A3;
consider f2 be Homomorphism of R,M,N such that
A6: y = f2 & h2.y =f2*u by A4;
thus h1.y = h2.y by A5,A6;
end;
hence h1 = h2;
end;
end;
Lm31:
for R,M1,M,N
for u be Homomorphism of R,M1,M holds
tau(N,u) is additive homogeneous
proof
let R,M1,M,N;
let u be Homomorphism of R,M1,M;
set F = tau(N,u);
A1: for f,g be Element of Hom(R,M,N) holds F.(f+g) = F.f + F.g
proof
let f,g be Element of Hom(R,M,N);
reconsider h = f + g as Element of Hom(R,M,N);
consider f1 be Homomorphism of R,M,N such that
A2: f = f1 & F.f =f1*u by Def23;
consider g1 be Homomorphism of R,M,N such that
A3: g = g1 & F.g =g1*u by Def23;
consider h1 be Homomorphism of R,M,N such that
A4: h1 = h & F.h = h1*u by Def23;
reconsider f0 = f1,g0 =g1 as Element of
Funcs(the carrier of M,the carrier of N) by FUNCT_2:8;
reconsider u0 = u as Element of
Funcs(the carrier of M1,the carrier of M) by FUNCT_2:8;
reconsider f1u0 = f1*u, g1u0 = g1*u as Homomorphism of R,M1,N by Th19;
F.(f+g) = (ADD(M,N).(f0,g0))*u0 by A2,A3,A4,Th21
.= ADD(M1,N).(f1*u, g1*u) by Lm25
.= (add_Hom(M1,N)).(f1u0, g1u0) by Th21 .= F.f + F.g by A2,A3;
hence thesis;
end;
for f be Element of Hom(R,M,N), a be Element of R holds F.(a*f) = a*(F.f)
proof
let f be Element of Hom(R,M,N), a be Element of R;
consider f1 be Homomorphism of R,M,N such that
A5: f = f1 & F.f =f1*u by Def23;
reconsider af = a*f as Element of Hom(R,M,N);
consider af1 be Homomorphism of R,M,N such that
A6: af = af1 & F.af =af1*u by Def23;
reconsider f0 = f1,af0 = af1 as Element of
Funcs(the carrier of M,the carrier of N) by FUNCT_2:8;
reconsider u0 = u as Element of
Funcs(the carrier of M1,the carrier of M) by FUNCT_2:8;
reconsider f1u0 = f1*u as Homomorphism of R,M1,N by Th19;
a*(F.f) = (LMULT(M1,N)).[a,f1u0] by Th22, A5
.= ((LMULT(M,N)).[a,f0])*u0 by Lm27
.= F.(a*f) by A6,A5,Th22;
hence thesis;
end;
hence thesis by A1;
end;
registration
let R,M1,M,N;
let u be Homomorphism of R,M1,M;
cluster tau(N,u) -> additive homogeneous;
coherence by Lm31;
end;
theorem
for R,M1,M,N
for u be Homomorphism of R,M1,M holds
tau(N,u) is Homomorphism of R, Hom(R,M,N), Hom(R,M1,N) by Def10;
definition
let R,M,N,N1;
let u be Homomorphism of R,N,N1;
func phi(M,u) -> Function of Hom(R,M,N), Hom(R,M,N1) means
:Def24:
for f be Element of Hom(R,M,N) holds
ex f1 be Homomorphism of R,M,N st f = f1 & it.f =u*f1;
existence
proof
defpred P[object,object] means
ex f1 be Homomorphism of R,M,N st f1 = $1 & $2 = u*f1;
A1: for y be Element of Hom(R,M,N)
ex z be Element of Hom(R,M,N1) st P[y,z]
proof
let y be Element of Hom(R,M,N);
reconsider f1=y as Homomorphism of R,M,N by Lm29;
reconsider uf1 = u*f1 as Homomorphism of R,M,N1 by Th19;
uf1 in set_Hom(M,N1); then
reconsider z = uf1 as Element of Hom(R,M,N1);
P[y,z];
hence thesis;
end;
consider h be Function of Hom(R,M,N), Hom(R,M,N1) such that
A2: for y be Element of Hom(R,M,N) holds P[y,h.y]
from FUNCT_2:sch 3 (A1);
reconsider h as Function of Hom(R,M,N), Hom(R,M,N1);
take h;
let f be Element of Hom(R,M,N);
thus thesis by A2;
end;
uniqueness
proof
let h1,h2 be Function of Hom(R,M,N), Hom(R,M,N1) such that
A3: for f be Element of Hom(R,M,N) holds
ex f1 be Homomorphism of R,M,N st f = f1 & h1.f = u*f1
and
A4: for f be Element of Hom(R,M,N) holds
ex f1 be Homomorphism of R,M,N st f = f1 & h2.f = u*f1;
now
let y be Element of Hom(R,M,N);
consider f1 be Homomorphism of R,M,N such that
A5: y = f1 & h1.y = u*f1 by A3;
consider f2 be Homomorphism of R,M,N such that
A6: y = f2 & h2.y = u*f2 by A4;
thus h1.y = h2.y by A5,A6;
end;
hence h1 = h2;
end;
end;
Lm32:
for R,M,N,N1
for u be Homomorphism of R,N,N1 holds
phi(M,u) is additive homogeneous
proof
let R,M,N,N1;
let u be Homomorphism of R,N,N1;
set F = phi(M,u);
A1: u is additive & u is homogeneous by Def10;
A2: for f,g be Element of Hom(R,M,N) holds F.(f+g) = F.f + F.g
proof
let f,g be Element of Hom(R,M,N);
reconsider h = f + g as Element of Hom(R,M,N);
consider f1 be Homomorphism of R,M,N such that
A3: f = f1 & F.f = u*f1 by Def24;
consider g1 be Homomorphism of R,M,N such that
A4: g = g1 & F.g = u*g1 by Def24;
consider h1 be Homomorphism of R,M,N such that
A5: h1 = h & F.h = u*h1 by Def24;
A6: h1 = ADD(M,N).(f1,g1) by A3,A4,A5,Th21;
reconsider f0 = f1,g0 =g1 as Element of
Funcs(the carrier of M,the carrier of N) by FUNCT_2:8;
reconsider u0 = u
as Element of Funcs(the carrier of N,the carrier of N1) by FUNCT_2:8;
reconsider uf10 = u*f1, ug10 = u*g1 as Homomorphism of R,M,N1 by Th19;
F.(f+g) = ADD(M,N1).(u0*f0, u*g0) by Lm26,A1,A6,A5
.= (add_Hom(M,N1)).(uf10, ug10) by Th21 .= F.f + F.g by A3,A4;
hence thesis;
end;
for f be Element of Hom(R,M,N), a be Element of R holds F.(a*f) = a*(F.f)
proof
let f be Element of Hom(R,M,N), a be Element of R;
consider f1 be Homomorphism of R,M,N such that
A7: f = f1 & F.f = u*f1 by Def24;
reconsider af = a*f as Element of Hom(R,M,N);
consider af1 be Homomorphism of R,M,N such that
A8: af = af1 & F.af =u*af1 by Def24;
reconsider f0 = f1 as Element of
Funcs(the carrier of M,the carrier of N) by FUNCT_2:8;
reconsider u0 = u as Element of
Funcs(the carrier of N,the carrier of N1) by FUNCT_2:8;
reconsider uf10 = u*f1 as Homomorphism of R,M,N1 by Th19;
a*(F.f) = (LMULT(M,N1)).[a,uf10] by A7,Th22
.=u0*((LMULT(M,N)).[a,f0]) by Lm28,A1
.= F.(a*f) by A8,A7,Th22;
hence thesis;
end;
hence thesis by A2;
end;
registration
let R,M,N,N1;
let u be Homomorphism of R,N,N1;
cluster phi(M,u) -> additive homogeneous;
coherence by Lm32;
end;
theorem
for R,M,N,N1
for u be Homomorphism of R,N,N1 holds
phi(M,u) is Homomorphism of R, Hom(R,M,N), Hom(R,M,N1) by Def10;
::$N A formal proof of Hom(R,M) ~= M.
theorem
for R,M holds Hom(R,LeftModule(R),M) ~= M
proof
let R,M;
reconsider R1 = LeftModule(R) as LeftMod of R;
reconsider m1 = 1.R as Element of R1;
deffunc F(Element of Funcs(the carrier of R1,the carrier of M)) = $1.m1;
consider G be Function of
Funcs(the carrier of R1, the carrier of M),M such that
A1: for x be Element of Funcs(the carrier of R1,the carrier of M) holds
G.x = F(x) from FUNCT_2:sch 4;
A2: for f,g be Element of Funcs(the carrier of R1,the carrier of M) holds
G.(ADD(R1,M).(f,g)) = G.f + G.g
proof
let f,g be Element of Funcs(the carrier of R1,the carrier of M);
set h = ADD(R1,M).(f,g);
G.h = h.m1 & G.f = f.m1 & G.g = g.m1 by A1;
hence thesis by Th15;
end;
A3: for f be Element of Funcs(the carrier of R1,the carrier of M),
a be Element of R holds G.((LMULT(R1,M)).[a,f]) = a*(G.f)
proof
let f be Element of Funcs(the carrier of R1,the carrier of M),
a be Element of R;
set h = (LMULT(R1,M)).[a,f];
G.h = h.m1 & G.f = f.m1 by A1;
hence thesis by Th16;
end;
set H = Hom(R,R1,M);
set caH = the carrier of Hom(R,R1,M);
set G1 = G|caH;
A4: dom G = Funcs(the carrier of R1, the carrier of M) by FUNCT_2:def 1;
A5: dom G1 = caH /\ dom G by RELAT_1:61 .= caH by A4,XBOOLE_1:28;
A6: for y be object st y in rng G1 holds y in the carrier of M
proof
let y be object;
assume y in rng G1; then
consider x be object such that
A8: x in dom G1 & y = G1.x by FUNCT_1:def 3;
G.x in the carrier of M by FUNCT_2:5,A8;
hence thesis by A8,FUNCT_1:49,A5;
end;
reconsider G1 as Function of Hom(R,R1,M),M by A5, A6,TARSKI:def 3, FUNCT_2:2;
A10: for f,g be Element of Hom(R,R1,M) holds
G1.(f+g) = G1.f + G1.g
proof
let f,g be Element of Hom(R,R1,M);
A11: f is Homomorphism of R,R1,M & g is Homomorphism of R,R1,M by Lm29;
reconsider f1 = f, g1 = g as Homomorphism of R,R1,M by Lm29;
reconsider f0 = f, g0 = g as
Element of Funcs(the carrier of R1,the carrier of M) by A11,Th21;
(ADD(R1,M)).(f1,g1) is Homomorphism of R,R1,M by Th21; then
A12: (ADD(R1,M)).(f1,g1) in caH;
A13: G1.f = G.f0 by FUNCT_1:49;
A14: G1.g = G.g0 by FUNCT_1:49;
G1.(f+g) = G1.((add_Hom(R1,M)).[f1,g1])
.= G1.(ADD(R1,M).(f,g)) by Th21
.= G.(ADD(R1,M).(f0,g0)) by A12,FUNCT_1:49
.= G1.f + G1.g by A2,A13,A14;
hence thesis;
end;
A15: G1 is additive by A10;
for f be Element of Hom(R,R1,M), a be Element of R holds
G1.(a*f) = a*G1.f
proof
let f be Element of Hom(R,R1,M), a be Element of R;
A16: f is Homomorphism of R,R1,M by Lm29;
reconsider f1 = f as Homomorphism of R,R1,M by Lm29;
reconsider f0 = f as Element of
Funcs(the carrier of R1,the carrier of M) by A16,Th21;
A17: (lmult_Hom(R1,M)).[a,f1] = (LMULT(R1,M)).[a,f1] &
(LMULT(R1,M)).[a,f1] is Homomorphism of R,R1,M by Th22;
A18: (LMULT(R1,M)).[a,f1] in caH by A17;
G1.(a*f) = G1.((lmult_Hom(R1,M)).[a,f1])
.= G1.((LMULT(R1,M)).[a,f]) by Th22
.= G.((LMULT(R1,M)).[a,f]) by A18,FUNCT_1:49
.= a*(G.f0) by A3 .= a*G1.f by FUNCT_1:49;
hence thesis;
end; then
G1 is homogeneous; then
reconsider G1 as Homomorphism of R,H,M by A15,Def10;
A19: ker G1 = {0.Hom(R,R1,M)}
proof
G1.0.H = G1.(0.H+0.H) by RLVECT_1:4 .= G1.0.H + G1.0.H by A10; then
G1.0.H = 0.M by RLVECT_1:9; then
0.H in ker G1; then
A20: for f be object holds f in {0.H} implies f in ker G1 by TARSKI:def 1;
for f be object holds f in ker G1 implies f in {0.H}
proof
let f be object;
assume f in ker G1; then
consider f1 be Element of set_Hom(R1,M) such that
A22: f1 = f & G1.f1 = 0.M;
reconsider f1 as Homomorphism of R,R1,M by Lm29;
reconsider f0 = f1 as Element of
Funcs(the carrier of R1,the carrier of M);
A23: f1 is additive & f1 is homogeneous by Def10;
A24: 0.M = G.f0 by A22,FUNCT_1:49 .= f0.m1 by A1;
for a be Element of R1 holds f0.a = 0.M
proof
let a be Element of R1;
reconsider a0 = a as Element of R;
a0*m1 = a0*1.R .= a0; then
f1.a = a0*0.M by A23,A24 .= 0.M by VECTSP_1:14;
hence thesis;
end; then
f0 = R1 --> 0.M; then
f0 = ZeroMap(R1,M) by GRCAT_1:def 7;
hence thesis by A22, TARSKI:def 1;
end;
hence thesis by A20,TARSKI:2;
end;
for y be object holds y in the carrier of M implies y in rng G1
proof
let y be object;
assume y in the carrier of M; then
reconsider y0 = y as Element of M;
defpred P[object,object] means
ex x1 be object st x1 in the carrier of R & x1 = $1 &
ex x0 be Element of R st x0 = x1 & $2 = x0*y0;
A26: for x be object st x in the carrier of R1
ex y be object st y in the carrier of M & P[x,y]
proof
let x be object;
assume x in the carrier of R1; then
reconsider x0 = x as Element of R;
consider y be object such that
A28: y in the carrier of M & y = x0*y0;
thus thesis by A28;
end;
consider h being Function of R1,the carrier of M such that
A29: for z being object st z in the carrier of R1
holds P[z,h.z] from FUNCT_2:sch 1(A26);
for a,b be Element of R1 holds h.(a+b) = h.a + h.b
proof
let a,b be Element of R1;
consider a1 be object such that
A30: a1 in the carrier of R & a = a1 &
ex a0 be Element of R st a0 = a1 & h.a = a0*y0 by A29;
consider a0 be Element of R such that
A31: a0 = a1 & h.a = a0*y0 by A30;
consider b1 be object such that
A32: b1 in the carrier of R & b = b1 &
ex b0 be Element of R st b0 = b1 & h.b = b0*y0 by A29;
consider b0 be Element of R such that
A33: b0 = b1 & h.b = b0*y0 by A32;
reconsider ab = a+ b as Element of R1;
consider ab1 be object such that
A34: ab1 in the carrier of R & ab = ab1 &
ex ab0 be Element of R st ab0 = ab1 & h.ab = ab0*y0 by A29;
consider ab0 be Element of R such that
A35: ab0 = ab1 & h.ab = ab0*y0 by A34;
ab0 = a0 + b0 by A30,A31,A32,A33,A34,A35;
hence thesis by A33,A31,VECTSP_1:def 15,A35;
end; then
A37: h is additive;
for a be Element of R,b be Element of R1 holds h.(a*b) = a*(h.b)
proof
let a be Element of R,b be Element of R1;
reconsider ab = a*b as Element of R1;
consider b1 be object such that
A38: b1 in the carrier of R & b = b1 &
ex b0 be Element of R st b0 = b1 & h.b = b0*y0 by A29;
consider b0 be Element of R such that
A39: b0 = b1 & h.b = b0*y0 by A38;
reconsider ab = a*b as Element of R1;
consider ab1 be object such that
A40: ab1 in the carrier of R & ab = ab1 &
ex ab0 be Element of R st ab0 = ab1 & h.ab = ab0*y0 by A29;
consider ab0 be Element of R such that
A41: ab0 = ab1 & h.ab = ab0*y0 by A40;
reconsider ab9 = a*b0 as Element of R;
a*b0 = ab0 by A41,A40,A39,A38;
hence thesis by A39,A41,VECTSP_1:def 16;
end; then
A43: h is homogeneous; then
A44: h is Homomorphism of R,R1,M by A37,Def10;
reconsider h1 = h as Homomorphism of R,R1,M by A43,A37,Def10;
reconsider h0 = h as Element of
Funcs(the carrier of R1,the carrier of M) by A44,Th21;
consider m be object such that
A45: m in the carrier of R & m1 = m &
ex m0 be Element of R st m0 = m & h.m1 = m0*y0 by A29;
reconsider n1 = m1 as Element of R;
h0 in caH by A44; then
A47: G1.h = G.h0 by FUNCT_1:49
.= n1*y0 by A1,A45
.= y;
h in dom G1 by A5,A44;
hence thesis by A47,FUNCT_1:def 3;
end; then
G1 is onto by A6,TARSKI:2;
hence thesis by A19,Th13;
end;
::$N Correspondence between Abelian Group and Left R-Module
definition ::forget lmult from ModuleStr
let R,M;
func AbGr(M) -> non empty strict AbGroup equals
addLoopStr (# the carrier of M, the addF of M, 0.M #);
coherence
proof
reconsider IT = addLoopStr(# the carrier of M,the addF of M,0.M #)
as non empty addLoopStr;
A1: for x,y,z being Element of IT holds x+y = y+x & (x+y)+z = x+(y+z) & x+
(0.IT) = x & ex v being Element of IT st x+v = 0.IT
proof
let x,y,z be Element of IT;
reconsider x9=x,y9=y,z9=z as Element of M;
thus x+y = y9+x9 by RLVECT_1:2 .= y+x;
thus (x+y)+z = (x9+y9)+z9 .= x9+(y9+z9) by RLVECT_1:def 3 .= x+(y+z);
thus x+0.IT = x9+(0.M) .= x by RLVECT_1:4;
consider b being Element of M such that
A2: x9 + b = 0.M by ALGSTR_0:def 11;
reconsider b9 = b as Element of IT;
take b9;
thus thesis by A2;
end;
IT is right_complementable
proof
let x be Element of IT;
reconsider x9=x as Element of M;
consider b being Element of M such that
A3: x9 + b = 0.M by ALGSTR_0:def 11;
reconsider b9 = b as Element of IT;
take b9;
thus thesis by A3;
end;
hence thesis by A1,RLVECT_1:def 2,def 3,def 4;
end;
end;
definition
let R,M,N;
let f be Homomorphism of R,M,N;
func AbGr(f) -> Function of AbGr(M), AbGr(N) means :Def26:
for x being object st x in the carrier of AbGr(M) holds it.x = f.x;
existence
proof
defpred P[object,object] means $2 = f.$1;
A1: for x being object st x in the carrier of AbGr(M)
ex y being object st y in the carrier of AbGr(N) & P[x,y]
proof
let x be object;
assume x in the carrier of AbGr(M); then
reconsider z=x as Element of M;
ex y be object st y in the carrier of AbGr(N) & y = f.z;
hence thesis;
end;
ex g being Function of AbGr(M), AbGr(N)
st for x being object st x in the carrier of AbGr(M) holds P[x,g.x]
from FUNCT_2:sch 1(A1); then
consider g being Function of AbGr(M), AbGr(N) such that
A4: for x being object st x in the carrier of AbGr(M) holds g.x = f.x;
take g;
thus thesis by A4;
end;
uniqueness
proof
let g1,g2 be Function of AbGr(M), AbGr(N) such that
A5: for x being object st x in the carrier of AbGr(M) holds
g1.x = f.x and
A6: for x being object st x in the carrier of AbGr(M) holds
g2.x = f.x;
A7: dom g1 = the carrier of AbGr(M) by FUNCT_2:def 1;
now let x be object;
assume
A9: x in dom g1;
hence g1.x = f.x by A5
.= g2.x by A6,A9;
end;
hence thesis by A7;
end;
end;
theorem Th28:
for R,M,N for f be Homomorphism of R,M,N holds
AbGr(f) is Homomorphism of AbGr(M),AbGr(N)
proof
let R, M,N;
let f be Homomorphism of R,M,N;
for x,y being Element of AbGr(M) holds
(AbGr(f)).(x+y) = (AbGr(f)).x + (AbGr(f)).y
proof
let x,y be Element of AbGr(M);
reconsider x1 = x, y1 = y as Element of the carrier of M;
A2: (AbGr(f)).x = f.x1 by Def26;
A4: (AbGr(f)).y = f.y1 by Def26;
reconsider z1 = x+y as Element of the carrier of M;
A6: (AbGr(f)).z1 = f.z1 by Def26;
A7: z1 = x1 + y1;
(AbGr(f)).(x+y)
= f.x1 + f.y1 by A6,A7,Def10,VECTSP_1:def 20
.= (AbGr(f)).x + (AbGr(f)).y by A2,A4;
hence thesis;
end;
hence thesis by VECTSP_1:def 20;
end;
theorem Th29:
for f,g,h be Endomorphism of R,M holds
AbGr(h) = (FuncComp(AbGr(M))).(AbGr(f),AbGr(g)) iff
for x being Element of the carrier of AbGr(M)
holds (AbGr(h)).x = (AbGr(f) * (AbGr(g))).x
proof
let f,g,h be Endomorphism of R,M;
reconsider f1 = AbGr(f), g1 = AbGr(g), h1 = AbGr(h) as
Element of Funcs(the carrier of AbGr(M),the carrier of AbGr(M)) by FUNCT_2:8;
thus AbGr(h) = (FuncComp(AbGr(M))).(AbGr(f),AbGr(g)) implies
for x being Element of the carrier of AbGr(M)
holds (AbGr(h)).x = (AbGr(f) * (AbGr(g))).x
proof
assume AbGr(h) = (FuncComp(AbGr(M))).(AbGr(f),AbGr(g)); then
for x being Element of the carrier of AbGr(M)
holds h1.x = (f1 * g1).x by Def4;
hence thesis;
end;
assume
A3: for x being Element of the carrier of AbGr(M) holds
(AbGr(h)).x = ((AbGr(f))*(AbGr(g))).x;
AbGr(h) = (FuncComp(AbGr(M))).(AbGr(f),AbGr(g))
proof
A4: for x be Element of the carrier of AbGr(M) holds
(AbGr(h)).x = ((FuncComp(AbGr(M))).(AbGr(f),AbGr(g))).x
proof
let x be Element of the carrier of AbGr(M);
((FuncComp(AbGr(M))).(f1,g1)).x = (f1*g1).x by Def4 .= h1.x by A3;
hence thesis;
end;
reconsider h2 = AbGr(h), addfg2 = (FuncComp(AbGr(M))).(f1,g1) as
Function of the carrier of AbGr(M), the carrier of AbGr(M);
h2 = addfg2 by A4;
hence thesis;
end;
hence thesis;
end;
theorem Lm33:
for f,g,h be Endomorphism of R,M st
h = f*g holds AbGr(h) = AbGr(f) * AbGr(g)
proof
let f,g, h be Endomorphism of R,M;
assume
A1: h = f*g;
for x being Element of the carrier of AbGr(M) holds
(AbGr(h)).x = (AbGr(f) * (AbGr(g))).x
proof
let x be Element of the carrier of AbGr(M);
reconsider x2 = x as Element of the carrier of M;
A2: (AbGr(g)).x = g.x2 by Def26;
A3: (AbGr(h)).x = h.x2 by Def26;
reconsider x0 = x as Element of the carrier of M;
A4: (AbGr(h)).x = f.(g.x0) by A1,A3,FUNCT_2:15;
reconsider y0 = g.x0 as Element of the carrier of AbGr(M);
reconsider y1 = y0 as Element of the carrier of M;
(AbGr(f)).y0 = f.y1 by Def26;
hence thesis by A4,A2,FUNCT_2:15;
end;
hence thesis;
end;
theorem Th30:
for f,g,h be Endomorphism of R,M holds
AbGr(h) = ADD(AbGr(M),AbGr(M)).(AbGr(f),AbGr(g)) iff
for x being Element of the carrier of AbGr(M) holds
(AbGr(h)).x = (AbGr(f)).x + (AbGr(g)).x
proof
let f,g,h be Endomorphism of R,M;
reconsider f1 = AbGr(f), g1 = AbGr(g), h1 = AbGr(h) as Element of
Funcs(the carrier of AbGr(M),the carrier of AbGr(M)) by FUNCT_2:8;
thus AbGr(h) = ADD(AbGr(M),AbGr(M)).(AbGr(f),AbGr(g)) implies
for x being Element of the carrier of AbGr(M) holds
(AbGr(h)).x = (AbGr(f)).x + (AbGr(g)).x
proof
assume
A2: AbGr(h) = ADD(AbGr(M),AbGr(M)).(AbGr(f),AbGr(g));
for x being Element of AbGr(M) holds
(AbGr(h)).x = (AbGr(f)).x + (AbGr(g)).x
proof
let x be Element of AbGr(M);
A3: x in dom ((the addF of AbGr(M)).:(f1,g1)) by Lm1;
h1.x = ((the addF of AbGr(M)).:(f1,g1)).x by A2,Def1
.= f1.x + g1.x by A3,FUNCOP_1:22;
hence thesis;
end;
hence thesis;
end;
assume
A4: for x being Element of the carrier of AbGr(M) holds
(AbGr(h)).x = (AbGr(f)).x + (AbGr(g)).x;
AbGr(h) = ADD(AbGr(M),AbGr(M)).(AbGr(f),AbGr(g))
proof
A5: for x be Element of the carrier of AbGr(M) holds
(AbGr(h)).x = (ADD(AbGr(M),AbGr(M)).(AbGr(f),AbGr(g))).x
proof
let x be Element of the carrier of AbGr(M);
A6: x in dom ((the addF of AbGr(M)).:(f1,g1)) by Lm1;
(ADD(AbGr(M),AbGr(M)).(f1,g1)).x
= ((the addF of AbGr(M)).:(f1,g1)).x by Def1
.= f1.x + g1.x by A6,FUNCOP_1:22 .= h1.x by A4;
hence thesis;
end;
reconsider h2 = AbGr(h), addfg2 = (ADD(AbGr(M),AbGr(M)).(f1,g1)) as
Function of the carrier of AbGr(M), the carrier of AbGr(M);
h2 = addfg2 by A5;
hence thesis;
end;
hence thesis;
end;
theorem Th31:
for f,g,h be Endomorphism of R,M st
h = ADD(M,M).(f,g) holds AbGr(h) = ADD(AbGr(M),AbGr(M)).(AbGr(f),AbGr(g))
proof
let f,g,h be Endomorphism of R,M;
assume
A1: h = ADD(M,M).(f,g);
reconsider f1 = AbGr(f), g1 = AbGr(g) as
Element of Funcs(the carrier of AbGr(M),the carrier of AbGr(M)) by FUNCT_2:8;
reconsider f0 = f, g0 = g, h0 = h as
Element of Funcs(the carrier of M,the carrier of M) by FUNCT_2:8;
for x being Element of the carrier of AbGr(M) holds
(AbGr(h)).x = (AbGr(f)).x + (AbGr(g)).x
proof
let x be Element of the carrier of AbGr(M);
reconsider x0 = x as Element of the carrier of M;
A2: (AbGr(f)).x = f.x0 by Def26;
A3: (AbGr(g)).x = g.x0 by Def26;
A4: (AbGr(h)).x = h.x0 by Def26;
(AbGr(h)).x = h0.x0 by A4
.= f0.x0 + g0.x0 by A1,Th15
.= (AbGr(f)).x + (AbGr(g)).x by A2,A3;
hence thesis;
end;
hence thesis by Th30;
end;
theorem
for R be Ring, M be LeftMod of R, a be Element of R, m be Element of M
holds ((curry (the lmult of M)).a ).m = a*m by LOPBAN_8:7;
theorem Th33: ::(a*b)*m by VECTSP_1:def 16 .= (b*a)*m
for R be comRing, M be LeftMod of R, a be Element of R holds
(curry (the lmult of M)).a is Endomorphism of R,M
proof
let R be comRing, M be LeftMod of R, a be Element of R;
set f = (curry (the lmult of M)).a;
A1: for m1,m2 being Element of M holds f.(m1+m2) = f.m1 + f.m2
proof
let m1,m2 be Element of M;
A2: a*m1 = f.m1 & a*m2 = f.m2 by LOPBAN_8:7;
f.(m1+m2) = a*(m1+m2) by LOPBAN_8:7
.= f.m1 + f.m2 by A2,VECTSP_1:def 14;
hence thesis;
end;
for b being Element of R, m being Element of M holds f.(b*m) = b*f.m
proof
let b be Element of R, m be Element of M;
f.(b*m) = a*(b*m) by LOPBAN_8:7
.= (a*b)*m by VECTSP_1:def 16 .= b*(a*m) by VECTSP_1:def 16
.= b*f.m by LOPBAN_8:7;
hence thesis;
end; then
f is homogeneous;
hence thesis by A1,Def10,VECTSP_1:def 20;
end;
theorem Th34:
for f,g,h be Endomorphism of R,M st
h = f*g
holds AbGr(h) = (FuncComp(AbGr(M))).(AbGr(f),AbGr(g))
proof
let f,g,h be Endomorphism of R,M;
assume h = f*g; then
for x being Element of the carrier of AbGr(M) holds
(AbGr(h)).x = ((AbGr(f))*(AbGr(g))).x by Lm33;
hence thesis by Th29;
end;
definition
let R be comRing, M be LeftMod of R; :::ThM3 requires comRing
func canHom(M) -> Function of R, End_Ring(AbGr(M)) means
:Def27:
for x being object st x in the carrier of R holds
ex f be Endomorphism of R,M st
f = (curry (the lmult of M)).x & it.x = AbGr(f);
existence
proof
defpred P[object,object] means
ex f1 being Endomorphism of R,M st
f1 = (curry (the lmult of M)).$1 & $2 = AbGr(f1);
A1: for x being object st x in the carrier of R
ex y being object st y in the carrier of End_Ring(AbGr(M)) & P[x,y]
proof
let x be object;
assume x in the carrier of R; then
reconsider x as Element of R;
reconsider f1 = (curry (the lmult of M)).x as Endomorphism of R,M by Th33;
AbGr(f1) is Endomorphism of AbGr(M) by Th28; then
AbGr(f1) in End_Ring(AbGr(M)); then
consider y be object such that
A3: y = AbGr(f1) and
A4: y in End_Ring(AbGr(M));
thus thesis by A3,A4;
end;
ex g being Function of R, End_Ring(AbGr(M))
st for x being object st x in the carrier of R holds P[x,g.x]
from FUNCT_2:sch 1(A1); then
consider g being Function of R, End_Ring(AbGr(M)) such that
A5: for x being object st x in the carrier of R holds
ex f1 be Endomorphism of R,M st f1 = (curry (the lmult of M)).x &
g.x = AbGr(f1);
take g;
thus thesis by A5;
end;
uniqueness
proof
let g1,g2 be Function of R, End_Ring(AbGr(M)) such that
A6: for x being object st x in the carrier of R holds
ex f1 be Endomorphism of R,M st
f1 = (curry (the lmult of M)).x & g1.x = AbGr(f1) and
A7: for x being object st x in the carrier of R holds
ex f2 be Endomorphism of R,M st
f2 = (curry (the lmult of M)).x & g2.x = AbGr(f2);
A8: dom g1 = the carrier of R by FUNCT_2:def 1
.= dom g2 by FUNCT_2:def 1;
now let x be object;
assume
A9: x in dom g1; then
consider f1 be Endomorphism of R,M such that
A10: f1 = (curry (the lmult of M)).x and
A11: g1.x = AbGr(f1) by A6;
consider f2 be Endomorphism of R,M such that
A12: f2 = (curry (the lmult of M)).x and
A13: g2.x = AbGr(f2) by A7,A9;
thus g1.x = g2.x by A13,A11,A12,A10;
end;
hence thesis by A8;
end;
end;
Lm34:
for R be comRing, M be LeftMod of R holds canHom(M) is additive
proof
let R be comRing, M be LeftMod of R;
for x,y being Element of R holds
(canHom(M)).(x+y) = (canHom(M)).x + (canHom(M)).y
proof
let x,y be Element of R;
consider f be Endomorphism of R,M such that
A1: f = (curry (the lmult of M)).x & (canHom(M)).x = AbGr(f) by Def27;
consider g be Endomorphism of R,M such that
A2: g = (curry (the lmult of M)).y & (canHom(M)).y = AbGr(g) by Def27;
consider h be Endomorphism of R,M such that
A3: h = (curry (the lmult of M)).(x+y) &
(canHom(M)).(x+y) = AbGr(h) by Def27;
reconsider f0 = f, g0 = g, h0 = h as
Element of Funcs(the carrier of M,the carrier of M) by FUNCT_2:8;
reconsider f1 = AbGr(f), g1 = AbGr(g) as Endomorphism of AbGr(M)
by Th28;
for m being Element of the carrier of M holds h.m = f.m + g.m
proof
let m be Element of the carrier of M;
A4: f.m = x*m by A1,LOPBAN_8:7;
A5: g.m = y*m by A2,LOPBAN_8:7;
h0.m = (x+y)*m by A3,LOPBAN_8:7
.= f0.m + g0.m by A4,A5,VECTSP_1:def 15;
hence thesis;
end; then
A6: h0 = ADD(M,M).(f0,g0) by Th15;
(canHom(M)).(x+y) = (ADD(AbGr(M),AbGr(M))).(f1,g1) by A3,A6,Th31
.= (canHom(M)).x + (canHom(M)).y by A1,A2,Th3;
hence thesis;
end;
hence thesis;
end;
registration
let R be comRing, M be LeftMod of R;
cluster canHom(M) -> additive;
coherence by Lm34;
end;
theorem
for R be comRing, M be LeftMod of R,a be Element of R holds
(canHom(M)).a is Homomorphism of AbGr(M),AbGr(M)
proof
let R be comRing, M be LeftMod of R,a be Element of R;
(canHom(M)).a in set_End(AbGr(M)); then
consider f be Function of the carrier of AbGr(M), the carrier of AbGr(M)
such that
A1: f = (canHom(M)).a & f is Endomorphism of AbGr(M);
thus thesis by A1;
end;
Lm36:
for R be comRing, M be LeftMod of R holds canHom(M) is multiplicative
proof
let R be comRing, M be LeftMod of R;
for x,y being Element of R holds
(canHom(M)).(x*y) = (canHom(M)).x * (canHom(M)).y
proof
let x,y be Element of R;
consider f be Endomorphism of R,M such that
A1: f = (curry (the lmult of M)).x & (canHom(M)).x = AbGr(f) by Def27;
consider g be Endomorphism of R,M such that
A2: g = (curry (the lmult of M)).y & (canHom(M)).y = AbGr(g) by Def27;
consider h be Endomorphism of R,M such that
A3: h = (curry (the lmult of M)).(x*y) &
(canHom(M)).(x*y) = AbGr(h) by Def27;
reconsider f0 = f, g0 = g, h0 = h as Element of
Funcs(the carrier of M,the carrier of M) by FUNCT_2:8;
A4: for m being Element of M holds h.m = (f*g).m
proof
let m be Element of M;
A5: g.m = y*m by A2,LOPBAN_8:7;
reconsider ym = y*m as Element of the carrier of M;
h0.m = (x*y)*m by A3,LOPBAN_8:7
.= x*ym by VECTSP_1:def 16
.= f0.(g0.m) by A5,A1,LOPBAN_8:7
.= (f0*g0).m by FUNCT_2:15;
hence thesis;
end;
reconsider f1 = AbGr(f), g1 = AbGr(g) as Endomorphism of AbGr(M) by Th28;
h = f*g by A4; then
(canHom(M)).(x*y) = (FuncComp(AbGr(M))).(f1,g1) by A3,Th34
.= (canHom(M)).x * (canHom(M)).y by A1,A2,Th6;
hence thesis;
end;
hence thesis by GROUP_6:def 6;
end;
Lm37:
for R be comRing, M be LeftMod of R,f be Endomorphism of R,M st
f = 1_End(M) holds
AbGr(f) = 1_End(AbGr(M))
proof
let R be comRing, M be LeftMod of R,f be Endomorphism of R,M;
assume f = 1_End(M);
then AbGr(f) = id AbGr(M) by Def26;
hence thesis;
end;
Lm38:
for R be comRing, M be LeftMod of R holds canHom(M) is unity-preserving
proof
let R be comRing, M be LeftMod of R;
consider f be Endomorphism of R,M such that
A1: f = (curry (the lmult of M)).1.R & (canHom(M)).1.R = AbGr(f) by Def27;
f = 1_End(M)
proof
for m being Element of M holds
f.m = (1_End(M)).m
proof
let m be Element of M;
f.m = 1.R * m by A1,LOPBAN_8:7
.= (1_End(M)).m;
hence thesis;
end;
hence thesis by FUNCT_2:63;
end;
hence thesis by A1,Lm37;
end;
registration
let R be comRing, M be LeftMod of R;
cluster canHom(M) -> linear;
coherence by Lm36,Lm38;
end;
registration
let R be comRing, M be LeftMod of R;
cluster AbGrLMod(AbGr(M),canHom(M)) -> non empty
Abelian add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital;
coherence by Th14;
end;
theorem Th35:
for R be comRing, M be LeftMod of R holds
LModlmult(AbGr(M),canHom(M)) = the lmult of M
proof
let R be comRing, M be LeftMod of R;
set F = LModlmult(AbGr(M),canHom(M));
for z be object st z in [:the carrier of R,the carrier of M:] holds
F.z = (the lmult of M).z
proof
let z be object;
assume
A1: z in [:the carrier of R,the carrier of M:];
consider x,y be object such that
A2: x in the carrier of R & y in the carrier of M & z = [x,y]
by A1,ZFMISC_1:def 2;
reconsider y0 = y as Element of M by A2;
reconsider y1 = y as Element of AbGr(M) by A2;
reconsider x0 = x as Element of R by A2;
consider h be Endomorphism of AbGr(M) such that
A3: h = (canHom(M)).x0 & F.(x0,y0) = h.y0 by Def12;
consider f be Endomorphism of R,M such that
A4: f = (curry (the lmult of M)).x0 & (canHom(M)).x0 = AbGr(f) by Def27;
reconsider y2 = y1 as Element of the carrier of M;
A5: (AbGr(f)).y1 = f.y2 by Def26;
F.(x0,y0) = (the lmult of M).(x0,y0) by A4,A5,A3,LOPBAN_8:7;
hence thesis by A2;
end;
hence thesis;
end;
theorem
for R be comRing, M be strict LeftMod of R holds
AbGrLMod(AbGr(M),canHom(M)) = M
proof
let R be comRing, M be strict LeftMod of R;
AbGrLMod(AbGr(M),canHom(M)) is Submodule of M
proof
set N = AbGrLMod(AbGr(M),canHom(M));
reconsider N as LeftMod of R;
A1: 0.N = 0.M;
A2: the addF of N = (the addF of M) || (the carrier of N)
proof
the addF of N
= (the addF of M) | dom(the addF of M) by RELAT_1:69
.= (the addF of M) ||(the carrier of N) by FUNCT_2:def 1;
hence thesis;
end;
the lmult of N = (the lmult of M)|[:the carrier of R,the carrier of N:]
proof
dom(the lmult of M) = [:the carrier of R,the carrier of M:]
by FUNCT_2:def 1; then
(the lmult of M)|[:the carrier of R,the carrier of N:]
= the lmult of M by RELAT_1:69
.= the lmult of N by Th35;
hence thesis;
end;
hence thesis by A1,A2,VECTSP_4:def 2;
end;
hence thesis by VECTSP_4:31;
end;
definition ::[A-Module]->[AbGr]
let R be comRing, M be LeftMod of R;
func rho(M) -> Function of M, AbGrLMod(AbGr(M),canHom(M)) equals
id M;
coherence;
end;
theorem Th37:
for R be comRing,M be LeftMod of R holds rho(M) is additive homogeneous
proof
let R be comRing,M be LeftMod of R;
reconsider EM = AbGrLMod(AbGr(M),canHom(M)) as LeftMod of R;
for x be Element of the carrier of M, a be Element of R holds
(rho(M)).(a*x) = a*(rho(M)).x
proof
let x be Element of the carrier of M, a be Element of R;
reconsider z = a*x as Element of the carrier of M;
consider F be Endomorphism of AbGr(M) such that
A7: F = (canHom(M)).a & (LModlmult(AbGr(M),canHom(M))).(a,x) = F.x by Def12;
consider f be Endomorphism of R,M such that
A8: f = (curry (the lmult of M)).a & (canHom(M)).a = AbGr(f) by Def27;
reconsider x1 = x as Element of the carrier of AbGr(M);
reconsider x2 = x1 as Element of the carrier of M;
(AbGr(f)).x1 = f.x2 by Def26;
hence thesis by LOPBAN_8:7,A8,A7;
end;
hence thesis;
end;
registration
let R be comRing, M be LeftMod of R;
cluster rho(M) -> additive homogeneous;
coherence by Th37;
end;
theorem Th38:
for R be comRing,M be LeftMod of R holds rho(M) is one-to-one onto
proof
let R be comRing,M be LeftMod of R;
reconsider EM = AbGrLMod(AbGr(M),canHom(M)) as LeftMod of R;
set f = rho(M);
for y being object st y in the carrier of EM
ex x being object st x in the carrier of M & y = f.x
proof
let y be object;
assume y in the carrier of EM; then
consider x be object such that
A6: x = y & x in the carrier of M;
reconsider x0 = x as Element of the carrier of M by A6;
f.x0 = x0;
hence thesis by A6;
end;
hence thesis by FUNCT_2:10;
end;
theorem
for R be comRing,M be LeftMod of R holds
M ~= AbGrLMod(AbGr(M),canHom(M))
proof
let R be comRing, M be LeftMod of R;
A1: rho(M) is Homomorphism of R,M,AbGrLMod(AbGr(M),canHom(M)) by Def10;
rho(M) is one-to-one onto by Th38;
hence thesis by A1;
end;