begin
theorem
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 Th14:
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
begin
theorem Th31:
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 Th33:
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 Th35:
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 Th37:
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 Th39:
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 Th41:
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 Th43:
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
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
begin
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 B1:
a,
b are_connected
;
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;
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:
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 )
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:
( 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)) ) ) ) );
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
;
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))) );
begin
definition
let n be
Nat;
let P,
Q be
Function of
I[01],
(TOP-REAL n);
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;
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
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;