:: The Fundamental Group of the Circle
:: by Artur Korni{\l}owicz
::
:: Received February 22, 2005
:: Copyright (c) 2005-2012 Association of Mizar Users


begin

set o = |[0,0]|;

set I = the carrier of I[01];

set R = the carrier of R^1;

Lm1:  0 in INT
by INT_1:def_1;

Lm2:  0 in the carrier of I[01]
by BORSUK_1:43;

then Lm3:  {0} c= the carrier of I[01]
by ZFMISC_1:31;

Lm4:  0 in {0}
by TARSKI:def_1;

Lm5:  the carrier of [:I[01],I[01]:] = [: the carrier of I[01], the carrier of I[01]:]
by BORSUK_1:def_2;

reconsider j0 = 0 , j1 = 1 as Point of I[01] by BORSUK_1:def_14, BORSUK_1:def_15;

Lm6:  [#] I[01] = the carrier of I[01]
;

Lm7:  I[01] | ([#] I[01]) = I[01]
by TSEP_1:3;

Lm8:  1 - 0 <= 1
;

Lm9:  (3 / 2) - (1 / 2) <= 1
;

registration
cluster INT.Group  ->  infinite ;
coherence
 not INT.Group is finite ;
end;

theorem Th1: :: TOPALG_5:1
for r, s, a being real number st r <= s holds
for p being Point of (Closed-Interval-MSpace (r,s)) holds
( Ball (p,a) = [.r,s.] or Ball (p,a) = [.r,(p + a).[ or Ball (p,a) = ].(p - a),s.] or Ball (p,a) = ].(p - a),(p + a).[ )
proofend;

theorem Th2: :: TOPALG_5:2
for r, s being real number st r <= s holds
ex B being Basis of (Closed-Interval-TSpace (r,s)) st
( ex f being ManySortedSet of (Closed-Interval-TSpace (r,s)) st
for y being Point of (Closed-Interval-MSpace (r,s)) holds
( f . y =  {  (Ball (y,(1 / n))) where n is Element of NAT : n <> 0  }  &amp; B = Union f ) &amp; ( for X being Subset of (Closed-Interval-TSpace (r,s)) st X in B holds
X is connected ) )
proofend;

theorem Th3: :: TOPALG_5:3
for T being TopStruct
for A being Subset of T
for t being Point of T st t in A holds
Component_of (t,A) c= A
proofend;

registration
let T be TopSpace;
let A be open Subset of T;
clusterT | A ->  open ;
coherence
 T | A is open
proofend;
end;

theorem Th4: :: TOPALG_5:4
for T being TopSpace
for S being SubSpace of T
for A being Subset of T
for B being Subset of S st A = B holds
T | A = S | B
proofend;

theorem Th5: :: TOPALG_5:5
for S, T being TopSpace
for A, B being Subset of T
for C, D being Subset of S st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) &amp; A = C &amp; B = D &amp; A,B are_separated holds
C,D are_separated
proofend;

theorem :: TOPALG_5:6
for S, T being TopSpace st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) &amp; S is connected holds
T is connected
proofend;

theorem Th7: :: TOPALG_5:7
for S, T being TopSpace
for A being Subset of S
for B being Subset of T st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) &amp; A = B &amp; A is connected holds
B is connected
proofend;

theorem Th8: :: TOPALG_5:8
for S, T being non empty TopSpace
for s being Point of S
for t being Point of T
for A being a_neighborhood of s st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) &amp; s = t holds
A is a_neighborhood of t
proofend;

theorem :: TOPALG_5:9
for S, T being non empty TopSpace
for A being Subset of S
for B being Subset of T
for N being a_neighborhood of A st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) &amp; A = B holds
N is a_neighborhood of B
proofend;

theorem Th10: :: TOPALG_5:10
for S, T being non empty TopSpace
for A, B being Subset of T
for f being Function of S,T st f is being_homeomorphism &amp; A is_a_component_of B holds
f " A is_a_component_of f " B
proofend;

begin

theorem Th11: :: TOPALG_5:11
for T being non empty TopSpace
for S being non empty SubSpace of T
for A being non empty Subset of T
for B being non empty Subset of S st A = B &amp; A is locally_connected holds
B is locally_connected
proofend;

theorem Th12: :: TOPALG_5:12
for S, T being non empty TopSpace st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) &amp; S is locally_connected holds
T is locally_connected
proofend;

theorem Th13: :: TOPALG_5:13
for T being non empty TopSpace holds
( T is locally_connected iff [#] T is locally_connected )
proofend;

Lm10:  for T being non empty TopSpace
for S being non empty open SubSpace of T st T is locally_connected holds
TopStruct(# the carrier of S, the topology of S #) is locally_connected
proofend;

theorem Th14: :: TOPALG_5:14
for T being non empty TopSpace
for S being non empty open SubSpace of T st T is locally_connected holds
S is locally_connected
proofend;

theorem :: TOPALG_5:15
for S, T being non empty TopSpace st S,T are_homeomorphic &amp; S is locally_connected holds
T is locally_connected
proofend;

theorem Th16: :: TOPALG_5:16
for T being non empty TopSpace st ex B being Basis of T st
for X being Subset of T st X in B holds
X is connected holds
T is locally_connected
proofend;

theorem Th17: :: TOPALG_5:17
for r, s being real number st r <= s holds
Closed-Interval-TSpace (r,s) is locally_connected
proofend;

registration
cluster I[01]  ->  locally_connected ;
coherence
 I[01] is locally_connected by Th17, TOPMETR:20;
end;

registration
let A be non empty open Subset of I[01];
clusterI[01] | A ->  locally_connected ;
coherence
 I[01] | A is locally_connected by Th14;
end;

begin

definition
let r be real number ;
func ExtendInt r ->  Function of I[01],R^1 means :Def1: :: TOPALG_5:def 1
 for x being Point of I[01] holds it . x = r * x;
existence
 ex b1 being Function of I[01],R^1 st
for x being Point of I[01] holds b1 . x = r * x
proofend;
uniqueness
 for b1, b2 being Function of I[01],R^1 st ( for x being Point of I[01] holds b1 . x = r * x ) &amp; ( for x being Point of I[01] holds b2 . x = r * x ) holds
b1 = b2
proofend;
end;

:: deftheorem Def1 defines ExtendInt TOPALG_5:def_1_:_
 for r being real number
for b2 being Function of I[01],R^1 holds
( b2 = ExtendInt r iff for x being Point of I[01] holds b2 . x = r * x );

registration
let r be real number ;
cluster ExtendInt r ->  continuous ;
coherence
 ExtendInt r is continuous
proofend;
end;

definition
let r be real number ;
:: original:ExtendInt
redefine func ExtendInt r ->  Path of R^1 0, R^1 r;
coherence
 ExtendInt r is Path of R^1 0, R^1 r
proofend;
end;

definition
let S, T, Y be non empty TopSpace;
let H be Function of [:S,T:],Y;
let t be Point of T;
func Prj1 (t,H) ->  Function of S,Y means :Def2: :: TOPALG_5:def 2
 for s being Point of S holds it . s = H . (s,t);
existence
 ex b1 being Function of S,Y st
for s being Point of S holds b1 . s = H . (s,t)
proofend;
uniqueness
 for b1, b2 being Function of S,Y st ( for s being Point of S holds b1 . s = H . (s,t) ) &amp; ( for s being Point of S holds b2 . s = H . (s,t) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def2 defines Prj1 TOPALG_5:def_2_:_
 for S, T, Y being non empty TopSpace
for H being Function of [:S,T:],Y
for t being Point of T
for b6 being Function of S,Y holds
( b6 = Prj1 (t,H) iff for s being Point of S holds b6 . s = H . (s,t) );

definition
let S, T, Y be non empty TopSpace;
let H be Function of [:S,T:],Y;
let s be Point of S;
func Prj2 (s,H) ->  Function of T,Y means :Def3: :: TOPALG_5:def 3
 for t being Point of T holds it . t = H . (s,t);
existence
 ex b1 being Function of T,Y st
for t being Point of T holds b1 . t = H . (s,t)
proofend;
uniqueness
 for b1, b2 being Function of T,Y st ( for t being Point of T holds b1 . t = H . (s,t) ) &amp; ( for t being Point of T holds b2 . t = H . (s,t) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def3 defines Prj2 TOPALG_5:def_3_:_
 for S, T, Y being non empty TopSpace
for H being Function of [:S,T:],Y
for s being Point of S
for b6 being Function of T,Y holds
( b6 = Prj2 (s,H) iff for t being Point of T holds b6 . t = H . (s,t) );

registration
let S, T, Y be non empty TopSpace;
let H be continuous Function of [:S,T:],Y;
let t be Point of T;
cluster Prj1 (t,H) ->  continuous ;
coherence
 Prj1 (t,H) is continuous
proofend;
end;

registration
let S, T, Y be non empty TopSpace;
let H be continuous Function of [:S,T:],Y;
let s be Point of S;
cluster Prj2 (s,H) ->  continuous ;
coherence
 Prj2 (s,H) is continuous
proofend;
end;

theorem :: TOPALG_5:18
for T being non empty TopSpace
for a, b being Point of T
for P, Q being Path of a,b
for H being Homotopy of P,Q
for t being Point of I[01] st H is continuous holds
Prj1 (t,H) is continuous ;

theorem :: TOPALG_5:19
for T being non empty TopSpace
for a, b being Point of T
for P, Q being Path of a,b
for H being Homotopy of P,Q
for s being Point of I[01] st H is continuous holds
Prj2 (s,H) is continuous ;

set TUC = Tunit_circle 2;

set cS1 = the carrier of (Tunit_circle 2);

Lm11: now__::_thesis:_the_carrier_of_(Tunit_circle_2)_=_Sphere_(|[0,0]|,1)
 Tunit_circle 2 = Tcircle ((0. (TOP-REAL 2)),1) by TOPREALB:def_7;
hence  the carrier of (Tunit_circle 2) = Sphere (|[0,0]|,1) by EUCLID:54, TOPREALB:9; ::_thesis: verum
end;

Lm12:  dom CircleMap = REAL
by FUNCT_2:def_1, TOPMETR:17;

definition
let r be real number ;
func cLoop r ->  Function of I[01],(Tunit_circle 2) means :Def4: :: TOPALG_5:def 4
 for x being Point of I[01] holds it . x = |[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x))]|;
existence
 ex b1 being Function of I[01],(Tunit_circle 2) st
for x being Point of I[01] holds b1 . x = |[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x))]|
proofend;
uniqueness
 for b1, b2 being Function of I[01],(Tunit_circle 2) st ( for x being Point of I[01] holds b1 . x = |[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x))]| ) &amp; ( for x being Point of I[01] holds b2 . x = |[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x))]| ) holds
b1 = b2
proofend;
end;

:: deftheorem Def4 defines cLoop TOPALG_5:def_4_:_
 for r being real number
for b2 being Function of I[01],(Tunit_circle 2) holds
( b2 = cLoop r iff for x being Point of I[01] holds b2 . x = |[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x))]| );

theorem Th20: :: TOPALG_5:20
for r being real number holds cLoop r = CircleMap * (ExtendInt r)
proofend;

definition
let n be Integer;
:: original:cLoop
redefine func cLoop n ->  Loop of c[10] ;
coherence
 cLoop n is Loop of c[10]
proofend;
end;

begin

Lm13:  ex F being Subset-Family of (Tunit_circle 2) st
( F is Cover of (Tunit_circle 2) &amp; F is open &amp; ( for U being Subset of (Tunit_circle 2) st U in F holds
ex D being mutually-disjoint open Subset-Family of R^1 st
( union D = CircleMap " U &amp; ( for d being Subset of R^1 st d in D holds
for f being Function of (R^1 | d),((Tunit_circle 2) | U) st f = CircleMap | d holds
f is being_homeomorphism ) ) ) )
proofend;

Lm14:  [#] (Sspace 0[01]) = {0}
by TEX_2:def_2;

Lm15:  for r, s being real number
for F being Subset-Family of (Closed-Interval-TSpace (r,s))
for C being IntervalCover of F
for G being IntervalCoverPts of C st F is Cover of (Closed-Interval-TSpace (r,s)) &amp; F is open &amp; F is connected &amp; r <= s holds
not G is empty
proofend;

theorem Th21: :: TOPALG_5:21
for UL being Subset-Family of (Tunit_circle 2) st UL is Cover of (Tunit_circle 2) &amp; UL is open holds
for Y being non empty TopSpace
for F being continuous Function of [:Y,I[01]:],(Tunit_circle 2)
for y being Point of Y ex T being non empty FinSequence of REAL st
( T . 1 = 0 &amp; T . (len T) = 1 &amp; T is increasing &amp; ex N being open Subset of Y st
( y in N &amp; ( for i being Nat st i in dom T &amp; i + 1 in dom T holds
ex Ui being non empty Subset of (Tunit_circle 2) st
( Ui in UL &amp; F .: [:N,[.(T . i),(T . (i + 1)).]:] c= Ui ) ) ) )
proofend;

theorem Th22: :: TOPALG_5:22
for Y being non empty TopSpace
for F being Function of [:Y,I[01]:],(Tunit_circle 2)
for Ft being Function of [:Y,(Sspace 0[01]):],R^1 st F is continuous &amp; Ft is continuous &amp; F | [: the carrier of Y,{0}:] = CircleMap * Ft holds
ex G being Function of [:Y,I[01]:],R^1 st
( G is continuous &amp; F = CircleMap * G &amp; G | [: the carrier of Y,{0}:] = Ft &amp; ( for H being Function of [:Y,I[01]:],R^1 st H is continuous &amp; F = CircleMap * H &amp; H | [: the carrier of Y,{0}:] = Ft holds
G = H ) )
proofend;

theorem Th23: :: TOPALG_5:23
for x0, y0 being Point of (Tunit_circle 2)
for xt being Point of R^1
for f being Path of x0,y0 st xt in CircleMap " {x0} holds
ex ft being Function of I[01],R^1 st
( ft . 0 = xt &amp; f = CircleMap * ft &amp; ft is continuous &amp; ( for f1 being Function of I[01],R^1 st f1 is continuous &amp; f = CircleMap * f1 &amp; f1 . 0 = xt holds
ft = f1 ) )
proofend;

theorem Th24: :: TOPALG_5:24
for x0, y0 being Point of (Tunit_circle 2)
for P, Q being Path of x0,y0
for F being Homotopy of P,Q
for xt being Point of R^1 st P,Q are_homotopic &amp; xt in CircleMap " {x0} holds
ex yt being Point of R^1 ex Pt, Qt being Path of xt,yt ex Ft being Homotopy of Pt,Qt st
( Pt,Qt are_homotopic &amp; F = CircleMap * Ft &amp; yt in CircleMap " {y0} &amp; ( for F1 being Homotopy of Pt,Qt st F = CircleMap * F1 holds
Ft = F1 ) )
proofend;

definition
func Ciso  ->  Function of INT.Group,(pi_1 ((Tunit_circle 2),c[10])) means :Def5: :: TOPALG_5:def 5
 for n being Integer holds it . n = Class ((EqRel ((Tunit_circle 2),c[10])),(cLoop n));
existence
 ex b1 being Function of INT.Group,(pi_1 ((Tunit_circle 2),c[10])) st
for n being Integer holds b1 . n = Class ((EqRel ((Tunit_circle 2),c[10])),(cLoop n))
proofend;
uniqueness
 for b1, b2 being Function of INT.Group,(pi_1 ((Tunit_circle 2),c[10])) st ( for n being Integer holds b1 . n = Class ((EqRel ((Tunit_circle 2),c[10])),(cLoop n)) ) &amp; ( for n being Integer holds b2 . n = Class ((EqRel ((Tunit_circle 2),c[10])),(cLoop n)) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def5 defines Ciso TOPALG_5:def_5_:_
 for b1 being Function of INT.Group,(pi_1 ((Tunit_circle 2),c[10])) holds
( b1 = Ciso iff for n being Integer holds b1 . n = Class ((EqRel ((Tunit_circle 2),c[10])),(cLoop n)) );

theorem Th25: :: TOPALG_5:25
for i being Integer
for f being Path of R^1 0, R^1 i holds Ciso . i = Class ((EqRel ((Tunit_circle 2),c[10])),(CircleMap * f))
proofend;

registration
cluster Ciso  ->  multiplicative ;
coherence
 Ciso is multiplicative
proofend;
end;

registration
cluster Ciso  ->  one-to-one onto ;
coherence
 ( Ciso is one-to-one &amp; Ciso is onto )
proofend;
end;

theorem :: TOPALG_5:26
Ciso is bijective ;

Lm16:  for r being positive real number
for o being Point of (TOP-REAL 2)
for x being Point of (Tcircle (o,r)) holds INT.Group , pi_1 ((Tcircle (o,r)),x) are_isomorphic
proofend;

theorem Th27: :: TOPALG_5:27
for S being being_simple_closed_curve SubSpace of TOP-REAL 2
for x being Point of S holds INT.Group , pi_1 (S,x) are_isomorphic
proofend;

registration
let S be being_simple_closed_curve SubSpace of TOP-REAL 2;
let x be Point of S;
cluster FundamentalGroup (S,x) ->  infinite ;
coherence
 not pi_1 (S,x) is finite
proofend;
end;