let R be comRing; for M being LeftMod of R holds Hom (R,(LeftModule R),M) ~= M
let M be LeftMod of R; Hom (R,(LeftModule R),M) ~= M
reconsider R1 = LeftModule R as LeftMod of R ;
reconsider m1 = 1. R as Element of R1 ;
deffunc H1( Element of Funcs ( the carrier of R1, the carrier of M)) -> Element of the carrier of M = $1 . m1;
consider G being Function of (Funcs ( the carrier of R1, the carrier of M)),M such that
A1:
for x being Element of Funcs ( the carrier of R1, the carrier of M) holds G . x = H1(x)
from FUNCT_2:sch 4();
A2:
for f, g being 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);
G . ((ADD (R1,M)) . (f,g)) = (G . f) + (G . g)
set h =
(ADD (R1,M)) . (
f,
g);
(
G . ((ADD (R1,M)) . (f,g)) = ((ADD (R1,M)) . (f,g)) . m1 &
G . f = f . m1 &
G . g = g . m1 )
by A1;
hence
G . ((ADD (R1,M)) . (f,g)) = (G . f) + (G . g)
by Th15;
verum
end;
A3:
for f being Element of Funcs ( the carrier of R1, the carrier of M)
for a being 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);
for a being Element of R holds G . ((LMULT (R1,M)) . [a,f]) = a * (G . f)let a be
Element of
R;
G . ((LMULT (R1,M)) . [a,f]) = a * (G . f)
set h =
(LMULT (R1,M)) . [a,f];
(
G . ((LMULT (R1,M)) . [a,f]) = ((LMULT (R1,M)) . [a,f]) . m1 &
G . f = f . m1 )
by A1;
hence
G . ((LMULT (R1,M)) . [a,f]) = a * (G . f)
by Th16;
verum
end;
set H = Hom (R,R1,M);
set caH = the carrier of (Hom (R,R1,M));
set G1 = G | the carrier of (Hom (R,R1,M));
A4:
dom G = Funcs ( the carrier of R1, the carrier of M)
by FUNCT_2:def 1;
A5: dom (G | the carrier of (Hom (R,R1,M))) =
the carrier of (Hom (R,R1,M)) /\ (dom G)
by RELAT_1:61
.=
the carrier of (Hom (R,R1,M))
by A4, XBOOLE_1:28
;
A6:
for y being object st y in rng (G | the carrier of (Hom (R,R1,M))) holds
y in the carrier of M
proof
let y be
object ;
( y in rng (G | the carrier of (Hom (R,R1,M))) implies y in the carrier of M )
assume
y in rng (G | the carrier of (Hom (R,R1,M)))
;
y in the carrier of M
then consider x being
object such that A8:
(
x in dom (G | the carrier of (Hom (R,R1,M))) &
y = (G | the carrier of (Hom (R,R1,M))) . x )
by FUNCT_1:def 3;
G . x in the
carrier of
M
by FUNCT_2:5, A8;
hence
y in the
carrier of
M
by A8, FUNCT_1:49, A5;
verum
end;
reconsider G1 = G | the carrier of (Hom (R,R1,M)) as Function of (Hom (R,R1,M)),M by A5, A6, TARSKI:def 3, FUNCT_2:2;
A10:
for f, g being 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));
G1 . (f + g) = (G1 . f) + (G1 . g)
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 the
carrier of
(Hom (R,R1,M))
;
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
G1 . (f + g) = (G1 . f) + (G1 . g)
;
verum
end;
A15:
G1 is additive
by A10;
for f being Element of (Hom (R,R1,M))
for a being Element of R holds G1 . (a * f) = a * (G1 . f)
proof
let f be
Element of
(Hom (R,R1,M));
for a being Element of R holds G1 . (a * f) = a * (G1 . f)let a be
Element of
R;
G1 . (a * f) = a * (G1 . f)
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 the
carrier of
(Hom (R,R1,M))
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
G1 . (a * f) = a * (G1 . f)
;
verum
end;
then
G1 is homogeneous
;
then reconsider G1 = G1 as Homomorphism of R, Hom (R,R1,M),M by A15, Def10;
A19:
ker G1 = {(0. (Hom (R,R1,M)))}
proof
G1 . (0. (Hom (R,R1,M))) =
G1 . ((0. (Hom (R,R1,M))) + (0. (Hom (R,R1,M))))
by RLVECT_1:4
.=
(G1 . (0. (Hom (R,R1,M)))) + (G1 . (0. (Hom (R,R1,M))))
by A10
;
then
G1 . (0. (Hom (R,R1,M))) = 0. M
by RLVECT_1:9;
then
0. (Hom (R,R1,M)) in ker G1
;
then A20:
for
f being
object st
f in {(0. (Hom (R,R1,M)))} holds
f in ker G1
by TARSKI:def 1;
for
f being
object st
f in ker G1 holds
f in {(0. (Hom (R,R1,M)))}
proof
let f be
object ;
( f in ker G1 implies f in {(0. (Hom (R,R1,M)))} )
assume
f in ker G1
;
f in {(0. (Hom (R,R1,M)))}
then consider f1 being
Element of
set_Hom (
R1,
M)
such that A22:
(
f1 = f &
G1 . f1 = 0. M )
;
reconsider f1 =
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 being
Element of
R1 holds
f0 . a = 0. M
then
f0 = R1 --> (0. M)
;
then
f0 = ZeroMap (
R1,
M)
by GRCAT_1:def 7;
hence
f in {(0. (Hom (R,R1,M)))}
by A22, TARSKI:def 1;
verum
end;
hence
ker G1 = {(0. (Hom (R,R1,M)))}
by A20, TARSKI:2;
verum
end;
for y being object st y in the carrier of M holds
y in rng G1
proof
let y be
object ;
( y in the carrier of M implies y in rng G1 )
assume
y in the
carrier of
M
;
y in rng G1
then reconsider y0 =
y as
Element of
M ;
defpred S1[
object ,
object ]
means ex
x1 being
object st
(
x1 in the
carrier of
R &
x1 = $1 & ex
x0 being
Element of
R st
(
x0 = x1 & $2
= x0 * y0 ) );
A26:
for
x being
object st
x in the
carrier of
R1 holds
ex
y being
object st
(
y in the
carrier of
M &
S1[
x,
y] )
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
S1[
z,
h . z]
from FUNCT_2:sch 1(A26);
for
a,
b being
Element of
R1 holds
h . (a + b) = (h . a) + (h . b)
then A37:
h is
additive
;
for
a being
Element of
R for
b being
Element of
R1 holds
h . (a * b) = a * (h . b)
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 being
object such that A45:
(
m in the
carrier of
R &
m1 = m & ex
m0 being
Element of
R st
(
m0 = m &
h . m1 = m0 * y0 ) )
by A29;
reconsider n1 =
m1 as
Element of
R ;
h0 in the
carrier of
(Hom (R,R1,M))
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
y in rng G1
by A47, FUNCT_1:def 3;
verum
end;
then
G1 is onto
by A6, TARSKI:2;
hence
Hom (R,(LeftModule R),M) ~= M
by A19, Th13; verum