:: The Fundamental Group
:: by Artur Korni{\l}owicz , Yasunari Shidama and Adam Grabowski
::
:: Received March 18, 2004
:: Copyright (c) 2004 Association of Mizar Users
theorem :: TOPALG_1:1
theorem Th2: :: TOPALG_1:2
theorem Th3: :: TOPALG_1:3
theorem Th4: :: TOPALG_1:4
theorem Th5: :: TOPALG_1:5
theorem :: TOPALG_1:6
theorem Th7: :: TOPALG_1:7
theorem Th8: :: TOPALG_1:8
theorem Th9: :: TOPALG_1:9
theorem Th10: :: TOPALG_1:10
theorem :: TOPALG_1:11
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
theorem Th13: :: TOPALG_1:13
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)
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
theorem :: TOPALG_1:15
canceled;
theorem Th16: :: TOPALG_1:16
theorem :: TOPALG_1:17
theorem Th18: :: TOPALG_1:18
theorem Th19: :: TOPALG_1:19
theorem Th20: :: TOPALG_1:20
theorem :: TOPALG_1:21
theorem Th22: :: TOPALG_1:22
theorem :: TOPALG_1:23
theorem Th24: :: TOPALG_1:24
theorem :: TOPALG_1:25
theorem Th26: :: TOPALG_1:26
theorem :: TOPALG_1:27
theorem Th28: :: TOPALG_1:28
theorem :: TOPALG_1:29
theorem Th30: :: TOPALG_1:30
theorem :: TOPALG_1:31
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
theorem :: TOPALG_1:33
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
theorem :: TOPALG_1:35
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
theorem :: TOPALG_1:37
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
theorem :: TOPALG_1:39
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
theorem :: TOPALG_1:41
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
theorem :: TOPALG_1:43
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
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
:: deftheorem Def1 defines Paths TOPALG_1:def 1 :
:: deftheorem defines Loops TOPALG_1:def 2 :
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 ) ) )
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 b1 being Relation of (Paths a,b) st
for P, Q being Path of a,b holds
( [P,Q] in b1 iff P,Q are_homotopic )
uniqueness
for b1, b2 being Relation of (Paths a,b) st ( for P, Q being Path of a,b holds
( [P,Q] in b1 iff P,Q are_homotopic ) ) & ( for P, Q being Path of a,b holds
( [P,Q] in b2 iff P,Q are_homotopic ) ) holds
b1 = b2
end;
:: deftheorem Def3 defines EqRel TOPALG_1:def 3 :
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 )
theorem Th46: :: TOPALG_1:46
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 )
:: deftheorem defines EqRel TOPALG_1:def 4 :
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 b1 being strict multMagma st
( the carrier of b1 = Class (EqRel X,a) & ( for x, y being Element of b1 ex P, Q being Loop of a st
( x = Class (EqRel X,a),P & y = Class (EqRel X,a),Q & the multF of b1 . x,y = Class (EqRel X,a),(P + Q) ) ) )
uniqueness
for b1, b2 being strict multMagma st the carrier of b1 = Class (EqRel X,a) & ( for x, y being Element of b1 ex P, Q being Loop of a st
( x = Class (EqRel X,a),P & y = Class (EqRel X,a),Q & the multF of b1 . x,y = Class (EqRel X,a),(P + Q) ) ) & the carrier of b2 = Class (EqRel X,a) & ( for x, y being Element of b2 ex P, Q being Loop of a st
( x = Class (EqRel X,a),P & y = Class (EqRel X,a),Q & the multF of b2 . x,y = Class (EqRel X,a),(P + Q) ) ) holds
b1 = b2
end;
:: deftheorem Def5 defines FundamentalGroup TOPALG_1:def 5 :
for
X being non
empty TopSpace for
a being
Point of
X for
b3 being
strict multMagma holds
(
b3 = FundamentalGroup X,
a iff ( the
carrier of
b3 = Class (EqRel X,a) & ( for
x,
y being
Element of
b3 ex
P,
Q being
Loop of
a st
(
x = Class (EqRel X,a),
P &
y = Class (EqRel X,a),
Q & the
multF of
b3 . x,
y = Class (EqRel X,a),
(P + Q) ) ) ) );
theorem Th48: :: TOPALG_1:48
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)
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 b1 being Function of (pi_1 T,x1),(pi_1 T,x0) st
for Q being Loop of x1 holds b1 . (Class (EqRel T,x1),Q) = Class (EqRel T,x0),((P + Q) + (- P))
uniqueness
for b1, b2 being Function of (pi_1 T,x1),(pi_1 T,x0) st ( for Q being Loop of x1 holds b1 . (Class (EqRel T,x1),Q) = Class (EqRel T,x0),((P + Q) + (- P)) ) & ( for Q being Loop of x1 holds b2 . (Class (EqRel T,x1),Q) = Class (EqRel T,x0),((P + Q) + (- P)) ) holds
b1 = b2
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
b5 being
Function of
(pi_1 T,x1),
(pi_1 T,x0) holds
(
b5 = pi_1-iso P iff for
Q being
Loop of
x1 holds
b5 . (Class (EqRel T,x1),Q) = Class (EqRel T,x0),
((P + Q) + (- P)) );
theorem Th49: :: TOPALG_1:49
theorem :: TOPALG_1:50
theorem Th51: :: TOPALG_1:51
theorem Th52: :: TOPALG_1:52
theorem Th53: :: TOPALG_1:53
theorem Th54: :: TOPALG_1:54
theorem :: TOPALG_1:55
theorem Th56: :: TOPALG_1:56
theorem :: TOPALG_1:57
theorem :: TOPALG_1:58
theorem :: TOPALG_1:59
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 b1 being Function of [:I[01] ,I[01] :],(TOP-REAL n) st
for s, t being Element of I[01] holds b1 . s,t = ((1 - t) * (P . s)) + (t * (Q . s))
uniqueness
for b1, b2 being Function of [:I[01] ,I[01] :],(TOP-REAL n) st ( for s, t being Element of I[01] holds b1 . s,t = ((1 - t) * (P . s)) + (t * (Q . s)) ) & ( for s, t being Element of I[01] holds b2 . s,t = ((1 - t) * (P . s)) + (t * (Q . s)) ) holds
b1 = b2
end;
:: deftheorem Def7 defines RealHomotopy TOPALG_1:def 7 :
Lm5:
for n being Nat
for P, Q being continuous Function of I[01] ,(TOP-REAL n) holds RealHomotopy P,Q is continuous
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 ) ) )
theorem Th60: :: TOPALG_1:60
theorem Th61: :: TOPALG_1:61
theorem :: TOPALG_1:62
theorem Th63: :: TOPALG_1:63
theorem :: TOPALG_1:64
theorem :: TOPALG_1:65
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;