:: The Fundamental Group
:: by Artur Korni{\l}owicz , Yasunari Shidama and Adam Grabowski
::
:: Received March 18, 2004
:: Copyright (c) 2004 Association of Mizar Users

begin

theorem :: TOPALG_1:1

for G, H being set
for g being Function of G,H
for h being Function of H,G st h * g = id G & g * h = id H holds
h is bijective

proof end;

theorem Th2: :: TOPALG_1:2

for X being Subset of I[01]
for a being Point of I[01] st X = ].a,1.] holds
X ` = [.0,a.]

proof end;

theorem Th3: :: TOPALG_1:3

for X being Subset of I[01]
for a being Point of I[01] st X = [.0,a.[ holds
X ` = [.a,1.]

proof end;

theorem Th4: :: TOPALG_1:4

for X being Subset of I[01]
for a being Point of I[01] st X = ].a,1.] holds
X is open

proof end;

theorem Th5: :: TOPALG_1:5

for X being Subset of I[01]
for a being Point of I[01] st X = [.0,a.[ holds
X is open

proof end;

theorem :: TOPALG_1:6

for x being real number
for f being real-valued FinSequence holds x * (- f) = - (x * f)

proof end;

theorem Th7: :: TOPALG_1:7

for x being real number
for f, g being real-valued FinSequence holds x * (f - g) = (x * f) - (x * g) by RFUNCT_1:30;

theorem Th8: :: TOPALG_1:8

for x, y being real number
for f being real-valued FinSequence holds (x - y) * f = (x * f) - (y * f)

proof end;

theorem Th9: :: TOPALG_1:9

for f, g, h, k being real-valued FinSequence holds (f + g) - (h + k) = (f - h) + (g - k)

proof end;

theorem Th10: :: TOPALG_1:10

for x being real number
for n being Nat
for f being Element of REAL n st 0 <= x & x <= 1 holds
|.(x * f).| <= |.f.|

proof end;

theorem :: TOPALG_1:11

for n being Nat
for f being Element of REAL n
for p being Point of I[01] holds |.(p * f).| <= |.f.|

proof end;

theorem :: TOPALG_1:12

for x, y being real number
for n being Nat
for e1, e2, e3, e4, e5, e6 being Point of (Euclid n)
for p1, p2, p3, p4 being Point of (TOP-REAL n) st e1 = p1 & e2 = p2 & e3 = p3 & e4 = p4 & e5 = p1 + p3 & e6 = p2 + p4 & dist (e1,e2) < x & dist (e3,e4) < y holds
dist (e5,e6) < x + y

proof end;

theorem Th13: :: TOPALG_1:13

for y, x being real number
for n being Nat
for e1, e2, e5, e6 being Point of (Euclid n)
for p1, p2 being Point of (TOP-REAL n) st e1 = p1 & e2 = p2 & e5 = y * p1 & e6 = y * p2 & dist (e1,e2) < x & y <> 0 holds
dist (e5,e6) < (abs y) * x

proof end;

theorem Th14: :: TOPALG_1:14

for x, y, p, q being real number
for n being Nat
for e1, e2, e3, e4, e5, e6 being Point of (Euclid n)
for p1, p2, p3, p4 being Point of (TOP-REAL n) st e1 = p1 & e2 = p2 & e3 = p3 & e4 = p4 & e5 = (x * p1) + (y * p3) & e6 = (x * p2) + (y * p4) & dist (e1,e2) < p & dist (e3,e4) < q & x <> 0 & y <> 0 holds
dist (e5,e6) < ((abs x) * p) + ((abs y) * q)

proof end;

Lm1: for n being Nat
for X being non empty TopSpace
for f1, f2, g being Function of X,(TOP-REAL n) st f1 is continuous & f2 is continuous & ( for p being Point of X holds g . p = (f1 . p) + (f2 . p) ) holds
g is continuous

proof end;

theorem :: TOPALG_1:15

canceled;

theorem Th16: :: TOPALG_1:16

for y being real number
for n being Nat
for X being non empty TopSpace
for f, g being Function of X,(TOP-REAL n) st f is continuous & ( for p being Point of X holds g . p = y * (f . p) ) holds
g is continuous

proof end;

theorem :: TOPALG_1:17

for x, y being real number
for n being Nat
for X being non empty TopSpace
for f1, f2, g being Function of X,(TOP-REAL n) st f1 is continuous & f2 is continuous & ( for p being Point of X holds g . p = (x * (f1 . p)) + (y * (f2 . p)) ) holds
g is continuous

proof end;

theorem Th18: :: TOPALG_1:18

for n being Nat
for F being Function of [:(TOP-REAL n),I[01]:],(TOP-REAL n) st ( for x being Point of (TOP-REAL n)
for i being Point of I[01] holds F . (x,i) = (1 - i) * x ) holds
F is continuous

proof end;

theorem Th19: :: TOPALG_1:19

for n being Nat
for F being Function of [:(TOP-REAL n),I[01]:],(TOP-REAL n) st ( for x being Point of (TOP-REAL n)
for i being Point of I[01] holds F . (x,i) = i * x ) holds
F is continuous

proof end;

begin

theorem Th20: :: TOPALG_1:20

for X being non empty TopSpace
for a, b, c being Point of X st a,b are_connected & b,c are_connected holds
for A1, A2 being Path of a,b
for B being Path of b,c st A1,A2 are_homotopic holds
A1,(A2 + B) + (- B) are_homotopic

proof end;

theorem :: TOPALG_1:21

for T being non empty pathwise_connected TopSpace
for a1, b1, c1 being Point of T
for A1, A2 being Path of a1,b1
for B being Path of b1,c1 st A1,A2 are_homotopic holds
A1,(A2 + B) + (- B) are_homotopic

proof end;

theorem Th22: :: TOPALG_1:22

for X being non empty TopSpace
for a, b, c being Point of X st a,b are_connected & c,b are_connected holds
for A1, A2 being Path of a,b
for B being Path of c,b st A1,A2 are_homotopic holds
A1,(A2 + (- B)) + B are_homotopic

proof end;

theorem :: TOPALG_1:23

for T being non empty pathwise_connected TopSpace
for a1, b1, c1 being Point of T
for A1, A2 being Path of a1,b1
for B being Path of c1,b1 st A1,A2 are_homotopic holds
A1,(A2 + (- B)) + B are_homotopic

proof end;

theorem Th24: :: TOPALG_1:24

for X being non empty TopSpace
for a, b, c being Point of X st a,b are_connected & c,a are_connected holds
for A1, A2 being Path of a,b
for B being Path of c,a st A1,A2 are_homotopic holds
A1,((- B) + B) + A2 are_homotopic

proof end;

theorem :: TOPALG_1:25

for T being non empty pathwise_connected TopSpace
for a1, b1, c1 being Point of T
for A1, A2 being Path of a1,b1
for B being Path of c1,a1 st A1,A2 are_homotopic holds
A1,((- B) + B) + A2 are_homotopic

proof end;

theorem Th26: :: TOPALG_1:26

for X being non empty TopSpace
for a, b, c being Point of X st a,b are_connected & a,c are_connected holds
for A1, A2 being Path of a,b
for B being Path of a,c st A1,A2 are_homotopic holds
A1,(B + (- B)) + A2 are_homotopic

proof end;

theorem :: TOPALG_1:27

for T being non empty pathwise_connected TopSpace
for a1, b1, c1 being Point of T
for A1, A2 being Path of a1,b1
for B being Path of a1,c1 st A1,A2 are_homotopic holds
A1,(B + (- B)) + A2 are_homotopic

proof end;

theorem Th28: :: TOPALG_1:28

for X being non empty TopSpace
for a, b, c being Point of X st a,b are_connected & c,b are_connected holds
for A, B being Path of a,b
for C being Path of b,c st A + C,B + C are_homotopic holds
A,B are_homotopic

proof end;

theorem :: TOPALG_1:29

for T being non empty pathwise_connected TopSpace
for a1, b1, c1 being Point of T
for A, B being Path of a1,b1
for C being Path of b1,c1 st A + C,B + C are_homotopic holds
A,B are_homotopic

proof end;

theorem Th30: :: TOPALG_1:30

for X being non empty TopSpace
for a, b, c being Point of X st a,b are_connected & a,c are_connected holds
for A, B being Path of a,b
for C being Path of c,a st C + A,C + B are_homotopic holds
A,B are_homotopic

proof end;

theorem :: TOPALG_1:31

for T being non empty pathwise_connected TopSpace
for a1, b1, c1 being Point of T
for A, B being Path of a1,b1
for C being Path of c1,a1 st C + A,C + B are_homotopic holds
A,B are_homotopic

proof end;

theorem Th32: :: TOPALG_1:32

for X being non empty TopSpace
for a, b, c, d, e being Point of X st a,b are_connected & b,c are_connected & c,d are_connected & d,e are_connected holds
for A being Path of a,b
for B being Path of b,c
for C being Path of c,d
for D being Path of d,e holds ((A + B) + C) + D,(A + (B + C)) + D are_homotopic

proof end;

theorem :: TOPALG_1:33

for T being non empty pathwise_connected TopSpace
for a1, b1, c1, d1, e1 being Point of T
for A being Path of a1,b1
for B being Path of b1,c1
for C being Path of c1,d1
for D being Path of d1,e1 holds ((A + B) + C) + D,(A + (B + C)) + D are_homotopic

proof end;

theorem Th34: :: TOPALG_1:34

for X being non empty TopSpace
for a, b, c, d, e being Point of X st a,b are_connected & b,c are_connected & c,d are_connected & d,e are_connected holds
for A being Path of a,b
for B being Path of b,c
for C being Path of c,d
for D being Path of d,e holds ((A + B) + C) + D,A + ((B + C) + D) are_homotopic

proof end;

theorem :: TOPALG_1:35

for T being non empty pathwise_connected TopSpace
for a1, b1, c1, d1, e1 being Point of T
for A being Path of a1,b1
for B being Path of b1,c1
for C being Path of c1,d1
for D being Path of d1,e1 holds ((A + B) + C) + D,A + ((B + C) + D) are_homotopic

proof end;

theorem Th36: :: TOPALG_1:36

for X being non empty TopSpace
for a, b, c, d, e being Point of X st a,b are_connected & b,c are_connected & c,d are_connected & d,e are_connected holds
for A being Path of a,b
for B being Path of b,c
for C being Path of c,d
for D being Path of d,e holds (A + (B + C)) + D,(A + B) + (C + D) are_homotopic

proof end;

theorem :: TOPALG_1:37

for T being non empty pathwise_connected TopSpace
for a1, b1, c1, d1, e1 being Point of T
for A being Path of a1,b1
for B being Path of b1,c1
for C being Path of c1,d1
for D being Path of d1,e1 holds (A + (B + C)) + D,(A + B) + (C + D) are_homotopic

proof end;

theorem Th38: :: TOPALG_1:38

for X being non empty TopSpace
for a, b, c, d being Point of X st a,b are_connected & b,c are_connected & b,d are_connected holds
for A being Path of a,b
for B being Path of d,b
for C being Path of b,c holds ((A + (- B)) + B) + C,A + C are_homotopic

proof end;

theorem :: TOPALG_1:39

for T being non empty pathwise_connected TopSpace
for a1, b1, d1, c1 being Point of T
for A being Path of a1,b1
for B being Path of d1,b1
for C being Path of b1,c1 holds ((A + (- B)) + B) + C,A + C are_homotopic

proof end;

theorem Th40: :: TOPALG_1:40

for X being non empty TopSpace
for a, b, c, d being Point of X st a,b are_connected & a,c are_connected & c,d are_connected holds
for A being Path of a,b
for B being Path of c,d
for C being Path of a,c holds (((A + (- A)) + C) + B) + (- B),C are_homotopic

proof end;

theorem :: TOPALG_1:41

for T being non empty pathwise_connected TopSpace
for a1, b1, c1, d1 being Point of T
for A being Path of a1,b1
for B being Path of c1,d1
for C being Path of a1,c1 holds (((A + (- A)) + C) + B) + (- B),C are_homotopic

proof end;

theorem Th42: :: TOPALG_1:42

for X being non empty TopSpace
for a, b, c, d being Point of X st a,b are_connected & a,c are_connected & d,c are_connected holds
for A being Path of a,b
for B being Path of c,d
for C being Path of a,c holds (A + (((- A) + C) + B)) + (- B),C are_homotopic

proof end;

theorem :: TOPALG_1:43

for T being non empty pathwise_connected TopSpace
for a1, b1, c1, d1 being Point of T
for A being Path of a1,b1
for B being Path of c1,d1
for C being Path of a1,c1 holds (A + (((- A) + C) + B)) + (- B),C are_homotopic

proof end;

theorem Th44: :: TOPALG_1:44

for X being non empty TopSpace
for a, b, c, d, e, f being Point of X st a,b are_connected & b,c are_connected & c,d are_connected & d,e are_connected & a,f are_connected holds
for A being Path of a,b
for B being Path of b,c
for C being Path of c,d
for D being Path of d,e
for E being Path of f,c holds (A + (B + C)) + D,((A + B) + (- E)) + ((E + C) + D) are_homotopic

proof end;

theorem :: TOPALG_1:45

for T being non empty pathwise_connected TopSpace
for a1, b1, c1, d1, e1, f1 being Point of T
for A being Path of a1,b1
for B being Path of b1,c1
for C being Path of c1,d1
for D being Path of d1,e1
for E being Path of f1,c1 holds (A + (B + C)) + D,((A + B) + (- E)) + ((E + C) + D) are_homotopic

proof end;

begin

definition

let T be TopStruct ;
let t be Point of T;
mode Loop of t is Path of t,t;

end;

definition

let T be non empty TopStruct ;
let t1, t2 be Point of T;
defpred S₁[ set ] means $1 is Path of t1,t2;
func Paths (t1,t2) -> set means :Def1: :: TOPALG_1:def 1
for x being set holds
( x in it iff x is Path of t1,t2 );
existence
ex b₁ being set st
for x being set holds
( x in b₁ iff x is Path of t1,t2 )

proof end;

uniqueness
for b₁, b₂ being set st ( for x being set holds
( x in b₁ iff x is Path of t1,t2 ) ) & ( for x being set holds
( x in b₂ iff x is Path of t1,t2 ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines Paths TOPALG_1:def 1 :
for T being non empty TopStruct
for t1, t2 being Point of T
for b₄ being set holds
( b₄ = Paths (t1,t2) iff for x being set holds
( x in b₄ iff x is Path of t1,t2 ) );

registration

let T be non empty TopStruct ;
let t1, t2 be Point of T;
cluster Paths (t1,t2) -> non empty ;
coherence
not Paths (t1,t2) is empty

proof end;

end;

definition

let T be non empty TopStruct ;
let t be Point of T;
func Loops t -> set equals :: TOPALG_1:def 2
Paths (t,t);
coherence
Paths (t,t) is set ;

end;

:: deftheorem defines Loops TOPALG_1:def 2 :
for T being non empty TopStruct
for t being Point of T holds Loops t = Paths (t,t);

registration

let T be non empty TopStruct ;
let t be Point of T;
cluster Loops t -> non empty ;
coherence
not Loops t is empty ;

end;

Lm2: for X being non empty TopSpace
for a, b being Point of X st a,b are_connected holds
ex E being Equivalence_Relation of (Paths (a,b)) st
for x, y being set holds
( [x,y] in E iff ( x in Paths (a,b) & y in Paths (a,b) & ex P, Q being Path of a,b st
( P = x & Q = y & P,Q are_homotopic ) ) )

proof end;

definition

let X be non empty TopSpace;
let a, b be Point of X;
assume A1: a,b are_connected ;
func EqRel (X,a,b) -> Relation of (Paths (a,b)) means :Def3: :: TOPALG_1:def 3
for P, Q being Path of a,b holds
( [P,Q] in it iff P,Q are_homotopic );
existence
ex b₁ being Relation of (Paths (a,b)) st
for P, Q being Path of a,b holds
( [P,Q] in b₁ iff P,Q are_homotopic )

proof end;

uniqueness
for b₁, b₂ being Relation of (Paths (a,b)) st ( for P, Q being Path of a,b holds
( [P,Q] in b₁ iff P,Q are_homotopic ) ) & ( for P, Q being Path of a,b holds
( [P,Q] in b₂ iff P,Q are_homotopic ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines EqRel TOPALG_1:def 3 :
for X being non empty TopSpace
for a, b being Point of X st a,b are_connected holds
for b₄ being Relation of (Paths (a,b)) holds
( b₄ = EqRel (X,a,b) iff for P, Q being Path of a,b holds
( [P,Q] in b₄ iff P,Q are_homotopic ) );

Lm3: for X being non empty TopSpace
for a, b being Point of X st a,b are_connected holds
( not EqRel (X,a,b) is empty & EqRel (X,a,b) is total & EqRel (X,a,b) is symmetric & EqRel (X,a,b) is transitive )

proof end;

theorem Th46: :: TOPALG_1:46

for X being non empty TopSpace
for a, b being Point of X st a,b are_connected holds
for P, Q being Path of a,b holds
( Q in Class ((EqRel (X,a,b)),P) iff P,Q are_homotopic )

proof end;

theorem Th47: :: TOPALG_1:47

for X being non empty TopSpace
for a, b being Point of X st a,b are_connected holds
for P, Q being Path of a,b holds
( Class ((EqRel (X,a,b)),P) = Class ((EqRel (X,a,b)),Q) iff P,Q are_homotopic )

proof end;

definition

let X be non empty TopSpace;
let a be Point of X;
func EqRel (X,a) -> Relation of (Loops a) equals :: TOPALG_1:def 4
EqRel (X,a,a);
coherence
EqRel (X,a,a) is Relation of (Loops a) ;

end;

:: deftheorem defines EqRel TOPALG_1:def 4 :
for X being non empty TopSpace
for a being Point of X holds EqRel (X,a) = EqRel (X,a,a);

registration

let X be non empty TopSpace;
let a be Point of X;
cluster EqRel (X,a) -> non empty total symmetric transitive ;
coherence
( not EqRel (X,a) is empty & EqRel (X,a) is total & EqRel (X,a) is symmetric & EqRel (X,a) is transitive ) by Lm3;

end;

definition

let X be non empty TopSpace;
let a be Point of X;
set E = EqRel (X,a);
set A = Class (EqRel (X,a));
set W = Loops a;
func FundamentalGroup (X,a) -> strict multMagma means :Def5: :: TOPALG_1:def 5
( the carrier of it = Class (EqRel (X,a)) & ( for x, y being Element of it ex P, Q being Loop of a st
( x = Class ((EqRel (X,a)),P) & y = Class ((EqRel (X,a)),Q) & the multF of it . (x,y) = Class ((EqRel (X,a)),(P + Q)) ) ) );
existence
ex b₁ being strict multMagma st
( the carrier of b₁ = Class (EqRel (X,a)) & ( for x, y being Element of b₁ ex P, Q being Loop of a st
( x = Class ((EqRel (X,a)),P) & y = Class ((EqRel (X,a)),Q) & the multF of b₁ . (x,y) = Class ((EqRel (X,a)),(P + Q)) ) ) )

proof end;

uniqueness
for b₁, b₂ being strict multMagma st the carrier of b₁ = Class (EqRel (X,a)) & ( for x, y being Element of b₁ ex P, Q being Loop of a st
( x = Class ((EqRel (X,a)),P) & y = Class ((EqRel (X,a)),Q) & the multF of b₁ . (x,y) = Class ((EqRel (X,a)),(P + Q)) ) ) & the carrier of b₂ = Class (EqRel (X,a)) & ( for x, y being Element of b₂ ex P, Q being Loop of a st
( x = Class ((EqRel (X,a)),P) & y = Class ((EqRel (X,a)),Q) & the multF of b₂ . (x,y) = Class ((EqRel (X,a)),(P + Q)) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def5 defines FundamentalGroup TOPALG_1:def 5 :
for X being non empty TopSpace
for a being Point of X
for b₃ being strict multMagma holds
( b₃ = FundamentalGroup (X,a) iff ( the carrier of b₃ = Class (EqRel (X,a)) & ( for x, y being Element of b₃ ex P, Q being Loop of a st
( x = Class ((EqRel (X,a)),P) & y = Class ((EqRel (X,a)),Q) & the multF of b₃ . (x,y) = Class ((EqRel (X,a)),(P + Q)) ) ) ) );

notation

let X be non empty TopSpace;
let a be Point of X;
synonym pi_1 (X,a) for FundamentalGroup (X,a);

end;

registration

let X be non empty TopSpace;
let a be Point of X;
cluster FundamentalGroup (X,a) -> non empty strict ;
coherence
not pi_1 (X,a) is empty

proof end;

end;

theorem Th48: :: TOPALG_1:48

for X being non empty TopSpace
for a being Point of X
for x being set holds
( x in the carrier of (pi_1 (X,a)) iff ex P being Loop of a st x = Class ((EqRel (X,a)),P) )

proof end;

Lm4: for S being non empty TopSpace
for s being Point of S
for x, y being Element of (pi_1 (S,s))
for P, Q being Loop of s st x = Class ((EqRel (S,s)),P) & y = Class ((EqRel (S,s)),Q) holds
x * y = Class ((EqRel (S,s)),(P + Q))

proof end;

registration

let X be non empty TopSpace;
let a be Point of X;
cluster FundamentalGroup (X,a) -> strict Group-like associative ;
coherence
( pi_1 (X,a) is associative & pi_1 (X,a) is Group-like )

proof end;

end;

definition

let T be non empty TopSpace;
let x0, x1 be Point of T;
let P be Path of x0,x1;
assume A1: x0,x1 are_connected ;
func pi_1-iso P -> Function of (pi_1 (T,x1)),(pi_1 (T,x0)) means :Def6: :: TOPALG_1:def 6
for Q being Loop of x1 holds it . (Class ((EqRel (T,x1)),Q)) = Class ((EqRel (T,x0)),((P + Q) + (- P)));
existence
ex b₁ being Function of (pi_1 (T,x1)),(pi_1 (T,x0)) st
for Q being Loop of x1 holds b₁ . (Class ((EqRel (T,x1)),Q)) = Class ((EqRel (T,x0)),((P + Q) + (- P)))

proof end;

uniqueness
for b₁, b₂ being Function of (pi_1 (T,x1)),(pi_1 (T,x0)) st ( for Q being Loop of x1 holds b₁ . (Class ((EqRel (T,x1)),Q)) = Class ((EqRel (T,x0)),((P + Q) + (- P))) ) & ( for Q being Loop of x1 holds b₂ . (Class ((EqRel (T,x1)),Q)) = Class ((EqRel (T,x0)),((P + Q) + (- P))) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def6 defines pi_1-iso TOPALG_1:def 6 :
for T being non empty TopSpace
for x0, x1 being Point of T
for P being Path of x0,x1 st x0,x1 are_connected holds
for b₅ being Function of (pi_1 (T,x1)),(pi_1 (T,x0)) holds
( b₅ = pi_1-iso P iff for Q being Loop of x1 holds b₅ . (Class ((EqRel (T,x1)),Q)) = Class ((EqRel (T,x0)),((P + Q) + (- P))) );

theorem Th49: :: TOPALG_1:49

for X being non empty TopSpace
for x0, x1 being Point of X
for P, Q being Path of x0,x1 st x0,x1 are_connected & P,Q are_homotopic holds
pi_1-iso P = pi_1-iso Q

proof end;

theorem :: TOPALG_1:50

for T being non empty pathwise_connected TopSpace
for y0, y1 being Point of T
for R, V being Path of y0,y1 st R,V are_homotopic holds
pi_1-iso R = pi_1-iso V

proof end;

theorem Th51: :: TOPALG_1:51

for X being non empty TopSpace
for x0, x1 being Point of X
for P being Path of x0,x1 st x0,x1 are_connected holds
pi_1-iso P is Homomorphism of (pi_1 (X,x1)),(pi_1 (X,x0))

proof end;

registration

let T be non empty pathwise_connected TopSpace;
let x0, x1 be Point of T;
let P be Path of x0,x1;
cluster pi_1-iso P -> multiplicative ;
coherence
pi_1-iso P is multiplicative

proof end;

end;

theorem Th52: :: TOPALG_1:52

for X being non empty TopSpace
for x0, x1 being Point of X
for P being Path of x0,x1 st x0,x1 are_connected holds
pi_1-iso P is one-to-one

proof end;

theorem Th53: :: TOPALG_1:53

for X being non empty TopSpace
for x0, x1 being Point of X
for P being Path of x0,x1 st x0,x1 are_connected holds
pi_1-iso P is onto

proof end;

registration

let T be non empty pathwise_connected TopSpace;
let x0, x1 be Point of T;
let P be Path of x0,x1;
cluster pi_1-iso P -> one-to-one onto ;
coherence
( pi_1-iso P is one-to-one & pi_1-iso P is onto )

proof end;

end;

theorem Th54: :: TOPALG_1:54

for X being non empty TopSpace
for x0, x1 being Point of X
for P being Path of x0,x1 st x0,x1 are_connected holds
(pi_1-iso P) " = pi_1-iso (- P)

proof end;

theorem :: TOPALG_1:55

for T being non empty pathwise_connected TopSpace
for y0, y1 being Point of T
for R being Path of y0,y1 holds (pi_1-iso R) " = pi_1-iso (- R)

proof end;

theorem Th56: :: TOPALG_1:56

for X being non empty TopSpace
for x0, x1 being Point of X
for P being Path of x0,x1 st x0,x1 are_connected holds
for h being Homomorphism of (pi_1 (X,x1)),(pi_1 (X,x0)) st h = pi_1-iso P holds
h is bijective

proof end;

theorem :: TOPALG_1:57

for T being non empty pathwise_connected TopSpace
for y0, y1 being Point of T
for R being Path of y0,y1 holds pi_1-iso R is bijective ;

theorem :: TOPALG_1:58

for X being non empty TopSpace
for x0, x1 being Point of X st x0,x1 are_connected holds
pi_1 (X,x0), pi_1 (X,x1) are_isomorphic

proof end;

theorem :: TOPALG_1:59

for T being non empty pathwise_connected TopSpace
for y0, y1 being Point of T holds pi_1 (T,y0), pi_1 (T,y1) are_isomorphic

proof end;

begin

definition

let n be Nat;
let P, Q be Function of I[01],(TOP-REAL n);
func RealHomotopy (P,Q) -> Function of [:I[01],I[01]:],(TOP-REAL n) means :Def7: :: TOPALG_1:def 7
for s, t being Element of I[01] holds it . (s,t) = ((1 - t) * (P . s)) + (t * (Q . s));
existence
ex b₁ being Function of [:I[01],I[01]:],(TOP-REAL n) st
for s, t being Element of I[01] holds b₁ . (s,t) = ((1 - t) * (P . s)) + (t * (Q . s))

proof end;

uniqueness
for b₁, b₂ being Function of [:I[01],I[01]:],(TOP-REAL n) st ( for s, t being Element of I[01] holds b₁ . (s,t) = ((1 - t) * (P . s)) + (t * (Q . s)) ) & ( for s, t being Element of I[01] holds b₂ . (s,t) = ((1 - t) * (P . s)) + (t * (Q . s)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def7 defines RealHomotopy TOPALG_1:def 7 :
for n being Nat
for P, Q being Function of I[01],(TOP-REAL n)
for b₄ being Function of [:I[01],I[01]:],(TOP-REAL n) holds
( b₄ = RealHomotopy (P,Q) iff for s, t being Element of I[01] holds b₄ . (s,t) = ((1 - t) * (P . s)) + (t * (Q . s)) );

Lm5: for n being Nat
for P, Q being continuous Function of I[01],(TOP-REAL n) holds RealHomotopy (P,Q) is continuous

proof end;

Lm6: for n being Nat
for a, b being Point of (TOP-REAL n)
for P, Q being Path of a,b
for s being Point of I[01] holds
( (RealHomotopy (P,Q)) . (s,0) = P . s & (RealHomotopy (P,Q)) . (s,1) = Q . s & ( for t being Point of I[01] holds
( (RealHomotopy (P,Q)) . (0,t) = a & (RealHomotopy (P,Q)) . (1,t) = b ) ) )

proof end;

theorem Th60: :: TOPALG_1:60

for n being Nat
for a, b being Point of (TOP-REAL n)
for P, Q being Path of a,b holds P,Q are_homotopic

proof end;

registration

let n be Nat;
let a, b be Point of (TOP-REAL n);
let P, Q be Path of a,b;
cluster -> continuous Homotopy of P,Q;
coherence
for b₁ being Homotopy of P,Q holds b₁ is continuous

proof end;

end;

theorem Th61: :: TOPALG_1:61

for n being Nat
for a being Point of (TOP-REAL n)
for C being Loop of a holds the carrier of (pi_1 ((TOP-REAL n),a)) = {(Class ((EqRel ((TOP-REAL n),a)),C))}

proof end;

registration

let n be Nat;
let a be Point of (TOP-REAL n);
cluster FundamentalGroup ((TOP-REAL n),a) -> trivial strict ;
coherence
pi_1 ((TOP-REAL n),a) is trivial

proof end;

end;

theorem :: TOPALG_1:62

for S being non empty TopSpace
for s being Point of S
for x, y being Element of (pi_1 (S,s))
for P, Q being Loop of s st x = Class ((EqRel (S,s)),P) & y = Class ((EqRel (S,s)),Q) holds
x * y = Class ((EqRel (S,s)),(P + Q)) by Lm4;

theorem Th63: :: TOPALG_1:63

for X being non empty TopSpace
for a being Point of X
for C being constant Loop of a holds 1_ (pi_1 (X,a)) = Class ((EqRel (X,a)),C)

proof end;

theorem :: TOPALG_1:64

for X being non empty TopSpace
for a being Point of X
for x, y being Element of (pi_1 (X,a))
for P being Loop of a st x = Class ((EqRel (X,a)),P) & y = Class ((EqRel (X,a)),(- P)) holds
x " = y

proof end;

registration

let n be Nat;
let P, Q be continuous Function of I[01],(TOP-REAL n);
cluster RealHomotopy (P,Q) -> continuous ;
coherence
RealHomotopy (P,Q) is continuous by Lm5;

end;

theorem :: TOPALG_1:65

for n being Nat
for a, b being Point of (TOP-REAL n)
for P, Q being Path of a,b holds RealHomotopy (P,Q) is Homotopy of P,Q

proof end;

theorem :: TOPALG_1:66

for X being non empty TopSpace
for a, b being Point of X st a,b are_connected holds
( not EqRel (X,a,b) is empty & EqRel (X,a,b) is total & EqRel (X,a,b) is symmetric & EqRel (X,a,b) is transitive ) by Lm3;