:: On the Isomorphism of Fundamental Groups
:: by Artur Korni{\l}owicz
::
:: Received July 30, 2004
:: Copyright (c) 2004-2011 Association of Mizar Users

begin

set I = the carrier of I[01];

Lm1: 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 I[01] by BORSUK_1:def 17, BORSUK_1:def 18;

theorem :: TOPALG_3:1

for A, B, a, b being set
for f being Function of A,B st a in A & b in B holds
f +* (a .--> b) is Function of A,B

proof end;

theorem :: TOPALG_3:2

for f being Function
for X, x being set st f | X is one-to-one & x in rng (f | X) holds
(f * ((f | X) ")) . x = x

proof end;

theorem :: TOPALG_3:3

canceled;

theorem Th4: :: TOPALG_3:4

for X, a, b being set
for f being Function of X,{a,b} holds X = (f " {a}) \/ (f " {b})

proof end;

theorem :: TOPALG_3:5

for S, T being non empty 1-sorted
for s being Point of S
for t being Point of T holds (S --> t) . s = t by FUNCOP_1:13;

theorem :: TOPALG_3:6

for T being non empty TopStruct
for t being Point of T
for A being Subset of T st A = {t} holds
Sspace t = T | A

proof end;

theorem Th7: :: TOPALG_3:7

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

proof end;

theorem Th8: :: TOPALG_3:8

for T being non empty TopSpace holds
( T is connected iff for f being Function of T,(1TopSp {0,1}) holds
( not f is continuous or not f is onto ) )

proof end;

registration

cluster empty -> connected TopStruct ;
coherence
for b₁ being TopStruct st b₁ is empty holds
b₁ is connected

proof end;

end;

theorem :: TOPALG_3:9

for T being TopSpace st TopStruct(# the carrier of T, the topology of T #) is connected holds
T is connected

proof end;

registration

let T be connected TopSpace;
cluster TopStruct(# the carrier of T, the topology of T #) -> connected ;
coherence
TopStruct(# the carrier of T, the topology of T #) is connected

proof end;

end;

theorem :: TOPALG_3:10

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

proof end;

registration

cluster non empty trivial TopSpace-like -> non empty pathwise_connected TopStruct ;
coherence
for b₁ being non empty TopSpace st b₁ is trivial holds
b₁ is pathwise_connected

proof end;

end;

theorem :: TOPALG_3:11

for T being SubSpace of TOP-REAL 2 st the carrier of T is Simple_closed_curve holds
T is pathwise_connected

proof end;

theorem :: TOPALG_3:12

for T being TopSpace ex F being Subset-Family of T st
( F = { the carrier of T} & F is Cover of T & F is open )

proof end;

registration

let T be TopSpace;
cluster non empty open closed mutually-disjoint Element of bool (bool the carrier of T);
existence
ex b₁ being Subset-Family of T st
( not b₁ is empty & b₁ is mutually-disjoint & b₁ is open & b₁ is closed )

proof end;

end;

theorem :: TOPALG_3:13

for T being TopSpace
for D being open mutually-disjoint Subset-Family of T
for A being Subset of T
for X being set st A is connected & X in D & X meets A & D is Cover of A holds
A c= X

proof end;

begin

theorem Th14: :: TOPALG_3:14

for S, T being TopSpace holds TopStruct(# the carrier of [:S,T:], the topology of [:S,T:] #) = [:TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #):]

proof end;

theorem Th15: :: TOPALG_3:15

for S, T being TopSpace
for A being Subset of S
for B being Subset of T holds Cl [:A,B:] = [:(Cl A),(Cl B):]

proof end;

theorem Th16: :: TOPALG_3:16

for S, T being TopSpace
for A being closed Subset of S
for B being closed Subset of T holds [:A,B:] is closed

proof end;

registration

let A, B be connected TopSpace;
cluster [:A,B:] -> connected ;
coherence
[:A,B:] is connected

proof end;

end;

theorem :: TOPALG_3:17

for S, T being TopSpace
for A being Subset of S
for B being Subset of T st A is connected & B is connected holds
[:A,B:] is connected

proof end;

theorem :: TOPALG_3:18

for S, T being TopSpace
for Y being non empty TopSpace
for A being Subset of S
for f being Function of [:S,T:],Y
for g being Function of [:(S | A),T:],Y st g = f | [:A, the carrier of T:] & f is continuous holds
g is continuous

proof end;

theorem :: TOPALG_3:19

for S, T being TopSpace
for Y being non empty TopSpace
for A being Subset of T
for f being Function of [:S,T:],Y
for g being Function of [:S,(T | A):],Y st g = f | [: the carrier of S,A:] & f is continuous holds
g is continuous

proof end;

theorem :: TOPALG_3:20

for S, T, T1, T2, Y being non empty TopSpace
for f being Function of [:Y,T1:],S
for g being Function of [:Y,T2:],S
for F1, F2 being closed Subset of T st T1 is SubSpace of T & T2 is SubSpace of T & F1 = [#] T1 & F2 = [#] T2 & ([#] T1) \/ ([#] T2) = [#] T & f is continuous & g is continuous & ( for p being set st p in ([#] [:Y,T1:]) /\ ([#] [:Y,T2:]) holds
f . p = g . p ) holds
ex h being Function of [:Y,T:],S st
( h = f +* g & h is continuous )

proof end;

theorem :: TOPALG_3:21

for S, T, T1, T2, Y being non empty TopSpace
for f being Function of [:T1,Y:],S
for g being Function of [:T2,Y:],S
for F1, F2 being closed Subset of T st T1 is SubSpace of T & T2 is SubSpace of T & F1 = [#] T1 & F2 = [#] T2 & ([#] T1) \/ ([#] T2) = [#] T & f is continuous & g is continuous & ( for p being set st p in ([#] [:T1,Y:]) /\ ([#] [:T2,Y:]) holds
f . p = g . p ) holds
ex h being Function of [:T,Y:],S st
( h = f +* g & h is continuous )

proof end;

begin

registration

let T be non empty TopSpace;
let t be Point of T;
cluster -> continuous Path of t,t;
coherence
for b₁ being Loop of t holds b₁ is continuous

proof end;

end;

theorem :: TOPALG_3:22

for T being non empty TopSpace
for t being Point of T
for x being Point of I[01]
for P being constant Loop of t holds P . x = t

proof end;

theorem Th23: :: TOPALG_3:23

for T being non empty TopSpace
for t being Point of T
for P being Loop of t holds
( P . 0 = t & P . 1 = t )

proof end;

theorem Th24: :: TOPALG_3:24

for S, T being non empty TopSpace
for f being continuous Function of S,T
for a, b being Point of S st a,b are_connected holds
f . a,f . b are_connected

proof end;

theorem :: TOPALG_3:25

for S, T being non empty TopSpace
for f being continuous Function of S,T
for a, b being Point of S
for P being Path of a,b st a,b are_connected holds
f * P is Path of f . a,f . b

proof end;

theorem Th26: :: TOPALG_3:26

for S being non empty pathwise_connected TopSpace
for T being non empty TopSpace
for f being continuous Function of S,T
for a, b being Point of S
for P being Path of a,b holds f * P is Path of f . a,f . b

proof end;

definition

let S be non empty pathwise_connected TopSpace;
let T be non empty TopSpace;
let a, b be Point of S;
let P be Path of a,b;
let f be continuous Function of S,T;
:: original: *
redefine func f * P -> Path of f . a,f . b;
coherence
P * f is Path of f . a,f . b by Th26;

end;

theorem Th27: :: TOPALG_3:27

for S, T being non empty TopSpace
for f being continuous Function of S,T
for a being Point of S
for P being Loop of a holds f * P is Loop of f . a

proof end;

definition

let S, T be non empty TopSpace;
let a be Point of S;
let P be Loop of a;
let f be continuous Function of S,T;
:: original: *
redefine func f * P -> Loop of f . a;
coherence
P * f is Loop of f . a by Th27;

end;

theorem Th28: :: TOPALG_3:28

for S, T being non empty TopSpace
for f being continuous Function of S,T
for a, b being Point of S
for P, Q being Path of a,b
for P1, Q1 being Path of f . a,f . b st P,Q are_homotopic & P1 = f * P & Q1 = f * Q holds
P1,Q1 are_homotopic

proof end;

theorem :: TOPALG_3:29

for S, T being non empty TopSpace
for f being continuous Function of S,T
for a, b being Point of S
for P, Q being Path of a,b
for P1, Q1 being Path of f . a,f . b
for F being Homotopy of P,Q st P,Q are_homotopic & P1 = f * P & Q1 = f * Q holds
f * F is Homotopy of P1,Q1

proof end;

theorem Th30: :: TOPALG_3:30

for S, T being non empty TopSpace
for f being continuous Function of S,T
for a, b, c being Point of S
for P being Path of a,b
for Q being Path of b,c
for P1 being Path of f . a,f . b
for Q1 being Path of f . b,f . c st a,b are_connected & b,c are_connected & P1 = f * P & Q1 = f * Q holds
P1 + Q1 = f * (P + Q)

proof end;

definition

let S, T be non empty TopSpace;
let s be Point of S;
let f be Function of S,T;
assume A1: f is continuous ;
set pT = pi_1 (T,(f . s));
set pS = pi_1 (S,s);
func FundGrIso (f,s) -> Function of (pi_1 (S,s)),(pi_1 (T,(f . s))) means :Def1: :: TOPALG_3:def 1
for x being Element of (pi_1 (S,s)) ex ls being Loop of s st
( x = Class ((EqRel (S,s)),ls) & it . x = Class ((EqRel (T,(f . s))),(f * ls)) );
existence
ex b₁ being Function of (pi_1 (S,s)),(pi_1 (T,(f . s))) st
for x being Element of (pi_1 (S,s)) ex ls being Loop of s st
( x = Class ((EqRel (S,s)),ls) & b₁ . x = Class ((EqRel (T,(f . s))),(f * ls)) )

proof end;

uniqueness
for b₁, b₂ being Function of (pi_1 (S,s)),(pi_1 (T,(f . s))) st ( for x being Element of (pi_1 (S,s)) ex ls being Loop of s st
( x = Class ((EqRel (S,s)),ls) & b₁ . x = Class ((EqRel (T,(f . s))),(f * ls)) ) ) & ( for x being Element of (pi_1 (S,s)) ex ls being Loop of s st
( x = Class ((EqRel (S,s)),ls) & b₂ . x = Class ((EqRel (T,(f . s))),(f * ls)) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines FundGrIso TOPALG_3:def 1 :
for S, T being non empty TopSpace
for s being Point of S
for f being Function of S,T st f is continuous holds
for b₅ being Function of (pi_1 (S,s)),(pi_1 (T,(f . s))) holds
( b₅ = FundGrIso (f,s) iff for x being Element of (pi_1 (S,s)) ex ls being Loop of s st
( x = Class ((EqRel (S,s)),ls) & b₅ . x = Class ((EqRel (T,(f . s))),(f * ls)) ) );

theorem :: TOPALG_3:31

canceled;

theorem :: TOPALG_3:32

for S, T being non empty TopSpace
for s being Point of S
for f being continuous Function of S,T
for ls being Loop of s holds (FundGrIso (f,s)) . (Class ((EqRel (S,s)),ls)) = Class ((EqRel (T,(f . s))),(f * ls))

proof end;

registration

let S, T be non empty TopSpace;
let s be Point of S;
let f be continuous Function of S,T;
cluster FundGrIso (f,s) -> multiplicative ;
coherence
FundGrIso (f,s) is multiplicative

proof end;

end;

theorem Th33: :: TOPALG_3:33

for S, T being non empty TopSpace
for s being Point of S
for f being continuous Function of S,T st f is being_homeomorphism holds
FundGrIso (f,s) is bijective

proof end;

theorem :: TOPALG_3:34

for S, T being non empty TopSpace
for s being Point of S
for t being Point of T
for f being continuous Function of S,T
for P being Path of t,f . s
for h being Homomorphism of (pi_1 (S,s)),(pi_1 (T,t)) st f is being_homeomorphism & f . s,t are_connected & h = (pi_1-iso P) * (FundGrIso (f,s)) holds
h is bijective

proof end;

theorem :: TOPALG_3:35

for S being non empty TopSpace
for T being non empty pathwise_connected TopSpace
for s being Point of S
for t being Point of T st S,T are_homeomorphic holds
pi_1 (S,s), pi_1 (T,t) are_isomorphic

proof end;