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;
then A3:
(f ") . (f . s) = s
by FUNCT_2:26;
set h = FundGrIso (f,s);
set pT = pi_1 (T,(f . s));
A4:
f " is continuous
by A1;
A5:
rng f = [#] T
by A1;
then
f is onto
;
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
object ;
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:47;
reconsider ls =
(f ") * lt as
Loop of
s by A4, A3, A6, Th26;
set x =
Class (
(EqRel (S,s)),
ls);
A10:
Class (
(EqRel (S,s)),
ls)
in the
carrier of
(pi_1 (S,s))
by TOPALG_1:47;
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:36
.=
(id (rng f)) * lt
by A5, A2, TOPS_2:52
.=
lt
by A5, FUNCT_2:17
;
ls,
ls1 are_homotopic
by A11, TOPALG_1:46;
then
lt,
f * ls1 are_homotopic
by A13, Th27;
then
(FundGrIso (f,s)) . (Class ((EqRel (S,s)),ls)) = y
by A9, A12, TOPALG_1:46;
hence
y in rng (FundGrIso (f,s))
by A7, A10, FUNCT_1:def 3;
verum
end;
FundGrIso (f,s) is one-to-one
proof
let x1,
x2 be
object ;
FUNCT_1:def 4 ( 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))
;
( 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 A14:
x1 = Class (
(EqRel (S,s)),
ls1)
and A15:
(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 A16:
x2 = Class (
(EqRel (S,s)),
ls2)
and A17:
(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, Th26;
assume
(FundGrIso (f,s)) . x1 = (FundGrIso (f,s)) . x2
;
x1 = x2
then
f * ls1,
f * ls2 are_homotopic
by A15, A17, TOPALG_1:46;
then A18:
a1,
a2 are_homotopic
by A4, A3, A6, Th27;
A19:
(f ") * f = id (dom f)
by A5, A2, TOPS_2:52;
A20:
(f ") * (f * ls1) =
((f ") * f) * ls1
by RELAT_1:36
.=
ls1
by A19, FUNCT_2:17
;
(f ") * (f * ls2) =
((f ") * f) * ls2
by RELAT_1:36
.=
ls2
by A19, FUNCT_2:17
;
hence
x1 = x2
by A14, A16, A20, A18, TOPALG_1:46;
verum
end;
hence
FundGrIso (f,s) is bijective
by A8, GROUP_6:60; verum