let f be Function of (Tcircle ((0. (TOP-REAL (2 + 1))),1)),(TOP-REAL 2); ( f is without_antipodals & f is continuous implies not H1(f) is nullhomotopic Loop of (Sn1->Sn f) . c100a )
assume A1:
( f is without_antipodals & f is continuous )
; H1(f) is not nullhomotopic Loop of (Sn1->Sn f) . c100a
then reconsider L = H1(f) as Loop of (Sn1->Sn f) . c100a by Lm16;
set g = Sn1->Sn f;
set s = (Sn1->Sn f) . c100a;
not L is nullhomotopic
proof
let c be
constant Loop of
(Sn1->Sn f) . c100a;
TOPALG_6:def 3 not L,c are_homotopic
rng CircleMap = the
carrier of
(Tunit_circle 2)
by FUNCT_2:def 3;
then consider xt being
object such that A2:
xt in the
carrier of
R^1
and A3:
CircleMap . xt = (Sn1->Sn f) . c100a
by FUNCT_2:11;
reconsider xt =
xt as
Point of
R^1 by A2;
(Sn1->Sn f) . c100a in {((Sn1->Sn f) . c100a)}
by TARSKI:def 1;
then A4:
xt in CircleMap " {((Sn1->Sn f) . c100a)}
by A3, FUNCT_2:38;
then consider q being
odd Integer such that A5:
S2[
f,
xt,
q]
by A1, Lm18;
reconsider l =
liftPath (
L,
xt) as
continuous Function of
I[01],
R^1 by A4, Def10;
A6:
l . 1
= (l . 0) + q
by A5, Lm19;
A7:
CircleMap . q = c[10]
by TOPREALB:32;
A8:
CircleMap . 0 = c[10]
by TOPREALB:32;
set hh =
l - xt;
l - xt is
Path of
R^1 0,
R^1 q
then reconsider hh =
l - xt as
Path of
R^1 0,
R^1 q ;
reconsider Ch =
CircleMap * hh as
Loop of
c[10] by A7, TOPREALB:32;
reconsider X =
I[01] --> xt as
Loop of
xt by JORDAN:41;
set xx =
X - xt;
reconsider Cx =
CircleMap * (X - xt) as
Loop of
c[10] by A8;
A9:
dom Ciso = the
carrier of
INT.Group
by FUNCT_2:def 1;
A10:
Ciso . q = Class (
(EqRel ((Tunit_circle 2),c[10])),
(CircleMap * hh))
by TOPALG_5:25;
A11:
Ciso . 0 = Class (
(EqRel ((Tunit_circle 2),c[10])),
(CircleMap * (X - xt)))
by TOPALG_5:25;
Ciso . (@' 0) <> Ciso . (@' q)
by A9, FUNCT_1:def 4;
then A12:
not
Cx,
Ch are_homotopic
by A10, A11, TOPALG_1:46;
assume
L,
c are_homotopic
;
contradiction
then consider F being
Function of
[:I[01],I[01]:],
(Tunit_circle 2) such that A13:
F is
continuous
and A14:
for
t being
Point of
I[01] holds
(
F . (
t,
0)
= H1(
f)
. t &
F . (
t,1)
= c . t &
F . (
0,
t)
= (Sn1->Sn f) . c100a &
F . (1,
t)
= (Sn1->Sn f) . c100a )
;
reconsider S =
(Sn1->Sn f) . c100a as
Point of
(TOP-REAL 2) by PRE_TOPC:25;
set A =
- (Arg S);
set H =
RotateCircle (1,
(- (Arg S)));
set G =
(RotateCircle (1,(- (Arg S)))) * F;
A15:
|.(euc2cpx S).| =
|.S.|
by EUCLID_3:25
.=
1
by TOPREALB:12
;
A16:
Rotate (
(euc2cpx S),
(- (Arg S)))
= |.(euc2cpx S).|
by COMPLEX2:55;
A17:
(RotateCircle (1,(- (Arg S)))) . ((Sn1->Sn f) . c100a) =
(Rotate (- (Arg S))) . S
by FUNCT_1:49
.=
c[10]
by A16, A15, COMPLEX1:6, JORDAN24:def 3
;
now for t being Point of I[01] holds
( ((RotateCircle (1,(- (Arg S)))) * F) . (t,0) = Ch . t & ((RotateCircle (1,(- (Arg S)))) * F) . (t,1) = Cx . t & ((RotateCircle (1,(- (Arg S)))) * F) . (0,t) = c[10] & ((RotateCircle (1,(- (Arg S)))) * F) . (1,t) = c[10] )let t be
Point of
I[01];
( ((RotateCircle (1,(- (Arg S)))) * F) . (t,0) = Ch . t & ((RotateCircle (1,(- (Arg S)))) * F) . (t,1) = Cx . t & ((RotateCircle (1,(- (Arg S)))) * F) . (0,t) = c[10] & ((RotateCircle (1,(- (Arg S)))) * F) . (1,t) = c[10] )reconsider E =
eLoop 1 as
Function of
I[01],
(Tunit_circle (2 + 1)) ;
reconsider BU =
H1(
f) as
Function of
I[01],
(Tunit_circle 2) ;
reconsider T =
BU . t as
Point of
(TOP-REAL 2) by PRE_TOPC:25;
H1(
f)
= CircleMap * l
by A4, Def10;
then A18:
H1(
f)
. t = CircleMap . (l . t)
by FUNCT_2:15;
thus ((RotateCircle (1,(- (Arg S)))) * F) . (
t,
0) =
(RotateCircle (1,(- (Arg S)))) . (F . (t,j0))
by Lm1, BINOP_1:18
.=
(RotateCircle (1,(- (Arg S)))) . T
by A14
.=
CircleMap . ((l . t) - xt)
by A3, A18, Th50
.=
CircleMap . (hh . t)
by VALUED_1:4
.=
Ch . t
by FUNCT_2:15
;
( ((RotateCircle (1,(- (Arg S)))) * F) . (t,1) = Cx . t & ((RotateCircle (1,(- (Arg S)))) * F) . (0,t) = c[10] & ((RotateCircle (1,(- (Arg S)))) * F) . (1,t) = c[10] )thus ((RotateCircle (1,(- (Arg S)))) * F) . (
t,1) =
(RotateCircle (1,(- (Arg S)))) . (F . (t,j1))
by Lm1, BINOP_1:18
.=
(RotateCircle (1,(- (Arg S)))) . (c . t)
by A14
.=
(RotateCircle (1,(- (Arg S)))) . ((Sn1->Sn f) . c100a)
by TOPALG_3:21
.=
CircleMap . (xt - xt)
by A17, TOPREALB:32
.=
CircleMap . ((X . t) - xt)
.=
CircleMap . ((X - xt) . t)
by VALUED_1:4
.=
Cx . t
by FUNCT_2:15
;
( ((RotateCircle (1,(- (Arg S)))) * F) . (0,t) = c[10] & ((RotateCircle (1,(- (Arg S)))) * F) . (1,t) = c[10] )thus ((RotateCircle (1,(- (Arg S)))) * F) . (
0,
t) =
(RotateCircle (1,(- (Arg S)))) . (F . (j0,t))
by Lm1, BINOP_1:18
.=
c[10]
by A14, A17
;
((RotateCircle (1,(- (Arg S)))) * F) . (1,t) = c[10] thus ((RotateCircle (1,(- (Arg S)))) * F) . (1,
t) =
(RotateCircle (1,(- (Arg S)))) . (F . (j1,t))
by Lm1, BINOP_1:18
.=
c[10]
by A14, A17
;
verum end;
hence
contradiction
by A12, A13, BORSUK_2:def 7;
verum
end;
hence
H1(f) is not nullhomotopic Loop of (Sn1->Sn f) . c100a
; verum