let I be non empty set ; for G being Group
for M being DirectSumComponents of G,I ex f being Homomorphism of (sum M),G ex N being internal DirectSumComponents of G,I st
( f is bijective & ( for i being Element of I ex qi being Homomorphism of (M . i),(N . i) st
( qi = f * (1ProdHom (M,i)) & qi is bijective ) ) )
let G be Group; for M being DirectSumComponents of G,I ex f being Homomorphism of (sum M),G ex N being internal DirectSumComponents of G,I st
( f is bijective & ( for i being Element of I ex qi being Homomorphism of (M . i),(N . i) st
( qi = f * (1ProdHom (M,i)) & qi is bijective ) ) )
let M be DirectSumComponents of G,I; ex f being Homomorphism of (sum M),G ex N being internal DirectSumComponents of G,I st
( f is bijective & ( for i being Element of I ex qi being Homomorphism of (M . i),(N . i) st
( qi = f * (1ProdHom (M,i)) & qi is bijective ) ) )
consider f being Homomorphism of (sum M),G such that
A1:
f is bijective
by GROUP_19:def 8;
deffunc H1( Element of I) -> Subgroup of G = f .: (ProjGroup (M,$1));
consider N being Function such that
A2:
dom N = I
and
A3:
for i being Element of I st i in I holds
N . i = H1(i)
from CLASSES1:sch 2();
A4:
for i being object st i in I holds
N . i is strict Subgroup of G
then
for i being object st i in I holds
N . i is Group
;
then reconsider N = N as Group-Family of I by A2, GROUP_19:2;
for i being object st i in I holds
N . i is Subgroup of G
by A4;
then reconsider N = N as Subgroup-Family of I,G by Def1;
A5:
for i being Element of I holds N . i is Subgroup of G
by A4;
deffunc H2( Element of I) -> Element of K19(K20( the carrier of (M . $1), the carrier of G)) = f * (1ProdHom (M,$1));
consider q being Function such that
A6:
dom q = I
and
A7:
for i being Element of I st i in I holds
q . i = H2(i)
from CLASSES1:sch 2();
reconsider q = q as non empty Function by A6;
A8:
now for i being Element of I ex qi being Homomorphism of (M . i),(N . i) st
( qi = q . i & qi is bijective )let i be
Element of
I;
ex qi being Homomorphism of (M . i),(N . i) st
( qi = q . i & qi is bijective )A9:
rng (1ProdHom (M,i)) = [#] (ProjGroup (M,i))
by FUNCT_2:def 3;
reconsider fi =
f | (ProjGroup (M,i)) as
Homomorphism of
(ProjGroup (M,i)),
G ;
dom fi = [#] (ProjGroup (M,i))
by FUNCT_2:def 1;
then A10:
f * (1ProdHom (M,i)) = fi * (1ProdHom (M,i))
by A9, RELAT_1:165;
A11:
rng fi =
f .: ([#] (ProjGroup (M,i)))
by RELAT_1:115
.=
[#] (f .: (ProjGroup (M,i)))
by GRSOLV_1:8
.=
[#] (N . i)
by A3
;
Image fi =
f .: (ProjGroup (M,i))
.=
N . i
by A3
;
then reconsider fi =
fi as
Homomorphism of
(ProjGroup (M,i)),
(N . i) by GROUP_6:49;
A12:
fi is
one-to-one
by A1, FUNCT_1:52;
A13:
fi is
onto
by A11, FUNCT_2:def 3;
reconsider qi =
fi * (1ProdHom (M,i)) as
Homomorphism of
(M . i),
(N . i) ;
take qi =
qi;
( qi = q . i & qi is bijective )thus
qi = q . i
by A7, A10;
qi is bijective thus
qi is
bijective
by A12, A13, GROUP_6:64;
verum end;
then A14:
for i being Element of I ex qi being Homomorphism of (M . i),(N . i) st
( qi = q . i & qi is bijective )
;
reconsider r = SumMap (M,N,q) as Homomorphism of (sum M),(sum N) ;
A15:
r is bijective
by A6, A14, GROUP_19:41;
reconsider s = r " as Homomorphism of (sum N),(sum M) by A6, A14, GROUP_19:41, GROUP_6:62;
A16:
s is bijective
by A15, GROUP_6:63;
reconsider g = f * s as Function ;
reconsider g = g as Homomorphism of (sum N),G ;
A17:
g is bijective
by A1, A16, GROUP_6:64;
then reconsider N = N as DirectSumComponents of G,I by GROUP_19:def 8;
for i being Element of I
for n being Element of (N . i) holds g . ((1ProdHom (N,i)) . n) = n
proof
let i be
Element of
I;
for n being Element of (N . i) holds g . ((1ProdHom (N,i)) . n) = nlet n be
Element of
(N . i);
g . ((1ProdHom (N,i)) . n) = n
consider qi being
Homomorphism of
(M . i),
(N . i) such that A18:
qi = q . i
and A19:
qi is
bijective
by A8;
A20:
dom qi = [#] (M . i)
by FUNCT_2:def 1;
rng qi = [#] (N . i)
by A19, FUNCT_2:def 3;
then consider m being
object such that A21:
m in [#] (M . i)
and A22:
qi . m = n
by A20, FUNCT_1:def 3;
reconsider m =
m as
Element of
(M . i) by A21;
for
i being
Element of
I holds
q . i is
Homomorphism of
(M . i),
(N . i)
then A24:
r . ((1ProdHom (M,i)) . m) = (1ProdHom (N,i)) . n
by A6, A18, A22, GROUP_19:42;
A25:
dom r = [#] (sum M)
by FUNCT_2:def 1;
(1ProdHom (M,i)) . m in ProjGroup (
M,
i)
;
then A26:
(1ProdHom (M,i)) . m in sum M
by GROUP_2:40;
A27:
dom s = [#] (sum N)
by FUNCT_2:def 1;
(1ProdHom (N,i)) . n in ProjGroup (
N,
i)
;
then A28:
(1ProdHom (N,i)) . n in sum N
by GROUP_2:40;
A29:
qi = f * (1ProdHom (M,i))
by A7, A18;
A30:
m in dom (1ProdHom (M,i))
by A21, FUNCT_2:def 1;
g . ((1ProdHom (N,i)) . n) =
f . (s . ((1ProdHom (N,i)) . n))
by A27, A28, FUNCT_1:13
.=
f . ((1ProdHom (M,i)) . m)
by A15, A24, A25, A26, FUNCT_1:34
.=
n
by A22, A29, A30, FUNCT_1:13
;
hence
g . ((1ProdHom (N,i)) . n) = n
;
verum
end;
then
for a being finite-support Function of I,G st a in sum N holds
g . a = Product a
by Th19;
then reconsider N = N as internal DirectSumComponents of G,I by A5, A17, GROUP_19:def 9;
take
f
; ex N being internal DirectSumComponents of G,I st
( f is bijective & ( for i being Element of I ex qi being Homomorphism of (M . i),(N . i) st
( qi = f * (1ProdHom (M,i)) & qi is bijective ) ) )
take
N
; ( f is bijective & ( for i being Element of I ex qi being Homomorphism of (M . i),(N . i) st
( qi = f * (1ProdHom (M,i)) & qi is bijective ) ) )
for i being Element of I ex qi being Homomorphism of (M . i),(N . i) st
( qi = f * (1ProdHom (M,i)) & qi is bijective )
hence
( f is bijective & ( for i being Element of I ex qi being Homomorphism of (M . i),(N . i) st
( qi = f * (1ProdHom (M,i)) & qi is bijective ) ) )
by A1; verum