:: Fundamental Group of $n$-sphere for $n \geq 2$
:: by Marco Riccardi and Artur Korni{\l}owicz
::
:: Received November 3, 2011
:: Copyright (c) 2011-2016 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies PRE_TOPC, FUNCT_1, EUCLID, RELAT_1, ARYTM_1, BORSUK_2, GRAPH_1,
ALGSTR_1, WAYBEL20, EQREL_1, NAT_1, XBOOLE_0, ARYTM_3, TOPALG_1, TOPS_2,
TOPREALB, T_0TOPSP, STRUCT_0, BORSUK_1, FUNCOP_1, SUBSET_1, TOPALG_3,
TARSKI, XREAL_0, FUNCT_2, XXREAL_0, ZFMISC_1, NUMBERS, RCOMP_1, ORDINAL2,
CARD_1, XXREAL_1, CONNSP_2, TOPMETR, MFOLD_2, PARTFUN1, METRIC_1,
CONVEX1, INCSP_1, RLTOPSP1, RVSUM_1, REAL_1, COMPLEX1, FINSEQ_1,
MEASURE5, XXREAL_2, FINSET_1, FINSEQ_2, MFOLD_1, VALUED_0, SERIES_1,
CARD_3, ORDINAL4, MEMBERED, SUPINF_2, TREAL_1, TOPREAL1, FUNCT_4,
TOPALG_6, BROUWER, XCMPLX_0;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, EQREL_1, RELAT_1, COMPLEX1,
FUNCOP_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, RVSUM_1, REAL_1, BINOP_1,
ORDINAL1, NUMBERS, XXREAL_0, XREAL_0, XCMPLX_0, NAT_1, FINSET_1,
STRUCT_0, PRE_TOPC, TOPS_2, BORSUK_1, CONNSP_2, TOPMETR, EUCLID,
BORSUK_2, TOPALG_1, TOPALG_3, TOPREALB, VALUED_0, METRIC_1, TOPREAL9,
TOPALG_2, RLTOPSP1, COMPTS_1, FINSEQ_1, TBSP_1, FINSEQ_2, METRIZTS,
RLVECT_1, XXREAL_1, XXREAL_2, NAT_D, BORSUK_6, MEMBERED, RCOMP_1,
BROUWER, MFOLD_0, MFOLD_1, MFOLD_2, TOPREAL1, FUNCT_4;
constructors BORSUK_6, BORSUK_3, TOPALG_3, SEQ_4, TOPREAL9, TOPREALB, MFOLD_2,
BINOP_2, FUNCSDOM, CONVEX1, MONOID_0, COMPTS_1, TBSP_1, BROUWER, MFOLD_0,
MFOLD_1, METRIZTS, NAT_D, TREAL_1, TOPREAL1, WAYBEL23, REAL_1, NUMBERS;
registrations RELSET_1, XXREAL_0, XREAL_0, MEMBERED, STRUCT_0, BORSUK_1,
EUCLID, BORSUK_2, TOPALG_1, PRE_TOPC, ZFMISC_1, TOPGRP_1, TOPMETR,
RCOMP_3, XXREAL_2, TEX_1, TOPALG_3, FUNCT_2, FUNCT_1, FUNCOP_1, MFOLD_2,
XBOOLE_0, RELAT_1, PARTFUN1, NAT_1, MONOID_0, VALUED_0, FINSET_1,
FINSEQ_1, FINSEQ_2, NUMBERS, TOPALG_2, TOPREAL9, TBSP_1, MFOLD_0,
MFOLD_1, BORSUK_3, TOPREAL6, TOPREALB, ORDINAL1, CARD_1;
requirements REAL, ARITHM, BOOLE, SUBSET, NUMERALS;
begin :: Preliminaries
reserve T,U for non empty TopSpace;
reserve t for Point of T;
reserve n for Nat;
registration
let S be TopSpace, T be non empty TopSpace;
cluster constant -> continuous for Function of S,T;
end;
theorem :: TOPALG_6:1
L[01](0,1,0,1) = id Closed-Interval-TSpace(0,1);
theorem :: TOPALG_6:2
for r1,r2,r3,r4,r5,r6 being Real
st r1 < r2 & r3 <= r4 & r5 < r6
holds L[01](r1,r2,r3,r4)*L[01](r5,r6,r1,r2) = L[01](r5,r6,r3,r4);
registration
let n be positive Nat;
cluster TOP-REAL n -> infinite;
cluster n-locally_euclidean -> infinite for non empty TopSpace;
end;
theorem :: TOPALG_6:3
for p being Point of TOP-REAL n st p in Sphere(0.TOP-REAL n,1)
holds -p in Sphere(0.TOP-REAL n,1) \ {p};
theorem :: TOPALG_6:4
for T being non empty TopStruct, t1,t2 being Point of T
for p being Path of t1,t2
holds inf dom p = 0 & sup dom p = 1;
theorem :: TOPALG_6:5
for C1,C2 being constant Loop of t holds
C1, C2 are_homotopic;
theorem :: TOPALG_6:6
for S being non empty SubSpace of T,
t1,t2 being Point of T, s1,s2 being Point of S,
A,B being Path of t1,t2, C,D being Path of s1,s2 st
s1,s2 are_connected & t1,t2 are_connected & A = C & B = D & C,D are_homotopic
holds A,B are_homotopic;
theorem :: TOPALG_6:7
for S being non empty SubSpace of T,
t1,t2 being Point of T, s1,s2 being Point of S,
A,B being Path of t1,t2, C,D being Path of s1,s2 st
s1,s2 are_connected & t1,t2 are_connected & A = C & B = D &
Class(EqRel(S,s1,s2),C) = Class(EqRel(S,s1,s2),D) holds
Class(EqRel(T,t1,t2),A) = Class(EqRel(T,t1,t2),B);
theorem :: TOPALG_6:8
for T being trivial non empty TopSpace
for t being Point of T, L being Loop of t holds
the carrier of pi_1(T,t) = { Class(EqRel(T,t),L) };
theorem :: TOPALG_6:9
for p being Point of TOP-REAL n, S being Subset of TOP-REAL n
st n >= 2 & S = ([#]TOP-REAL n) \ {p}
holds (TOP-REAL n) | S is pathwise_connected;
theorem :: TOPALG_6:10
for S being non empty Subset of T
st n >= 2 & S = ([#]T) \ {t} & TOP-REAL n, T are_homeomorphic
holds T | S is pathwise_connected;
registration
let n be Element of NAT;
let p,q be Point of TOP-REAL n;
cluster TPlane(p,q) -> convex;
end;
begin :: Fundamental groups
definition
let T;
attr T is having_trivial_Fundamental_Group means
:: TOPALG_6:def 1
for t being Point of T holds pi_1(T,t) is trivial;
end;
definition
let T;
attr T is simply_connected means
:: TOPALG_6:def 2
T is having_trivial_Fundamental_Group pathwise_connected;
end;
registration
cluster simply_connected ->
having_trivial_Fundamental_Group pathwise_connected
for non empty TopSpace;
cluster having_trivial_Fundamental_Group pathwise_connected ->
simply_connected for non empty TopSpace;
end;
theorem :: TOPALG_6:11
T is having_trivial_Fundamental_Group implies
for t being Point of T, P,Q being Loop of t holds
P,Q are_homotopic;
registration
let n be Nat;
cluster TOP-REAL n -> having_trivial_Fundamental_Group;
end;
registration
cluster trivial -> having_trivial_Fundamental_Group for non empty TopSpace;
end;
theorem :: TOPALG_6:12
T is simply_connected iff
for t1,t2 being Point of T holds t1,t2 are_connected &
for P, Q being Path of t1,t2 holds
Class(EqRel(T,t1,t2),P) = Class(EqRel(T,t1,t2),Q);
registration
let T be having_trivial_Fundamental_Group non empty TopSpace;
let t be Point of T;
cluster pi_1(T,t) -> trivial;
end;
theorem :: TOPALG_6:13
for S, T being non empty TopSpace st S,T are_homeomorphic holds
S is having_trivial_Fundamental_Group implies
T is having_trivial_Fundamental_Group;
theorem :: TOPALG_6:14
for S, T being non empty TopSpace st S,T are_homeomorphic holds
S is simply_connected implies T is simply_connected;
theorem :: TOPALG_6:15
for T being having_trivial_Fundamental_Group non empty TopSpace,
t being Point of T, P1,P2 being Loop of t
holds P1,P2 are_homotopic;
definition
let T, t;
let l be Loop of t;
attr l is nullhomotopic means
:: TOPALG_6:def 3
ex c being constant Loop of t st l,c are_homotopic;
end;
registration
let T, t;
cluster constant -> nullhomotopic for Loop of t;
end;
registration
let T, t;
cluster constant for Loop of t;
end;
theorem :: TOPALG_6:16
for f being Loop of t, g being continuous Function of T,U st
f is nullhomotopic holds g*f is nullhomotopic;
registration
let T, U be non empty TopSpace,
t be Point of T,
f be nullhomotopic Loop of t,
g be continuous Function of T,U;
cluster g*f -> nullhomotopic for Loop of g.t;
end;
registration
let T be having_trivial_Fundamental_Group non empty TopSpace;
let t be Point of T;
cluster -> nullhomotopic for Loop of t;
end;
theorem :: TOPALG_6:17
(for t being Point of T, f being Loop of t holds f is nullhomotopic)
implies T is having_trivial_Fundamental_Group;
registration
let n be Element of NAT;
let p,q be Point of TOP-REAL n;
cluster TPlane(p,q) -> having_trivial_Fundamental_Group;
end;
theorem :: TOPALG_6:18
for S being non empty SubSpace of T, s being Point of S,
f being Loop of t, g being Loop of s st
t = s & f = g & g is nullhomotopic
holds f is nullhomotopic;
begin :: Curves
reserve T for TopStruct;
reserve f for PartFunc of R^1, T;
definition
let T,f;
attr f is parametrized-curve means
:: TOPALG_6:def 4
dom f is interval Subset of REAL &
ex S being SubSpace of R^1, g being Function of S, T
st f = g & S = R^1|dom f & g is continuous;
end;
registration
let T;
cluster parametrized-curve for PartFunc of R^1, T;
end;
theorem :: TOPALG_6:19
{} is parametrized-curve PartFunc of R^1, T;
definition
let T;
func Curves T -> Subset of PFuncs(REAL, [#]T) equals
:: TOPALG_6:def 5
{f where f is Element of PFuncs(REAL, [#]T) :
f is parametrized-curve PartFunc of R^1, T};
end;
registration
let T;
cluster Curves T -> non empty;
end;
definition
let T;
mode Curve of T is Element of Curves T;
end;
reserve c for Curve of T;
theorem :: TOPALG_6:20
for f being parametrized-curve PartFunc of R^1, T holds f is Curve of T;
theorem :: TOPALG_6:21
{} is Curve of T;
theorem :: TOPALG_6:22
for t1,t2 being Point of T
for p being Path of t1,t2 st t1,t2 are_connected holds p is Curve of T;
theorem :: TOPALG_6:23
c is parametrized-curve PartFunc of R^1, T;
theorem :: TOPALG_6:24
dom c c= REAL & rng c c= [#]T;
registration
let T,c;
cluster dom c -> real-membered;
end;
definition
let T,c;
attr c is with_first_point means
:: TOPALG_6:def 6
dom c is left_end;
attr c is with_last_point means
:: TOPALG_6:def 7
dom c is right_end;
end;
definition
let T,c;
attr c is with_endpoints means
:: TOPALG_6:def 8
c is with_first_point with_last_point;
end;
registration
let T;
cluster with_first_point with_last_point -> with_endpoints for Curve of T;
cluster with_endpoints -> with_first_point with_last_point for Curve of T;
end;
reserve T for non empty TopStruct;
registration
let T;
cluster with_endpoints for Curve of T;
end;
registration
let T;
let c be with_first_point Curve of T;
cluster dom c -> non empty;
cluster inf dom c -> real;
end;
registration
let T;
let c be with_last_point Curve of T;
cluster dom c -> non empty;
cluster sup dom c -> real;
end;
registration
let T;
cluster with_first_point -> non empty for Curve of T;
cluster with_last_point -> non empty for Curve of T;
end;
definition
let T;
let c be with_first_point Curve of T;
func the_first_point_of c -> Point of T equals
:: TOPALG_6:def 9
c.(inf dom c);
end;
definition
let T;
let c be with_last_point Curve of T;
func the_last_point_of c -> Point of T equals
:: TOPALG_6:def 10
c.(sup dom c);
end;
theorem :: TOPALG_6:25
for t1,t2 being Point of T
for p being Path of t1,t2 st t1,t2 are_connected
holds p is with_endpoints Curve of T;
theorem :: TOPALG_6:26
for c being Curve of T
for r1,r2 being Real
holds c | [.r1, r2.] is Curve of T;
theorem :: TOPALG_6:27
for c being with_endpoints Curve of T holds
dom c = [.inf dom c, sup dom c.];
theorem :: TOPALG_6:28
for c being with_endpoints Curve of T st dom c = [.0,1.]
holds c is Path of the_first_point_of c,the_last_point_of c;
theorem :: TOPALG_6:29
for c being with_endpoints Curve of T holds
c*L[01](0,1,inf dom c,sup dom c)
is Path of the_first_point_of c,the_last_point_of c;
theorem :: TOPALG_6:30
for c being with_endpoints Curve of T,
t1,t2 being Point of T
st c*L[01](0,1,inf dom c,sup dom c) is Path of t1,t2 & t1,t2 are_connected
holds t1 = the_first_point_of c & t2 = the_last_point_of c;
theorem :: TOPALG_6:31
for c being with_endpoints Curve of T
holds the_first_point_of c in rng c & the_last_point_of c in rng c;
theorem :: TOPALG_6:32
for r1,r2 being Real
for t1,t2 being Point of T
for p1 being Path of t1,t2
st t1,t2 are_connected & r1 < r2
holds p1*L[01](r1,r2,0,1) is with_endpoints Curve of T;
theorem :: TOPALG_6:33
for c being with_endpoints Curve of T
holds the_first_point_of c, the_last_point_of c are_connected;
definition
let T be non empty TopStruct;
let c1,c2 be with_endpoints Curve of T;
pred c1,c2 are_homotopic means
:: TOPALG_6:def 11
ex a,b being Point of T, p1,p2 being Path of a,b st
p1 = c1*L[01](0,1,inf dom c1,sup dom c1) &
p2 = c2*L[01](0,1,inf dom c2,sup dom c2) &
p1,p2 are_homotopic;
symmetry;
end;
definition
let T be non empty TopSpace;
let c1,c2 be with_endpoints Curve of T;
redefine pred c1,c2 are_homotopic;
reflexivity;
symmetry;
end;
theorem :: TOPALG_6:34
for T being non empty TopStruct,
c1,c2 being with_endpoints Curve of T,
a,b being Point of T,
p1,p2 being Path of a,b
st c1 = p1 & c2 = p2 & a,b are_connected
holds c1,c2 are_homotopic iff p1,p2 are_homotopic;
theorem :: TOPALG_6:35
for c1,c2 being with_endpoints Curve of T
st c1, c2 are_homotopic
holds the_first_point_of c1 = the_first_point_of c2 &
the_last_point_of c1 = the_last_point_of c2;
theorem :: TOPALG_6:36
for T being non empty TopSpace
for c1,c2 being with_endpoints Curve of T
for S being Subset of R^1
st dom c1 = dom c2 & S = dom c1 holds c1,c2 are_homotopic iff
ex f being Function of [:R^1|S,I[01]:], T, a,b being Point of T
st f is continuous &
(for t being Point of R^1|S holds f.(t,0) = c1.t & f.(t,1) = c2.t) &
(for t being Point of I[01] holds f.(inf S,t) = a & f.(sup S,t) = b);
definition
let T be TopStruct;
let c1, c2 be Curve of T;
func c1 + c2 -> Curve of T equals
:: TOPALG_6:def 12
c1 \/ c2 if c1 \/ c2 is Curve of T otherwise {};
end;
theorem :: TOPALG_6:37
for c being with_endpoints Curve of T
for r being Real holds
ex c1,c2 being Element of Curves T
st c = c1 + c2 & c1 = c | [.inf dom c, r.] & c2 = c | [.r, sup dom c.];
theorem :: TOPALG_6:38
for T being non empty TopSpace
for c1,c2 being with_endpoints Curve of T
st sup dom c1 = inf dom c2 & the_last_point_of c1 = the_first_point_of c2
holds c1 + c2 is with_endpoints &
dom(c1 + c2) = [.inf dom c1, sup dom c2.] &
(c1+c2).inf dom c1 = the_first_point_of c1 &
(c1+c2).sup dom c2 = the_last_point_of c2;
theorem :: TOPALG_6:39
for T being non empty TopSpace
for c1,c2,c3,c4,c5,c6 being with_endpoints Curve of T
st c1,c2 are_homotopic & dom c1 = dom c2 &
c3,c4 are_homotopic & dom c3 = dom c4 &
c5 = c1 + c3 & c6 = c2 + c4
& the_last_point_of c1 = the_first_point_of c3
& sup dom c1 = inf dom c3
holds c5,c6 are_homotopic;
definition
let T be TopStruct;
let f be FinSequence of Curves T;
func Partial_Sums f -> FinSequence of Curves T means
:: TOPALG_6:def 13
len f = len it & f.1 = it.1 & for i being Nat
st 1<=i & i Curve of T equals
:: TOPALG_6:def 14
(Partial_Sums f).len f if len f > 0 otherwise {};
end;
theorem :: TOPALG_6:40
for c being Curve of T holds Sum <*c*> = c;
theorem :: TOPALG_6:41
for c being Curve of T,
f being FinSequence of Curves T holds Sum(f ^ <*c*>) = Sum f + c;
theorem :: TOPALG_6:42
for X being set, f being FinSequence of Curves T
st (for i being Nat st 1 <= i & i <= len f holds rng(f/.i) c= X)
holds rng Sum f c= X;
theorem :: TOPALG_6:43
for T being non empty TopSpace
for f being FinSequence of Curves T
st len f > 0 &
(for i being Nat st 1 <= i & i < len f
holds (f/.i).sup dom(f/.i) = (f/.(i+1)).inf dom(f/.(i+1))
& sup dom(f/.i) = inf dom(f/.(i+1))) &
(for i being Nat st 1 <= i & i <= len f
holds f/.i is with_endpoints)
holds ex c being with_endpoints Curve of T st
Sum f = c & dom c = [.inf dom(f/.1), sup dom(f/.(len f)).] &
the_first_point_of c = (f/.1).(inf dom(f/.1)) &
the_last_point_of c = (f/.(len f)).(sup dom(f/.(len f)));
theorem :: TOPALG_6:44
for T being non empty TopSpace
for f1,f2 being FinSequence of Curves T
for c1,c2 being with_endpoints Curve of T
st len f1 > 0 & len f1 = len f2 & Sum f1 = c1 & Sum f2 = c2 &
(for i being Nat st 1 <= i & i < len f1
holds (f1/.i).sup dom(f1/.i) = (f1/.(i+1)).inf dom(f1/.(i+1))
& sup dom(f1/.i) = inf dom(f1/.(i+1))) &
(for i being Nat st 1 <= i & i < len f2
holds (f2/.i).sup dom(f2/.i) = (f2/.(i+1)).inf dom(f2/.(i+1))
& sup dom(f2/.i) = inf dom(f2/.(i+1)) ) &
(for i being Nat st 1 <= i & i <= len f1 holds
ex c3,c4 being with_endpoints Curve of T st c3 = f1/.i & c4 = f2/.i
& c3,c4 are_homotopic & dom c3 = dom c4)
holds c1,c2 are_homotopic;
theorem :: TOPALG_6:45
for c being with_endpoints Curve of T
for h being FinSequence of REAL
st len h >= 2 & h.1 = inf dom c & h.len h = sup dom c & h is increasing
holds
ex f being FinSequence of Curves T
st len f = len h - 1 & c = Sum f &
(for i being Nat st 1 <= i & i <= len f
holds f/.i = c | ([.h/.i,h/.(i+1).]));
theorem :: TOPALG_6:46
n >= 2 implies TUnitSphere(n) is having_trivial_Fundamental_Group;
theorem :: TOPALG_6:47
for n being non zero Nat, r being positive Real,
x being Point of TOP-REAL n st n >= 3 holds
Tcircle(x,r) is having_trivial_Fundamental_Group;