:: The Fundamental Group of the Circle
:: by Artur Korni{\l}owicz
::
:: Received February 22, 2005
:: Copyright (c) 2005 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:86;

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

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

reconsider j0 = 0 , j1 = 1 as Point of by BORSUK_1:def 17, BORSUK_1:def 18;

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 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).[ )

proof end;

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 holds
( f . y = { (Ball y,(1 / n)) where n is Element of NAT : n <> 0 } & B = Union f ) & ( for X being Subset of st X in B holds
X is connected ) )

proof end;

theorem Th3: :: TOPALG_5:3

for T being TopStruct
for A being Subset of
for t being Point of st t in A holds
Component_of t,A c= A

proof end;

registration

let T be TopSpace;
let A be open Subset of ;
cluster T | A -> open ;
coherence
T | A is open

proof end;

end;

theorem Th4: :: TOPALG_5:4

for T being TopSpace
for S being SubSpace of T
for A being Subset of
for B being Subset of st A = B holds
T | A = S | B

proof end;

theorem Th5: :: TOPALG_5:5

for S, T being TopSpace
for A, B being Subset of
for C, D being Subset of st TopStruct(# the carrier of S,the topology of S #) = TopStruct(# the carrier of T,the topology of T #) & A = C & B = D & A,B are_separated holds
C,D are_separated

proof end;

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 #) & S is connected holds
T is connected

proof end;

theorem Th7: :: TOPALG_5:7

for S, T being TopSpace
for A being Subset of
for B being Subset of st TopStruct(# the carrier of S,the topology of S #) = TopStruct(# the carrier of T,the topology of T #) & A = B & A is connected holds
B is connected

proof end;

theorem Th8: :: TOPALG_5:8

for S, T being non empty TopSpace
for s being Point of
for t being Point of
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 #) & s = t holds
A is a_neighborhood of t

proof end;

theorem :: TOPALG_5:9

for S, T being non empty TopSpace
for A being Subset of
for B being Subset of
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 #) & A = B holds
N is a_neighborhood of B

proof end;

theorem Th10: :: TOPALG_5:10

for S, T being non empty TopSpace
for A, B being Subset of
for f being Function of S,T st f is being_homeomorphism & A is_a_component_of B holds
f " A is_a_component_of f " B

proof end;

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
for B being non empty Subset of st A = B & A is locally_connected holds
B is locally_connected

proof end;

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 #) & S is locally_connected holds
T is locally_connected

proof end;

theorem Th13: :: TOPALG_5:13

for T being non empty TopSpace holds
( T is locally_connected iff [#] T is locally_connected )

proof end;

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

proof end;

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

proof end;

theorem :: TOPALG_5:15

for S, T being non empty TopSpace st S,T are_homeomorphic & S is locally_connected holds
T is locally_connected

proof end;

theorem Th16: :: TOPALG_5:16

for T being non empty TopSpace st ex B being Basis of T st
for X being Subset of st X in B holds
X is connected holds
T is locally_connected

proof end;

theorem Th17: :: TOPALG_5:17

for r, s being real number st r <= s holds
Closed-Interval-TSpace r,s is locally_connected

proof end;

registration

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

end;

registration

let A be non empty open Subset of ;
cluster I[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 holds it . x = r * x;
existence
ex b₁ being Function of I[01] ,R^1 st
for x being Point of holds b₁ . x = r * x

proof end;

uniqueness
for b₁, b₂ being Function of I[01] ,R^1 st ( for x being Point of holds b₁ . x = r * x ) & ( for x being Point of holds b₂ . x = r * x ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines ExtendInt TOPALG_5:def 1 :

for r being real number
for b₂ being Function of I[01] ,R^1 holds
( b₂ = ExtendInt r iff for x being Point of holds b₂ . x = r * x );

registration

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

proof end;

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

proof end;

end;

definition

let S, T, Y be non empty TopSpace;
let H be Function of [:S,T:],Y;
let t be Point of ;
func Prj1 t,H -> Function of S,Y means :Def2: :: TOPALG_5:def 2
for s being Point of holds it . s = H . s,t;
existence
ex b₁ being Function of S,Y st
for s being Point of holds b₁ . s = H . s,t

proof end;

uniqueness
for b₁, b₂ being Function of S,Y st ( for s being Point of holds b₁ . s = H . s,t ) & ( for s being Point of holds b₂ . s = H . s,t ) holds
b₁ = b₂

proof end;

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
for b₆ being Function of S,Y holds
( b₆ = Prj1 t,H iff for s being Point of holds b₆ . 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 ;
func Prj2 s,H -> Function of T,Y means :Def3: :: TOPALG_5:def 3
for t being Point of holds it . t = H . s,t;
existence
ex b₁ being Function of T,Y st
for t being Point of holds b₁ . t = H . s,t

proof end;

uniqueness
for b₁, b₂ being Function of T,Y st ( for t being Point of holds b₁ . t = H . s,t ) & ( for t being Point of holds b₂ . t = H . s,t ) holds
b₁ = b₂

proof end;

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
for b₆ being Function of T,Y holds
( b₆ = Prj2 s,H iff for t being Point of holds b₆ . 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 ;
cluster Prj1 t,H -> continuous ;
coherence
Prj1 t,H is continuous

proof end;

end;

registration

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

proof end;

end;

theorem :: TOPALG_5:18

for T being non empty TopSpace
for a, b being Point of
for P, Q being Path of a,b
for H being Homotopy of P,Q
for t being Point of 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
for P, Q being Path of a,b
for H being Homotopy of P,Q
for s being Point of 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

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:58, TOPREALB:9; :: thesis: verum

end;

Lm12: dom CircleMap = REAL
by FUNCT_2:def 1, TOPMETR:24;

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 holds it . x = |[(cos (((2 * PI ) * r) * x)),(sin (((2 * PI ) * r) * x))]|;
existence
ex b₁ being Function of I[01] ,(Tunit_circle 2) st
for x being Point of holds b₁ . x = |[(cos (((2 * PI ) * r) * x)),(sin (((2 * PI ) * r) * x))]|

proof end;

uniqueness
for b₁, b₂ being Function of I[01] ,(Tunit_circle 2) st ( for x being Point of holds b₁ . x = |[(cos (((2 * PI ) * r) * x)),(sin (((2 * PI ) * r) * x))]| ) & ( for x being Point of holds b₂ . x = |[(cos (((2 * PI ) * r) * x)),(sin (((2 * PI ) * r) * x))]| ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines cLoop TOPALG_5:def 4 :

for r being real number
for b₂ being Function of I[01] ,(Tunit_circle 2) holds
( b₂ = cLoop r iff for x being Point of holds b₂ . 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)

proof end;

definition

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

proof end;

end;

begin

Lm13: ex F being Subset-Family of st
( F is Cover of & F is open & ( for U being Subset of st U in F holds
ex D being mutually-disjoint open Subset-Family of st
( union D = CircleMap " U & ( for d being Subset of 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 ) ) ) )

proof end;

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

Lm15: for r, s being real number
for F being Subset-Family of
for C being IntervalCover of F
for G being IntervalCoverPts of C st F is Cover of & F is open & F is connected & r <= s holds
not G is empty

proof end;

theorem Th21: :: TOPALG_5:21

for UL being Subset-Family of st UL is Cover of & 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 ex T being non empty FinSequence of REAL st
( T . 1 = 0 & T . (len T) = 1 & T is increasing & ex N being open Subset of st
( y in N & ( for i being natural number st i in dom T & i + 1 in dom T holds
ex Ui being non empty Subset of st
( Ui in UL & F .: [:N,[.(T . i),(T . (i + 1)).]:] c= Ui ) ) ) )

proof end;

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 & Ft is continuous & F | [:the carrier of Y,{0 }:] = CircleMap * Ft holds
ex G being Function of [:Y,I[01] :],R^1 st
( G is continuous & F = CircleMap * G & G | [:the carrier of Y,{0 }:] = Ft & ( for H being Function of [:Y,I[01] :],R^1 st H is continuous & F = CircleMap * H & H | [:the carrier of Y,{0 }:] = Ft holds
G = H ) )

proof end;

theorem Th23: :: TOPALG_5:23

for x0, y0 being Point of
for xt being Point of
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 & f = CircleMap * ft & ft is continuous & ( for f1 being Function of I[01] ,R^1 st f1 is continuous & f = CircleMap * f1 & f1 . 0 = xt holds
ft = f1 ) )

proof end;

theorem Th24: :: TOPALG_5:24

for x0, y0 being Point of
for P, Q being Path of x0,y0
for F being Homotopy of P,Q
for xt being Point of st P,Q are_homotopic & xt in CircleMap " {x0} holds
ex yt being Point of ex Pt, Qt being Path of xt,yt ex Ft being Homotopy of Pt,Qt st
( Pt,Qt are_homotopic & F = CircleMap * Ft & yt in CircleMap " {y0} & ( for F1 being Homotopy of Pt,Qt st F = CircleMap * F1 holds
Ft = F1 ) )

proof end;

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 b₁ being Function of INT.Group ,(pi_1 (Tunit_circle 2),c[10] ) st
for n being Integer holds b₁ . n = Class (EqRel (Tunit_circle 2),c[10] ),(cLoop n)

proof end;

uniqueness
for b₁, b₂ being Function of INT.Group ,(pi_1 (Tunit_circle 2),c[10] ) st ( for n being Integer holds b₁ . n = Class (EqRel (Tunit_circle 2),c[10] ),(cLoop n) ) & ( for n being Integer holds b₂ . n = Class (EqRel (Tunit_circle 2),c[10] ),(cLoop n) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def5 defines Ciso TOPALG_5:def 5 :

for b₁ being Function of INT.Group ,(pi_1 (Tunit_circle 2),c[10] ) holds
( b₁ = Ciso iff for n being Integer holds b₁ . 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)

proof end;

definition

:: original: Ciso
redefine func Ciso -> Homomorphism of INT.Group , pi_1 (Tunit_circle 2),c[10] ;
coherence
Ciso is Homomorphism of INT.Group , pi_1 (Tunit_circle 2),c[10]

proof end;

end;

registration

cluster Ciso -> one-to-one onto ;
coherence
( Ciso is one-to-one & Ciso is onto )

proof end;

end;

theorem :: TOPALG_5:26

Ciso is bijective ;

Lm16: for r being positive real number
for o being Point of
for x being Point of holds INT.Group , pi_1 (Tcircle o,r),x are_isomorphic

proof end;

theorem Th27: :: TOPALG_5:27

for S being being_simple_closed_curve SubSpace of TOP-REAL 2
for x being Point of holds INT.Group , pi_1 S,x are_isomorphic

proof end;

registration

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

proof end;

end;