:: The Fundamental Group
:: by Artur Korni{\l}owicz , Yasunari Shidama and Adam Grabowski
::
:: Received March 18, 2004
:: Copyright (c) 2004-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 NUMBERS, NAT_1, GROUP_1, GROUP_6, RELAT_1, FUNCT_2, STRUCT_0,
FUNCT_1, SUBSET_1, BORSUK_1, PRE_TOPC, XXREAL_1, CARD_1, XBOOLE_0,
XXREAL_0, REAL_1, ARYTM_3, RCOMP_1, TARSKI, VALUED_0, FINSEQ_1, ARYTM_1,
COMPLEX1, EUCLID, METRIC_1, FINSEQ_2, ORDINAL2, TOPS_1, SUPINF_2,
ZFMISC_1, BORSUK_2, GRAPH_1, ALGSTR_1, EQREL_1, WAYBEL20, PARTFUN1,
RELAT_2, ALGSTR_0, BINOP_1, WELLORD1, BORSUK_6, TOPALG_1, MSSUBFAM;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, EQREL_1, FUNCT_1, RELSET_1,
PARTFUN1, FUNCT_2, RELAT_2, BINOP_1, ORDINAL1, NUMBERS, XCMPLX_0,
XXREAL_0, XREAL_0, COMPLEX1, REAL_1, RCOMP_1, FINSEQ_1, VALUED_0,
RVSUM_1, FINSEQ_2, STRUCT_0, ALGSTR_0, METRIC_1, PRE_TOPC, TOPS_1,
TOPS_2, GROUP_1, BORSUK_1, RLVECT_1, EUCLID, BORSUK_2, GROUP_6, BORSUK_6;
constructors BINOP_2, COMPLEX1, REAL_1, RCOMP_1, TOPS_1, TOPS_2, GROUP_6,
T_0TOPSP, EUCLID, BORSUK_6, MONOID_0, BINOP_1;
registrations RELSET_1, FUNCT_2, XXREAL_0, XREAL_0, MEMBERED, EQREL_1,
STRUCT_0, TOPS_1, BORSUK_1, EUCLID, BORSUK_2, JORDAN5A, VALUED_0,
ZFMISC_1, MONOID_0, PRE_TOPC, RVSUM_1, TOPMETR, ORDINAL1;
requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL;
begin :: Preliminaries
reserve p, q, x, y for Real,
n for Nat;
theorem :: TOPALG_1:1
for G, H being set, g being Function of G,H, h being Function of H,G
st h * g = id G & g * h = id H holds h is bijective;
theorem :: TOPALG_1:2
for X being Subset of I[01], a being Point of I[01] st X = ]. a, 1 .]
holds X` = [. 0, a .];
theorem :: TOPALG_1:3
for X being Subset of I[01], a being Point of I[01] st X = [. 0, a .[
holds X` = [. a, 1 .];
theorem :: TOPALG_1:4
for X being Subset of I[01], a being Point of I[01] st X = ]. a, 1 .]
holds X is open;
theorem :: TOPALG_1:5
for X being Subset of I[01], a being Point of I[01] st X = [. 0, a .[
holds X is open;
theorem :: TOPALG_1:6
for f being real-valued FinSequence holds x * (-f) = - (x*f);
theorem :: TOPALG_1:7
for f, g being real-valued FinSequence holds x * (f-g) = x*f - x*g;
theorem :: TOPALG_1:8
for f being real-valued FinSequence holds (x-y) * f = x*f - y*f;
theorem :: TOPALG_1:9
for f, g, h, k being real-valued FinSequence holds (f+g)-(h+k) = (f-h)+(g-k);
theorem :: TOPALG_1:10
for f being Element of REAL n st 0 <= x & x <= 1 holds |.x*f.| <= |.f.|;
theorem :: TOPALG_1:11
for f being Element of REAL n, p being Point of I[01] holds |.p*f.| <= |.f.|;
theorem :: TOPALG_1:12
for e1, e2, e3, e4, e5, e6 being Point of Euclid n, p1, p2, p3, p4
being Point of TOP-REAL n st e1 = p1 & e2 = p2 & e3 = p3 & e4 = p4 & e5 = p1+p3
& e6 = p2+p4 & dist(e1,e2) < x & dist(e3,e4) < y holds dist(e5,e6) < x+y;
theorem :: TOPALG_1:13
for e1, e2, e5, e6 being Point of Euclid n, p1, p2 being Point
of TOP-REAL n st e1 = p1 & e2 = p2 & e5 = y*p1 & e6 = y*p2 & dist(e1,e2) < x &
y <> 0 holds dist(e5,e6) < |.y.|*x;
theorem :: TOPALG_1:14
for e1, e2, e3, e4, e5, e6 being Point of Euclid n, p1, p2, p3,
p4 being Point of TOP-REAL n st e1 = p1 & e2 = p2 & e3 = p3 & e4 = p4 & e5 = x*
p1+y*p3 & e6 = x*p2+y*p4 & dist(e1,e2) < p & dist(e3,e4) < q & x <> 0 & y <> 0
holds dist(e5,e6) < |.x.|*p + |.y.|*q;
theorem :: TOPALG_1:15
for X being non empty TopSpace, f, g being Function of X,
TOP-REAL n st f is continuous & for p being Point of X holds g.p = y * f.p
holds g is continuous;
theorem :: TOPALG_1:16
for X being non empty TopSpace, f1, f2, g being Function of X,TOP-REAL
n st f1 is continuous & f2 is continuous & for p being Point of X holds g.p = x
* f1.p + y * f2.p holds g is continuous;
theorem :: TOPALG_1:17
for F being Function of [:TOP-REAL n,I[01]:], TOP-REAL n st for
x being Point of TOP-REAL n, i being Point of I[01] holds F.(x,i) = (1-i) * x
holds F is continuous;
theorem :: TOPALG_1:18
for F being Function of [:TOP-REAL n,I[01]:], TOP-REAL n st for
x being Point of TOP-REAL n, i being Point of I[01] holds F.(x,i) = i * x holds
F is continuous;
begin :: Paths
reserve X for non empty TopSpace,
a, b, c, d, e, f for Point of X,
T for non empty pathwise_connected TopSpace,
a1, b1, c1, d1, e1, f1 for Point of T;
theorem :: TOPALG_1:19
a,b are_connected & b,c are_connected implies for A1,A2 being
Path of a,b, B being Path of b,c holds A1,A2 are_homotopic implies A1, A2+B+-B
are_homotopic;
theorem :: TOPALG_1:20
for A1,A2 being Path of a1,b1, B being Path of b1,c1 holds A1,A2
are_homotopic implies A1, A2+B+-B are_homotopic;
theorem :: TOPALG_1:21
a,b are_connected & c,b are_connected implies for A1,A2 being
Path of a,b, B being Path of c,b holds A1,A2 are_homotopic implies A1, A2+-B+B
are_homotopic;
theorem :: TOPALG_1:22
for A1,A2 being Path of a1,b1, B being Path of c1,b1 holds A1,A2
are_homotopic implies A1, A2+-B+B are_homotopic;
theorem :: TOPALG_1:23
a,b are_connected & c,a are_connected implies for A1,A2 being
Path of a,b, B being Path of c,a holds A1,A2 are_homotopic implies A1, -B+B+A2
are_homotopic;
theorem :: TOPALG_1:24
for A1,A2 being Path of a1,b1, B being Path of c1,a1 holds A1,A2
are_homotopic implies A1, -B+B+A2 are_homotopic;
theorem :: TOPALG_1:25
a,b are_connected & a,c are_connected implies for A1,A2 being
Path of a,b, B being Path of a,c holds A1,A2 are_homotopic implies A1, B+-B+A2
are_homotopic;
theorem :: TOPALG_1:26
for A1,A2 being Path of a1,b1, B being Path of a1,c1 holds A1,A2
are_homotopic implies A1, B+-B+A2 are_homotopic;
theorem :: TOPALG_1:27
a,b are_connected & c,b are_connected implies for A, B being
Path of a,b, C being Path of b,c st A+C, B+C are_homotopic holds A, B
are_homotopic;
theorem :: TOPALG_1:28
for A, B being Path of a1,b1, C being Path of b1,c1 st A+C, B+C
are_homotopic holds A, B are_homotopic;
theorem :: TOPALG_1:29
a,b are_connected & a,c are_connected implies for A, B being
Path of a,b, C being Path of c,a st C+A, C+B are_homotopic holds A, B
are_homotopic;
theorem :: TOPALG_1:30
for A, B being Path of a1,b1, C being Path of c1,a1 st C+A, C+B
are_homotopic holds A, B are_homotopic;
theorem :: TOPALG_1:31
a,b are_connected & b,c are_connected & c,d are_connected & d,e
are_connected implies for A being Path of a,b, B being Path of b,c, C being
Path of c,d, D being Path of d,e holds A+B+C+D, A+(B+C)+D are_homotopic;
theorem :: TOPALG_1:32
for A being Path of a1,b1, B being Path of b1,c1, C being Path of c1,
d1, D being Path of d1,e1 holds A+B+C+D, A+(B+C)+D are_homotopic;
theorem :: TOPALG_1:33
a,b are_connected & b,c are_connected & c,d are_connected & d,e
are_connected implies for A being Path of a,b, B being Path of b,c, C being
Path of c,d, D being Path of d,e holds A+B+C+D, A+(B+C+D) are_homotopic;
theorem :: TOPALG_1:34
for A being Path of a1,b1, B being Path of b1,c1, C being Path of c1,
d1, D being Path of d1,e1 holds A+B+C+D, A+(B+C+D) are_homotopic;
theorem :: TOPALG_1:35
a,b are_connected & b,c are_connected & c,d are_connected & d,e
are_connected implies for A being Path of a,b, B being Path of b,c, C being
Path of c,d, D being Path of d,e holds A+(B+C)+D, A+B+(C+D) are_homotopic;
theorem :: TOPALG_1:36
for A being Path of a1,b1, B being Path of b1,c1, C being Path of c1,
d1, D being Path of d1,e1 holds A+(B+C)+D, A+B+(C+D) are_homotopic;
theorem :: TOPALG_1:37
a,b are_connected & b,c are_connected & b,d are_connected
implies for A being Path of a,b, B being Path of d,b, C being Path of b,c holds
A+-B+B+C, A+C are_homotopic;
theorem :: TOPALG_1:38
for A being Path of a1,b1, B being Path of d1,b1, C being Path of b1,
c1 holds A+-B+B+C, A+C are_homotopic;
theorem :: TOPALG_1:39
a,b are_connected & a,c are_connected & c,d are_connected
implies for A being Path of a,b, B being Path of c,d, C being Path of a,c holds
A+-A+C+B+-B, C are_homotopic;
theorem :: TOPALG_1:40
for A being Path of a1,b1, B being Path of c1,d1, C being Path of a1,
c1 holds A+-A+C+B+-B, C are_homotopic;
theorem :: TOPALG_1:41
a,b are_connected & a,c are_connected & d,c are_connected
implies for A being Path of a,b, B being Path of c,d, C being Path of a,c holds
A+(-A+C+B)+-B, C are_homotopic;
theorem :: TOPALG_1:42
for A being Path of a1,b1, B being Path of c1,d1, C being Path of a1,
c1 holds A+(-A+C+B)+-B, C are_homotopic;
theorem :: TOPALG_1:43
a,b are_connected & b,c are_connected & c,d are_connected & d,e
are_connected & a,f are_connected implies for A being Path of a,b, B being Path
of b,c, C being Path of c,d, D being Path of d,e, E being Path of f,c holds A+(
B+C)+D, A+B+-E+(E+C+D) are_homotopic;
theorem :: TOPALG_1:44
for A being Path of a1,b1, B being Path of b1,c1, C being Path of c1,
d1, D being Path of d1,e1, E being Path of f1,c1 holds A+(B+C)+D, A+B+-E+(E+C+D
) are_homotopic;
begin :: Fundamental group
definition
let T be TopStruct, t be Point of T;
mode Loop of t is Path of t,t;
end;
definition
let T be non empty TopStruct, t1,t2 be Point of T;
func Paths(t1,t2) -> set means
:: TOPALG_1:def 1
for x being object holds x in it iff x is Path of t1,t2;
end;
registration
let T be non empty TopStruct, t1,t2 be Point of T;
cluster Paths(t1,t2) -> non empty;
end;
definition
let T be non empty TopStruct, t be Point of T;
func Loops(t) -> set equals
:: TOPALG_1:def 2
Paths(t,t);
end;
registration
let T be non empty TopStruct, t be Point of T;
cluster Loops(t) -> non empty;
end;
definition
let X be non empty TopSpace, a,b be Point of X such that
a,b are_connected;
func EqRel(X,a,b) -> Relation of Paths(a,b) means
:: TOPALG_1:def 3
for P, Q being Path of a,b holds [P,Q] in it iff P,Q are_homotopic;
end;
theorem :: TOPALG_1:45
a,b are_connected implies for P, Q being Path of a,b holds Q in
Class(EqRel(X,a,b),P) iff P,Q are_homotopic;
theorem :: TOPALG_1:46
a,b are_connected implies for P, Q being Path of a,b holds Class
(EqRel(X,a,b),P) = Class(EqRel(X,a,b),Q) iff P,Q are_homotopic;
definition
let X be non empty TopSpace, a be Point of X;
func EqRel(X,a) -> Relation of Loops(a) equals
:: TOPALG_1:def 4
EqRel(X,a,a);
end;
registration
let X be non empty TopSpace, a be Point of X;
cluster EqRel(X,a) -> non empty total symmetric transitive;
end;
definition
let X be non empty TopSpace, a be Point of X;
func FundamentalGroup(X,a) -> strict multMagma means
:: TOPALG_1:def 5
the carrier of
it = Class EqRel (X,a) & for x,y being Element of it ex P,Q being Loop of a st
x = Class(EqRel(X,a),P) & y = Class(EqRel(X,a),Q) & (the multF of it).(x,y) =
Class(EqRel(X,a),P+Q);
end;
notation
let X be non empty TopSpace, a be Point of X;
synonym pi_1(X,a) for FundamentalGroup(X,a);
end;
registration
let X be non empty TopSpace;
let a be Point of X;
cluster pi_1(X,a) -> non empty;
end;
theorem :: TOPALG_1:47
for x being set holds x in the carrier of pi_1(X,a) iff ex P
being Loop of a st x = Class(EqRel(X,a),P);
registration
let X be non empty TopSpace;
let a be Point of X;
cluster pi_1(X,a) -> associative Group-like;
end;
definition
let T be non empty TopSpace, x0, x1 be Point of T, P being Path of x0,x1;
assume
x0,x1 are_connected;
func pi_1-iso(P) -> Function of pi_1(T,x1), pi_1(T,x0) means
:: TOPALG_1:def 6
for Q
being Loop of x1 holds it.Class(EqRel(T,x1),Q) = Class(EqRel(T,x0),P+Q+-P);
end;
reserve x0, x1 for Point of X,
P, Q for Path of x0,x1,
y0, y1 for Point of T,
R, V for Path of y0,y1;
theorem :: TOPALG_1:48
x0,x1 are_connected & P,Q are_homotopic implies pi_1-iso(P) = pi_1-iso(Q);
theorem :: TOPALG_1:49
R,V are_homotopic implies pi_1-iso(R) = pi_1-iso(V);
theorem :: TOPALG_1:50
x0,x1 are_connected implies pi_1-iso(P) is Homomorphism of pi_1(
X,x1), pi_1(X,x0);
registration
let T be non empty pathwise_connected TopSpace, x0, x1 be Point of T,
P be Path of x0,x1;
cluster pi_1-iso(P) -> multiplicative;
end;
theorem :: TOPALG_1:51
x0,x1 are_connected implies pi_1-iso(P) is one-to-one;
theorem :: TOPALG_1:52
x0,x1 are_connected implies pi_1-iso(P) is onto;
registration
let T be non empty pathwise_connected TopSpace,
x0, x1 be Point of T, P be Path of x0,x1;
cluster pi_1-iso(P) -> one-to-one onto;
end;
theorem :: TOPALG_1:53
x0,x1 are_connected implies (pi_1-iso(P))" = pi_1-iso(-P);
theorem :: TOPALG_1:54
(pi_1-iso(R))" = pi_1-iso(-R);
theorem :: TOPALG_1:55
x0,x1 are_connected implies for h being Homomorphism of pi_1(X,
x1), pi_1(X,x0) st h = pi_1-iso(P) holds h is bijective;
theorem :: TOPALG_1:56
pi_1-iso(R) is bijective;
theorem :: TOPALG_1:57
x0,x1 are_connected implies pi_1(X,x0), pi_1(X,x1) are_isomorphic;
theorem :: TOPALG_1:58
pi_1(T,y0), pi_1(T,y1) are_isomorphic;
begin :: TOP-REAL n
definition
let n be Nat, P, Q be Function of I[01], TOP-REAL n;
func RealHomotopy(P,Q) -> Function of [:I[01],I[01]:], TOP-REAL n means
:: TOPALG_1:def 7
for s, t being Element of I[01] holds it.(s,t) = (1-t) * P.s + t * Q.s;
end;
theorem :: TOPALG_1:59
for a, b being Point of TOP-REAL n, P, Q being Path of a,b holds
P, Q are_homotopic;
registration
let n be Nat, a, b be Point of TOP-REAL n, P, Q be Path of a,b;
cluster -> continuous for Homotopy of P,Q;
end;
theorem :: TOPALG_1:60
for a being Point of TOP-REAL n, C being Loop of a holds the
carrier of pi_1(TOP-REAL n,a) = { Class(EqRel(TOP-REAL n,a),C) };
registration
let n be Nat;
let a be Point of TOP-REAL n;
cluster pi_1(TOP-REAL n,a) -> trivial;
end;
theorem :: TOPALG_1:61
for S being non empty TopSpace, s being Point of S for x, y being
Element of pi_1(S,s) for P, Q being Loop of s st x = Class(EqRel(S,s),P) & y =
Class(EqRel(S,s),Q) holds x*y = Class(EqRel(S,s),P+Q);
:: Added, AK 5.02.2007
theorem :: TOPALG_1:62
for C being constant Loop of a holds 1_pi_1(X,a) = Class(EqRel(X ,a),C);
theorem :: TOPALG_1:63
for x, y being Element of pi_1(X,a), P being Loop of a st x = Class(
EqRel(X,a),P) & y = Class(EqRel(X,a),-P) holds x" = y;
registration
let n;
let P, Q be continuous Function of I[01],TOP-REAL n;
cluster RealHomotopy(P,Q) -> continuous;
end;
theorem :: TOPALG_1:64
for a, b be Point of TOP-REAL n, P, Q be Path of a,b holds
RealHomotopy(P,Q) is Homotopy of P,Q;
theorem :: TOPALG_1:65
a,b are_connected implies EqRel(X,a,b) is non empty total symmetric
transitive;