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