:: TOPALG_1 semantic presentation

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_isomorphism

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 Th6: :: TOPALG_1:6

for x being real number
for n being Nat
for f being Element of n -tuples_on REAL holds x * (- f) = - (x * f)

proof end;

theorem Th7: :: TOPALG_1:7

for x being real number
for n being Nat
for f, g being Element of n -tuples_on REAL holds x * (f - g) = (x * f) - (x * g)

proof end;

theorem Th8: :: TOPALG_1:8

for x, y being real number
for n being Nat
for f being Element of n -tuples_on REAL holds (x - y) * f = (x * f) - (y * f)

proof end;

theorem Th9: :: TOPALG_1:9

for n being Nat
for f, g, h, k being Element of n -tuples_on REAL 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;

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 A being Path of a,b
for B being Path of b,c holds A,(A + 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 A being Path of a1,b1
for B being Path of b1,c1 holds A,(A + 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 A being Path of a,b
for B being Path of c,b holds A,(A + (- 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 A being Path of a1,b1
for B being Path of c1,b1 holds A,(A + (- 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 A being Path of a,b
for B being Path of c,a holds A,((- B) + B) + A 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 A being Path of a1,b1
for B being Path of c1,a1 holds A,((- B) + B) + A 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 A being Path of a,b
for B being Path of a,c holds A,(B + (- B)) + A 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 A being Path of a1,b1
for B being Path of a1,c1 holds A,(B + (- B)) + A 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

proof end;

theorem :: TOPALG_1:35

proof end;

theorem Th36: :: TOPALG_1:36

proof end;

theorem :: TOPALG_1:37

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;

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 t be Point of T;
func Loops t -> set means :Def1: :: TOPALG_1:def 1
for x being set holds
( x in it iff x is Loop of t );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines Loops TOPALG_1:def 1 :

registration

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

proof end;

end;

Lm2: for X being non empty TopSpace
for a being Point of X ex E being Equivalence_Relation of Loops a st
for x, y being set holds
( [x,y] in E iff ( x in Loops a & y in Loops a & ex P, Q being Loop of a st
( P = x & Q = y & 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 means :Def2: :: TOPALG_1:def 2
for P, Q being Loop of a holds
( [P,Q] in it iff P,Q are_homotopic );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines EqRel TOPALG_1:def 2 :

registration

let X be non empty TopSpace;
let a be Point of X;
cluster EqRel X,a -> non empty symmetric transitive total ;
coherence

proof end;

end;

theorem Th46: :: TOPALG_1:46

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

proof end;

theorem Th47: :: TOPALG_1:47

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

proof end;

definition

let X be non empty TopSpace;
let a be Point of X;
func FundamentalGroup X,a -> strict HGrStr means :Def3: :: TOPALG_1:def 3
( 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 mult of it . x,y = Class (EqRel X,a),(P + Q) ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines FundamentalGroup TOPALG_1:def 3 :

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

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;

registration

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

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 :Def4: :: TOPALG_1:def 4
for Q being Loop of x1 holds it . (Class (EqRel T,x1),Q) = Class (EqRel T,x0),((P + Q) + (- P));
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines pi_1-iso TOPALG_1:def 4 :

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

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

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_isomorphism

proof end;

theorem Th57: :: 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_isomorphism

proof end;

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;

definition

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines RealHomotopy TOPALG_1:def 5 :

Lm3: 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 continuous

proof end;

Lm4: 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;

definition

let n be Nat;
let a, b be Point of (TOP-REAL n);
let P, Q be Path of a,b;
:: original: RealHomotopy
redefine func RealHomotopy P,Q -> Homotopy of P,Q;
coherence

proof end;

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

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 -> non empty strict Group-like associative trivial ;
coherence

proof end;

end;