let S, T be non empty TopSpace; :: thesis: 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
let s be Point of S; :: thesis: for f being continuous Function of S,T st f is being_homeomorphism holds
FundGrIso f,s is bijective
let f be continuous Function of S,T; :: thesis: ( f is being_homeomorphism implies FundGrIso f,s is bijective )
assume A1:
f is being_homeomorphism
; :: thesis: FundGrIso f,s is bijective
set pS = pi_1 S,s;
set pT = pi_1 T,(f . s);
A2:
f " is continuous
by A1, TOPS_2:def 5;
set h = FundGrIso f,s;
A3:
dom (FundGrIso f,s) = the carrier of (pi_1 S,s)
by FUNCT_2:def 1;
A4:
dom f = [#] S
by A1, TOPS_2:def 5;
A5:
rng f = [#] T
by A1, TOPS_2:def 5;
A6:
f is one-to-one
by A1, TOPS_2:def 5;
then A7:
(f " ) . (f . s) = s
by FUNCT_2:32;
A8:
f " = f "
by A5, A6, TOPS_2:def 4;
A9:
rng (FundGrIso f,s) = the carrier of (pi_1 T,(f . s))
proof
thus
rng (FundGrIso f,s) c= the
carrier of
(pi_1 T,(f . s))
;
:: according to XBOOLE_0:def 10 :: thesis: the carrier of (pi_1 T,(f . s)) c= rng (FundGrIso f,s)
let y be
set ;
:: according to TARSKI:def 3 :: thesis: ( not y in the carrier of (pi_1 T,(f . s)) or y in rng (FundGrIso f,s) )
assume
y in the
carrier of
(pi_1 T,(f . s))
;
:: thesis: y in rng (FundGrIso f,s)
then consider lt being
Loop of
f . s such that A10:
y = Class (EqRel T,(f . s)),
lt
by TOPALG_1:48;
reconsider ls =
(f " ) * lt as
Loop of
s by A2, A7, A8, Th27;
set x =
Class (EqRel S,s),
ls;
A11:
Class (EqRel S,s),
ls in the
carrier of
(pi_1 S,s)
by TOPALG_1:48;
then consider ls1 being
Loop of
s such that A12:
Class (EqRel S,s),
ls = Class (EqRel S,s),
ls1
and A13:
(FundGrIso f,s) . (Class (EqRel S,s),ls) = Class (EqRel T,(f . s)),
(f * ls1)
by Def1;
A14:
f * ls =
(f * (f " )) * lt
by RELAT_1:55
.=
(id (rng f)) * lt
by A5, A6, TOPS_2:65
.=
lt
by A5, FUNCT_2:23
;
ls,
ls1 are_homotopic
by A12, TOPALG_1:47;
then
lt,
f * ls1 are_homotopic
by A14, Th28;
then
(FundGrIso f,s) . (Class (EqRel S,s),ls) = y
by A10, A13, TOPALG_1:47;
hence
y in rng (FundGrIso f,s)
by A3, A11, FUNCT_1:def 5;
:: thesis: verum
end;
FundGrIso f,s is one-to-one
proof
let x1,
x2 be
set ;
:: according to FUNCT_1:def 8 :: thesis: ( not x1 in dom (FundGrIso f,s) or not x2 in dom (FundGrIso f,s) or not (FundGrIso f,s) . x1 = (FundGrIso f,s) . x2 or x1 = x2 )
assume
x1 in dom (FundGrIso f,s)
;
:: thesis: ( not x2 in dom (FundGrIso f,s) or not (FundGrIso f,s) . x1 = (FundGrIso f,s) . x2 or x1 = x2 )
then consider ls1 being
Loop of
s such that A15:
x1 = Class (EqRel S,s),
ls1
and A16:
(FundGrIso f,s) . x1 = Class (EqRel T,(f . s)),
(f * ls1)
by Def1;
assume
x2 in dom (FundGrIso f,s)
;
:: thesis: ( not (FundGrIso f,s) . x1 = (FundGrIso f,s) . x2 or x1 = x2 )
then consider ls2 being
Loop of
s such that A17:
x2 = Class (EqRel S,s),
ls2
and A18:
(FundGrIso f,s) . x2 = Class (EqRel T,(f . s)),
(f * ls2)
by Def1;
reconsider a1 =
(f " ) * (f * ls1),
a2 =
(f " ) * (f * ls2) as
Loop of
s by A2, A7, A8, Th27;
A19:
(f " ) * f = id (dom f)
by A5, A6, TOPS_2:65;
A20:
(f " ) * (f * ls1) =
((f " ) * f) * ls1
by RELAT_1:55
.=
ls1
by A4, A19, FUNCT_2:23
;
A21:
(f " ) * (f * ls2) =
((f " ) * f) * ls2
by RELAT_1:55
.=
ls2
by A4, A19, FUNCT_2:23
;
assume
(FundGrIso f,s) . x1 = (FundGrIso f,s) . x2
;
:: thesis: x1 = x2
then
f * ls1,
f * ls2 are_homotopic
by A16, A18, TOPALG_1:47;
then
a1,
a2 are_homotopic
by A2, A7, A8, Th28;
hence
x1 = x2
by A15, A17, A20, A21, TOPALG_1:47;
:: thesis: verum
end;
hence
FundGrIso f,s is bijective
by A9, GROUP_6:70; :: thesis: verum