:: 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 Group
for h being Homomorphism of G,H st h * (h " ) = id H & (h " ) * h = id G 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 arcwise_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 arcwise_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 arcwise_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 arcwise_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 arcwise_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 arcwise_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 arcwise_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 arcwise_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 arcwise_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 arcwise_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 arcwise_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 arcwise_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 arcwise_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 arcwise_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;

definition

let T be non empty arcwise_connected TopSpace;
let x0, x1 be Point of T;
let P be Path of x0,x1;
:: original: pi_1-iso
redefine func pi_1-iso P -> Homomorphism of (pi_1 T,x1),(pi_1 T,x0);
coherence
pi_1-iso P is Homomorphism of (pi_1 T,x1),(pi_1 T,x0)

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 arcwise_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 arcwise_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 arcwise_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 arcwise_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;