begin
Lm1:
1 in {1,2}
by TARSKI:def 2;
Lm2:
2 in {1,2}
by TARSKI:def 2;
theorem Th1:
definition
let G1,
G2,
H1,
H2 be non
empty multMagma ;
let f be
Function of
G1,
H1;
let g be
Function of
G2,
H2;
func Gr2Iso f,
g -> Function of
(product <*G1,G2*>),
(product <*H1,H2*>) means :
Def1:
for
x being
Element of
(product <*G1,G2*>) ex
x1 being
Element of
G1 ex
x2 being
Element of
G2 st
(
x = <*x1,x2*> &
it . x = <*(f . x1),(g . x2)*> );
existence
ex b1 being Function of (product <*G1,G2*>),(product <*H1,H2*>) st
for x being Element of (product <*G1,G2*>) ex x1 being Element of G1 ex x2 being Element of G2 st
( x = <*x1,x2*> & b1 . x = <*(f . x1),(g . x2)*> )
uniqueness
for b1, b2 being Function of (product <*G1,G2*>),(product <*H1,H2*>) st ( for x being Element of (product <*G1,G2*>) ex x1 being Element of G1 ex x2 being Element of G2 st
( x = <*x1,x2*> & b1 . x = <*(f . x1),(g . x2)*> ) ) & ( for x being Element of (product <*G1,G2*>) ex x1 being Element of G1 ex x2 being Element of G2 st
( x = <*x1,x2*> & b2 . x = <*(f . x1),(g . x2)*> ) ) holds
b1 = b2
end;
:: deftheorem Def1 defines Gr2Iso TOPALG_4:def 1 :
for
G1,
G2,
H1,
H2 being non
empty multMagma for
f being
Function of
G1,
H1 for
g being
Function of
G2,
H2 for
b7 being
Function of
(product <*G1,G2*>),
(product <*H1,H2*>) holds
(
b7 = Gr2Iso f,
g iff for
x being
Element of
(product <*G1,G2*>) ex
x1 being
Element of
G1 ex
x2 being
Element of
G2 st
(
x = <*x1,x2*> &
b7 . x = <*(f . x1),(g . x2)*> ) );
theorem
definition
let G1,
G2,
H1,
H2 be
Group;
let f be
Homomorphism of
G1,
H1;
let g be
Homomorphism of
G2,
H2;
Gr2Isoredefine func Gr2Iso f,
g -> Homomorphism of
(product <*G1,G2*>),
(product <*H1,H2*>);
coherence
Gr2Iso f,g is Homomorphism of (product <*G1,G2*>),(product <*H1,H2*>)
end;
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
begin
set I = the carrier of I[01] ;
reconsider j0 = 0 , j1 = 1 as Point of I[01] by BORSUK_1:def 17, BORSUK_1:def 18;
theorem Th7:
theorem Th8:
definition
let S,
T,
Y be non
empty TopSpace;
let f be
Function of
Y,
S;
let g be
Function of
Y,
T;
<:redefine func <:f,g:> -> Function of
Y,
[:S,T:];
coherence
<:f,g:> is Function of Y,[:S,T:]
end;
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
for
S,
T being non
empty TopSpace for
s1,
s2 being
Point of
S for
t1,
t2 being
Point of
T st
[s1,t1],
[s2,t2] are_connected holds
for
L being
Path of
[s1,t1],
[s2,t2] holds
pr1 L is
Path of
s1,
s2
theorem Th14:
for
S,
T being non
empty TopSpace for
s1,
s2 being
Point of
S for
t1,
t2 being
Point of
T st
[s1,t1],
[s2,t2] are_connected holds
for
L being
Path of
[s1,t1],
[s2,t2] holds
pr2 L is
Path of
t1,
t2
theorem Th15:
theorem Th16:
for
S,
T being non
empty TopSpace for
s1,
s2 being
Point of
S for
t1,
t2 being
Point of
T st
s1,
s2 are_connected &
t1,
t2 are_connected holds
for
L1 being
Path of
s1,
s2 for
L2 being
Path of
t1,
t2 holds
<:L1,L2:> is
Path of
[s1,t1],
[s2,t2]
definition
let S,
T be non
empty arcwise_connected TopSpace;
let s1,
s2 be
Point of
S;
let t1,
t2 be
Point of
T;
let L1 be
Path of
s1,
s2;
let L2 be
Path of
t1,
t2;
<:redefine func <:L1,L2:> -> Path of
[s1,t1],
[s2,t2];
coherence
<:L1,L2:> is Path of [s1,t1],[s2,t2]
end;
definition
let S,
T be non
empty arcwise_connected TopSpace;
let s1,
s2 be
Point of
S;
let t1,
t2 be
Point of
T;
let L be
Path of
[s1,t1],
[s2,t2];
pr1redefine func pr1 L -> Path of
s1,
s2;
coherence
pr1 L is Path of s1,s2
pr2redefine func pr2 L -> Path of
t1,
t2;
coherence
pr2 L is Path of t1,t2
end;
Lm3:
for S, T being non empty TopSpace
for s1, s2 being Point of S
for t1, t2 being Point of T
for l1, l2 being Path of [s1,t1],[s2,t2]
for H being Homotopy of l1,l2 st l1,l2 are_homotopic holds
( pr1 H is continuous & ( for a being Point of I[01] holds
( (pr1 H) . a,0 = (pr1 l1) . a & (pr1 H) . a,1 = (pr1 l2) . a & ( for b being Point of I[01] holds
( (pr1 H) . 0 ,b = s1 & (pr1 H) . 1,b = s2 ) ) ) ) )
Lm4:
for S, T being non empty TopSpace
for s1, s2 being Point of S
for t1, t2 being Point of T
for l1, l2 being Path of [s1,t1],[s2,t2]
for H being Homotopy of l1,l2 st l1,l2 are_homotopic holds
( pr2 H is continuous & ( for a being Point of I[01] holds
( (pr2 H) . a,0 = (pr2 l1) . a & (pr2 H) . a,1 = (pr2 l2) . a & ( for b being Point of I[01] holds
( (pr2 H) . 0 ,b = t1 & (pr2 H) . 1,b = t2 ) ) ) ) )
theorem
for
S,
T being non
empty TopSpace for
s1,
s2 being
Point of
S for
t1,
t2 being
Point of
T for
l1,
l2 being
Path of
[s1,t1],
[s2,t2] for
H being
Homotopy of
l1,
l2 for
p,
q being
Path of
s1,
s2 st
p = pr1 l1 &
q = pr1 l2 &
l1,
l2 are_homotopic holds
pr1 H is
Homotopy of
p,
q
theorem
for
S,
T being non
empty TopSpace for
s1,
s2 being
Point of
S for
t1,
t2 being
Point of
T for
l1,
l2 being
Path of
[s1,t1],
[s2,t2] for
H being
Homotopy of
l1,
l2 for
p,
q being
Path of
t1,
t2 st
p = pr2 l1 &
q = pr2 l2 &
l1,
l2 are_homotopic holds
pr2 H is
Homotopy of
p,
q
theorem Th19:
for
S,
T being non
empty TopSpace for
s1,
s2 being
Point of
S for
t1,
t2 being
Point of
T for
l1,
l2 being
Path of
[s1,t1],
[s2,t2] for
p,
q being
Path of
s1,
s2 st
p = pr1 l1 &
q = pr1 l2 &
l1,
l2 are_homotopic holds
p,
q are_homotopic
theorem Th20:
for
S,
T being non
empty TopSpace for
s1,
s2 being
Point of
S for
t1,
t2 being
Point of
T for
l1,
l2 being
Path of
[s1,t1],
[s2,t2] for
p,
q being
Path of
t1,
t2 st
p = pr2 l1 &
q = pr2 l2 &
l1,
l2 are_homotopic holds
p,
q are_homotopic
Lm5:
for S, T being non empty TopSpace
for s1, s2 being Point of S
for t1, t2 being Point of T
for l1, l2 being Path of [s1,t1],[s2,t2]
for p, q being Path of s1,s2
for x, y being Path of t1,t2
for f being Homotopy of p,q
for g being Homotopy of x,y st p = pr1 l1 & q = pr1 l2 & x = pr2 l1 & y = pr2 l2 & p,q are_homotopic & x,y are_homotopic holds
( <:f,g:> is continuous & ( for a being Point of I[01] holds
( <:f,g:> . a,0 = l1 . a & <:f,g:> . a,1 = l2 . a & ( for b being Point of I[01] holds
( <:f,g:> . 0 ,b = [s1,t1] & <:f,g:> . 1,b = [s2,t2] ) ) ) ) )
theorem
for
S,
T being non
empty TopSpace for
s1,
s2 being
Point of
S for
t1,
t2 being
Point of
T for
l1,
l2 being
Path of
[s1,t1],
[s2,t2] for
p,
q being
Path of
s1,
s2 for
x,
y being
Path of
t1,
t2 for
f being
Homotopy of
p,
q for
g being
Homotopy of
x,
y st
p = pr1 l1 &
q = pr1 l2 &
x = pr2 l1 &
y = pr2 l2 &
p,
q are_homotopic &
x,
y are_homotopic holds
<:f,g:> is
Homotopy of
l1,
l2
theorem Th22:
for
S,
T being non
empty TopSpace for
s1,
s2 being
Point of
S for
t1,
t2 being
Point of
T for
l1,
l2 being
Path of
[s1,t1],
[s2,t2] for
p,
q being
Path of
s1,
s2 for
x,
y being
Path of
t1,
t2 st
p = pr1 l1 &
q = pr1 l2 &
x = pr2 l1 &
y = pr2 l2 &
p,
q are_homotopic &
x,
y are_homotopic holds
l1,
l2 are_homotopic
theorem Th23:
for
S,
T being non
empty TopSpace for
s1,
s2,
s3 being
Point of
S for
t1,
t2,
t3 being
Point of
T for
l1 being
Path of
[s1,t1],
[s2,t2] for
l2 being
Path of
[s2,t2],
[s3,t3] for
p1 being
Path of
s1,
s2 for
p2 being
Path of
s2,
s3 st
[s1,t1],
[s2,t2] are_connected &
[s2,t2],
[s3,t3] are_connected &
p1 = pr1 l1 &
p2 = pr1 l2 holds
pr1 (l1 + l2) = p1 + p2
theorem
for
S,
T being non
empty arcwise_connected TopSpace for
s1,
s2,
s3 being
Point of
S for
t1,
t2,
t3 being
Point of
T for
l1 being
Path of
[s1,t1],
[s2,t2] for
l2 being
Path of
[s2,t2],
[s3,t3] holds
pr1 (l1 + l2) = (pr1 l1) + (pr1 l2)
theorem Th25:
for
S,
T being non
empty TopSpace for
s1,
s2,
s3 being
Point of
S for
t1,
t2,
t3 being
Point of
T for
l1 being
Path of
[s1,t1],
[s2,t2] for
l2 being
Path of
[s2,t2],
[s3,t3] for
p1 being
Path of
t1,
t2 for
p2 being
Path of
t2,
t3 st
[s1,t1],
[s2,t2] are_connected &
[s2,t2],
[s3,t3] are_connected &
p1 = pr2 l1 &
p2 = pr2 l2 holds
pr2 (l1 + l2) = p1 + p2
theorem
for
S,
T being non
empty arcwise_connected TopSpace for
s1,
s2,
s3 being
Point of
S for
t1,
t2,
t3 being
Point of
T for
l1 being
Path of
[s1,t1],
[s2,t2] for
l2 being
Path of
[s2,t2],
[s3,t3] holds
pr2 (l1 + l2) = (pr2 l1) + (pr2 l2)
definition
let S,
T be non
empty TopSpace;
let s be
Point of
S;
let t be
Point of
T;
set pS =
pi_1 [:S,T:],
[s,t];
set G =
<*(pi_1 S,s),(pi_1 T,t)*>;
set pT =
product <*(pi_1 S,s),(pi_1 T,t)*>;
func FGPrIso s,
t -> Function of
(pi_1 [:S,T:],[s,t]),
(product <*(pi_1 S,s),(pi_1 T,t)*>) means :
Def2:
for
x being
Point of
(pi_1 [:S,T:],[s,t]) ex
l being
Loop of
[s,t] st
(
x = Class (EqRel [:S,T:],[s,t]),
l &
it . x = <*(Class (EqRel S,s),(pr1 l)),(Class (EqRel T,t),(pr2 l))*> );
existence
ex b1 being Function of (pi_1 [:S,T:],[s,t]),(product <*(pi_1 S,s),(pi_1 T,t)*>) st
for x being Point of (pi_1 [:S,T:],[s,t]) ex l being Loop of [s,t] st
( x = Class (EqRel [:S,T:],[s,t]),l & b1 . x = <*(Class (EqRel S,s),(pr1 l)),(Class (EqRel T,t),(pr2 l))*> )
uniqueness
for b1, b2 being Function of (pi_1 [:S,T:],[s,t]),(product <*(pi_1 S,s),(pi_1 T,t)*>) st ( for x being Point of (pi_1 [:S,T:],[s,t]) ex l being Loop of [s,t] st
( x = Class (EqRel [:S,T:],[s,t]),l & b1 . x = <*(Class (EqRel S,s),(pr1 l)),(Class (EqRel T,t),(pr2 l))*> ) ) & ( for x being Point of (pi_1 [:S,T:],[s,t]) ex l being Loop of [s,t] st
( x = Class (EqRel [:S,T:],[s,t]),l & b2 . x = <*(Class (EqRel S,s),(pr1 l)),(Class (EqRel T,t),(pr2 l))*> ) ) holds
b1 = b2
end;
:: deftheorem Def2 defines FGPrIso TOPALG_4:def 2 :
for
S,
T being non
empty TopSpace for
s being
Point of
S for
t being
Point of
T for
b5 being
Function of
(pi_1 [:S,T:],[s,t]),
(product <*(pi_1 S,s),(pi_1 T,t)*>) holds
(
b5 = FGPrIso s,
t iff for
x being
Point of
(pi_1 [:S,T:],[s,t]) ex
l being
Loop of
[s,t] st
(
x = Class (EqRel [:S,T:],[s,t]),
l &
b5 . x = <*(Class (EqRel S,s),(pr1 l)),(Class (EqRel T,t),(pr2 l))*> ) );
theorem Th27:
for
S,
T being non
empty TopSpace for
s being
Point of
S for
t being
Point of
T for
x being
Point of
(pi_1 [:S,T:],[s,t]) for
l being
Loop of
[s,t] st
x = Class (EqRel [:S,T:],[s,t]),
l holds
(FGPrIso s,t) . x = <*(Class (EqRel S,s),(pr1 l)),(Class (EqRel T,t),(pr2 l))*>
theorem Th28:
for
S,
T being non
empty TopSpace for
s being
Point of
S for
t being
Point of
T for
l being
Loop of
[s,t] holds
(FGPrIso s,t) . (Class (EqRel [:S,T:],[s,t]),l) = <*(Class (EqRel S,s),(pr1 l)),(Class (EqRel T,t),(pr2 l))*>
definition
let S,
T be non
empty TopSpace;
let s be
Point of
S;
let t be
Point of
T;
FGPrIsoredefine func FGPrIso s,
t -> Homomorphism of
(pi_1 [:S,T:],[s,t]),
(product <*(pi_1 S,s),(pi_1 T,t)*>);
coherence
FGPrIso s,t is Homomorphism of (pi_1 [:S,T:],[s,t]),(product <*(pi_1 S,s),(pi_1 T,t)*>)
end;
theorem Th29:
theorem Th30:
theorem
for
S,
T being non
empty TopSpace for
s1,
s2 being
Point of
S for
t1,
t2 being
Point of
T for
f being
Homomorphism of
(pi_1 S,s1),
(pi_1 S,s2) for
g being
Homomorphism of
(pi_1 T,t1),
(pi_1 T,t2) st
f is
bijective &
g is
bijective holds
(Gr2Iso f,g) * (FGPrIso s1,t1) is
bijective
theorem
for
S,
T being non
empty arcwise_connected TopSpace for
s1,
s2 being
Point of
S for
t1,
t2 being
Point of
T holds
pi_1 [:S,T:],
[s1,t1],
product <*(pi_1 S,s2),(pi_1 T,t2)*> are_isomorphic