:: TOPALG_4 semantic presentation

Lm1: 1 in {1,2}
by TARSKI:def 2;

Lm2: 2 in {1,2}
by TARSKI:def 2;

theorem Th1: :: TOPALG_4:1

for G, H being non empty HGrStr
for x being Element of (product <*G,H*>) ex g being Element of G ex h being Element of H st x = <*g,h*>

proof end;

definition

let G1, G2, H1, H2 be non empty HGrStr ;
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: :: TOPALG_4:def 1
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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines Gr2Iso TOPALG_4:def 1 :

theorem :: TOPALG_4:2

for G1, G2, H1, H2 being non empty HGrStr
for f being Function of G1,H1
for g being Function of G2,H2
for x1 being Element of G1
for x2 being Element of G2 holds (Gr2Iso f,g) . <*x1,x2*> = <*(f . x1),(g . x2)*>

proof end;

definition

let G1, G2, H1, H2 be Group;
let f be Homomorphism of G1,H1;
let g be Homomorphism of G2,H2;
:: original: Gr2Iso
redefine func Gr2Iso f,g -> Homomorphism of (product <*G1,G2*>),(product <*H1,H2*>);
coherence

proof end;

end;

theorem Th3: :: TOPALG_4:3

for G1, G2, H1, H2 being non empty HGrStr
for f being Function of G1,H1
for g being Function of G2,H2 st f is one-to-one & g is one-to-one holds
Gr2Iso f,g is one-to-one

proof end;

theorem Th4: :: TOPALG_4:4

for G1, G2, H1, H2 being non empty HGrStr
for f being Function of G1,H1
for g being Function of G2,H2 st f is onto & g is onto holds
Gr2Iso f,g is onto

proof end;

theorem Th5: :: TOPALG_4:5

for G1, G2, H1, H2 being Group
for f being Homomorphism of G1,H1
for g being Homomorphism of G2,H2 st f is being_isomorphism & g is being_isomorphism holds
Gr2Iso f,g is being_isomorphism

proof end;

theorem Th6: :: TOPALG_4:6

for G1, G2, H1, H2 being Group st G1,H1 are_isomorphic & G2,H2 are_isomorphic holds
product <*G1,G2*>, product <*H1,H2*> are_isomorphic

proof end;

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: :: TOPALG_4:7

for f, g being Function st dom f = dom g holds
pr1 <:f,g:> = f

proof end;

theorem Th8: :: TOPALG_4:8

for f, g being Function st dom f = dom g holds
pr2 <:f,g:> = g

proof end;

definition

let S, T, Y be non empty TopSpace;
let f be Function of Y,S;
let g be Function of Y,T;
:: original: <:
redefine func <:f,g:> -> Function of Y,[:S,T:];
coherence

proof end;

end;

definition

let S, T, Y be non empty TopSpace;
let f be Function of Y,[:S,T:];
:: original: pr1
redefine func pr1 f -> Function of Y,S;
coherence

proof end;

:: original: pr2
redefine func pr2 f -> Function of Y,T;
coherence

proof end;

end;

theorem Th9: :: TOPALG_4:9

for Y, S, T being non empty TopSpace
for f being continuous Function of Y,[:S,T:] holds pr1 f is continuous

proof end;

theorem Th10: :: TOPALG_4:10

for Y, S, T being non empty TopSpace
for f being continuous Function of Y,[:S,T:] holds pr2 f is continuous

proof end;

theorem Th11: :: TOPALG_4:11

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
s1,s2 are_connected

proof end;

theorem Th12: :: TOPALG_4:12

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
t1,t2 are_connected

proof end;

theorem Th13: :: TOPALG_4:13

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

proof end;

theorem Th14: :: TOPALG_4:14

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

proof end;

theorem Th15: :: TOPALG_4:15

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
[s1,t1],[s2,t2] are_connected

proof end;

theorem Th16: :: TOPALG_4:16

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]

proof 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 L1 be Path of s1,s2;
let L2 be Path of t1,t2;
:: original: <:
redefine func <:L1,L2:> -> Path of [s1,t1],[s2,t2];
coherence

proof end;

end;

definition

let S, T be non empty TopSpace;
let s be Point of S;
let t be Point of T;
let L1 be Loop of s;
let L2 be Loop of t;
:: original: <:
redefine func <:L1,L2:> -> Loop of [s,t];
coherence by Th16;

end;

registration

let S, T be non empty arcwise_connected TopSpace;
cluster [:S,T:] -> arcwise_connected ;
coherence

proof end;

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];
:: original: pr1
redefine func pr1 L -> Path of s1,s2;
coherence

proof end;

:: original: pr2
redefine func pr2 L -> Path of t1,t2;
coherence

proof end;

end;

definition

let S, T be non empty TopSpace;
let s be Point of S;
let t be Point of T;
let L be Loop of [s,t];
:: original: pr1
redefine func pr1 L -> Loop of s;
coherence by Th13;
:: original: pr2
redefine func pr2 L -> Loop of t;
coherence by Th14;

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 ) ) ) ) )

proof end;

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 ) ) ) ) )

proof end;

theorem :: TOPALG_4:17

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

proof end;

theorem :: TOPALG_4:18

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

proof end;

theorem Th19: :: TOPALG_4:19

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

proof end;

theorem Th20: :: TOPALG_4:20

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

proof end;

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] ) ) ) ) )

proof end;

theorem :: TOPALG_4:21

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

proof end;

theorem Th22: :: TOPALG_4:22

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

proof end;

theorem Th23: :: TOPALG_4:23

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

proof end;

theorem :: TOPALG_4:24

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)

proof end;

theorem Th25: :: TOPALG_4:25

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

proof end;

theorem :: TOPALG_4:26

proof end;

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: :: TOPALG_4:def 2
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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines FGPrIso TOPALG_4:def 2 :

theorem Th27: :: TOPALG_4:27

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))*>

proof end;

theorem Th28: :: TOPALG_4:28

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))*>

proof end;

registration

let S, T be non empty TopSpace;
let s be Point of S;
let t be Point of T;
cluster FGPrIso s,t -> one-to-one onto ;
coherence

proof end;

end;

definition

let S, T be non empty TopSpace;
let s be Point of S;
let t be Point of T;
:: original: FGPrIso
redefine func FGPrIso s,t -> Homomorphism of (pi_1 [:S,T:],[s,t]),(product <*(pi_1 S,s),(pi_1 T,t)*>);
coherence

proof end;

end;

theorem Th29: :: TOPALG_4:29

for S, T being non empty TopSpace
for s being Point of S
for t being Point of T holds FGPrIso s,t is being_isomorphism

proof end;

theorem Th30: :: TOPALG_4:30

for S, T being non empty TopSpace
for s being Point of S
for t being Point of T holds pi_1 [:S,T:],[s,t], product <*(pi_1 S,s),(pi_1 T,t)*> are_isomorphic

proof end;

theorem :: TOPALG_4:31

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 being_isomorphism & g is being_isomorphism holds
(Gr2Iso f,g) * (FGPrIso s1,t1) is being_isomorphism

proof end;

theorem :: TOPALG_4:32

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

proof end;