:: On the Isomorphism of Fundamental Groups
:: by Artur Korni{\l}owicz
::
:: Received July 30, 2004
:: Copyright (c) 2004-2012 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_2;

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

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

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

theorem Th3: :: TOPALG_3:3
for X, a, b being set
for f being Function of X,{a,b} holds X = (f " {a}) \/ (f " {b})
proofend;

theorem :: TOPALG_3:4
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:7;

:: Topological preliminaries
theorem :: TOPALG_3:5
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
proofend;

theorem Th6: :: TOPALG_3:6
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 )
proofend;

theorem Th7: :: TOPALG_3:7
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 ) )
proofend;

registration
cluster empty  ->  connected for TopStruct ;
coherence
 for b1 being TopStruct st b1 is empty holds
b1 is connected
proofend;
end;

theorem :: TOPALG_3:8
for T being TopSpace st TopStruct(# the carrier of T, the topology of T #) is connected holds
T is connected
proofend;

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
proofend;
end;

theorem :: TOPALG_3:9
for S, T being non empty TopSpace st S,T are_homeomorphic & S is pathwise_connected holds
T is pathwise_connected
proofend;

registration
cluster non empty trivial TopSpace-like  ->  non empty pathwise_connected for TopStruct ;
coherence
 for b1 being non empty TopSpace st b1 is trivial holds
b1 is pathwise_connected
proofend;
end;

theorem :: TOPALG_3:10
for T being SubSpace of TOP-REAL 2 st the carrier of T is Simple_closed_curve holds
T is pathwise_connected
proofend;

theorem :: TOPALG_3:11
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 )
proofend;

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

theorem :: TOPALG_3:12
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
proofend;

begin

theorem Th13: :: TOPALG_3:13
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 #):]
proofend;

theorem Th14: :: TOPALG_3:14
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):]
proofend;

theorem Th15: :: TOPALG_3:15
for S, T being TopSpace
for A being closed Subset of S
for B being closed Subset of T holds [:A,B:] is closed
proofend;

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

theorem :: TOPALG_3:16
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
proofend;

theorem :: TOPALG_3:17
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
proofend;

theorem :: TOPALG_3:18
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
proofend;

theorem :: TOPALG_3:19
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 )
proofend;

theorem :: TOPALG_3:20
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 )
proofend;

begin

registration
let T be non empty TopSpace;
let t be Point of T;
cluster  ->  continuous for Path of t,t;
coherence
 for b1 being Loop of t holds b1 is continuous
proofend;
end;

theorem :: TOPALG_3:21
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
proofend;

theorem Th22: :: TOPALG_3:22
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 )
proofend;

theorem Th23: :: TOPALG_3:23
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
proofend;

theorem :: 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
for P being Path of a,b st a,b are_connected holds
f * P is Path of f . a,f . b
proofend;

theorem Th25: :: TOPALG_3:25
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
proofend;

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 funcf * P ->  Path of f . a,f . b;
coherence
 P * f is Path of f . a,f . b by Th25;
end;

theorem Th26: :: TOPALG_3:26
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
proofend;

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 funcf * P ->  Loop of f . a;
coherence
 P * f is Loop of f . a 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, 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
proofend;

theorem :: 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
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
proofend;

theorem Th29: :: TOPALG_3:29
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)
proofend;

definition
let S, T be non empty TopSpace;
let s be Point of S;
let f be Function of S,T;
assume B1: 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 b1 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) & b1 . x = Class ((EqRel (T,(f . s))),(f * ls)) )
proofend;
uniqueness
 for b1, b2 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) & b1 . 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) & b2 . x = Class ((EqRel (T,(f . s))),(f * ls)) ) ) holds
b1 = b2
proofend;
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 b5 being Function of (pi_1 (S,s)),(pi_1 (T,(f . s))) holds
( b5 = 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) & b5 . x = Class ((EqRel (T,(f . s))),(f * ls)) ) );

theorem :: TOPALG_3:30
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))
proofend;

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
proofend;
end;

theorem Th31: :: TOPALG_3:31
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
proofend;

theorem :: TOPALG_3:32
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
proofend;

theorem :: TOPALG_3:33
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
proofend;