:: The Fundamental Group of the Circle
:: by Artur Korni{\l}owicz
::
:: Received February 22, 2005
:: Copyright (c) 2005-2021 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, EUCLID, CARD_1, STRUCT_0, BORSUK_1, TOPMETR, TARSKI,
ZFMISC_1, PRE_TOPC, SUBSET_1, RELAT_1, ARYTM_1, XXREAL_0, ARYTM_3,
GR_CY_1, FINSET_1, ORDINAL1, METRIC_1, XXREAL_1, XBOOLE_0, REAL_1,
RLVECT_3, PBOOLE, FUNCT_1, CARD_3, RELAT_2, PCOMPS_1, FRECHET, CONNSP_1,
CONNSP_3, RCOMP_1, CONNSP_2, TOPS_1, TOPS_2, ORDINAL2, T_0TOPSP,
CANTOR_1, SETFAM_1, GRAPH_1, BORSUK_6, TOPREALB, SUPINF_2, SIN_COS,
COMPLEX1, SQUARE_1, MCART_1, INT_1, ALGSTR_1, TAXONOM2, TEX_2, RCOMP_3,
FINSEQ_1, FUNCT_4, COMPTS_1, FUNCOP_1, BORSUK_2, TOPALG_1, EQREL_1,
WAYBEL20, TOPALG_2, GROUP_6, ALGSTR_0, JGRAPH_2, FUNCT_2, WELLORD1,
TOPREAL2, TOPALG_5, MSSUBFAM, MEASURE5, NAT_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, ORDINAL1, RELAT_1,
EQREL_1, FUNCT_1, PBOOLE, CARD_3, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1,
FINSET_1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, SQUARE_1, INT_1, NAT_1,
SEQM_3, FINSEQ_1, FUNCT_4, RCOMP_1, DOMAIN_1, STRUCT_0, ALGSTR_0,
PRE_TOPC, TOPS_1, GR_CY_1, GROUP_6, METRIC_1, CANTOR_1, YELLOW_8,
BORSUK_1, TOPS_2, COMPTS_1, CONNSP_1, CONNSP_2, CONNSP_3, TEX_2, TSEP_1,
TOPMETR, EUCLID, PCOMPS_1, FRECHET, BORSUK_2, SIN_COS, BORSUK_3, FCONT_1,
TAXONOM2, BORSUK_6, TOPALG_1, TOPREAL9, TOPALG_2, TOPREALB, RCOMP_3,
XXREAL_0;
constructors SQUARE_1, BINARITH, SIN_COS, TOPS_1, CONNSP_1, FUNCOP_1,
COMPTS_1, GRCAT_1, TSEP_1, TEX_2, CANTOR_1, MONOID_0, CONNSP_3, YELLOW_8,
TAXONOM2, BORSUK_3, FCONT_1, TOPALG_1, TOPREAL9, TOPREALB, RCOMP_3,
BORSUK_6, SEQ_4, FRECHET, GROUP_6, FUNCT_4, REAL_1, BINOP_2;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, RELSET_1, FUNCT_2, NUMBERS,
XREAL_0, NAT_1, INT_1, MEMBERED, FINSEQ_1, STRUCT_0, PRE_TOPC, TOPS_1,
COMPTS_1, METRIC_1, BORSUK_1, TSEP_1, GR_CY_1, MONOID_0, EUCLID, TOPMETR,
BORSUK_2, YELLOW13, TOPALG_1, TOPALG_2, TOPALG_3, TOPREALB, RCOMP_3,
VALUED_0, XXREAL_2, FRECHET, CONNSP_1, GROUP_6, SQUARE_1, SIN_COS,
ORDINAL1;
requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
begin
registration
cluster INT.Group -> infinite;
end;
reserve a, r, s for Real;
theorem :: TOPALG_5:1
r <= s implies for p being Point of Closed-Interval-MSpace(r,s)
holds Ball(p,a) = [.r,s.] or Ball(p,a) = [.r,p+a.[ or Ball(p,a) = ].p-a,s.] or
Ball(p,a) = ].p-a,p+a.[;
theorem :: TOPALG_5:2
r <= s implies ex B being Basis of Closed-Interval-TSpace(r,s) st
(ex f being ManySortedSet of Closed-Interval-TSpace(r,s) st for y being Point
of Closed-Interval-MSpace(r,s)
holds f.y = {Ball(y,1/n) where n is Nat: n <> 0}
& B = Union f) & for X being Subset of Closed-Interval-TSpace(r,s)
st X in B holds X is connected;
theorem :: TOPALG_5:3
for T being TopStruct, A being Subset of T, t be Point of T st t
in A holds Component_of(t,A) c= A;
registration
let T be TopSpace, A be open Subset of T;
cluster T|A -> open;
end;
theorem :: TOPALG_5:4
for T being TopSpace, S being SubSpace of T, A being Subset of T,
B being Subset of S st A = B holds T|A = S|B;
theorem :: TOPALG_5:5
for S, T being TopSpace, A, B being Subset of T, C, D being
Subset of S st the TopStruct of S = the TopStruct of T & A = C & B = D & A,B
are_separated holds C,D are_separated;
theorem :: TOPALG_5:6
for S, T being TopSpace st the TopStruct of S = the TopStruct of T & S
is connected holds T is connected;
theorem :: TOPALG_5:7
for S, T being TopSpace, A being Subset of S, B being Subset of T
st the TopStruct of S = the TopStruct of T & A = B & A is connected holds B is
connected;
theorem :: TOPALG_5:8
for S, T being non empty TopSpace, s being Point of S, t being
Point of T, A being a_neighborhood of s st the TopStruct of S = the TopStruct
of T & s = t holds A is a_neighborhood of t;
theorem :: TOPALG_5:9
for S, T being non empty TopSpace, A being Subset of S, B being Subset
of T, N being a_neighborhood of A st the TopStruct of S = the TopStruct of T &
A = B holds N is a_neighborhood of B;
theorem :: TOPALG_5:10
for S, T being non empty TopSpace, A, B being Subset of T, f
being Function of S,T st f is being_homeomorphism & A is_a_component_of B holds
f"A is_a_component_of f"B;
begin :: Locally connectedness
theorem :: TOPALG_5:11
for T being non empty TopSpace, S being non empty SubSpace of T,
A being non empty Subset of T, B being non empty Subset of S st A = B & A is
locally_connected holds B is locally_connected;
theorem :: TOPALG_5:12
for S, T being non empty TopSpace st the TopStruct of S = the
TopStruct of T & S is locally_connected holds T is locally_connected;
theorem :: TOPALG_5:13
for T being non empty TopSpace holds T is locally_connected iff
[#]T is locally_connected;
theorem :: TOPALG_5:14
for T being non empty TopSpace, S being non empty open SubSpace
of T st T is locally_connected holds S is locally_connected;
theorem :: TOPALG_5:15
for S, T being non empty TopSpace st S,T are_homeomorphic & S is
locally_connected holds T is locally_connected;
theorem :: TOPALG_5:16
for T being non empty TopSpace st ex B being Basis of T st for X
being Subset of T st X in B holds X is connected holds T is locally_connected
;
theorem :: TOPALG_5:17
r <= s implies Closed-Interval-TSpace(r,s) is locally_connected;
registration
cluster I[01] -> locally_connected;
end;
registration
let A be non empty open Subset of I[01];
cluster I[01] | A -> locally_connected;
end;
begin :: Some useful functions
definition
let r be Real;
func ExtendInt(r) -> Function of I[01], R^1 means
:: TOPALG_5:def 1
for x being Point of I[01] holds it.x = r*x;
end;
registration
let r be Real;
cluster ExtendInt(r) -> continuous;
end;
definition
let r be Real;
redefine func ExtendInt(r) -> Path of R^1(0),R^1(r);
end;
definition
let S, T, Y be non empty TopSpace, H be Function of [:S,T:],Y, t be Point of
T;
func Prj1(t,H) -> Function of S,Y means
:: TOPALG_5:def 2
for s being Point of S holds it.s = H.(s,t);
end;
definition
let S, T, Y be non empty TopSpace, H be Function of [:S,T:],Y, s be Point of
S;
func Prj2(s,H) -> Function of T,Y means
:: TOPALG_5:def 3
for t being Point of T holds it.t = H.(s,t);
end;
registration
let S, T, Y be non empty TopSpace, H be continuous Function of [:S,T:],Y, t
be Point of T;
cluster Prj1(t,H) -> continuous;
end;
registration
let S, T, Y be non empty TopSpace, H be continuous Function of [:S,T:],Y, s
be Point of S;
cluster Prj2(s,H) -> continuous;
end;
theorem :: TOPALG_5:18
for T being non empty TopSpace, a, b being Point of T, P, Q being Path
of a,b, H being Homotopy of P,Q, t being Point of I[01] st H is continuous
holds Prj1(t,H) is continuous;
theorem :: TOPALG_5:19
for T being non empty TopSpace, a, b being Point of T, P, Q being Path
of a,b, H being Homotopy of P,Q, s being Point of I[01] st H is continuous
holds Prj2(s,H) is continuous;
definition
let r be Real;
func cLoop(r) -> Function of I[01], Tunit_circle(2) means
:: TOPALG_5:def 4
for x being Point of I[01] holds it.x = |[ cos(2*PI*r*x), sin(2*PI*r*x) ]|;
end;
theorem :: TOPALG_5:20
cLoop(r) = CircleMap * ExtendInt(r);
definition
let n be Integer;
redefine func cLoop(n) -> Loop of c[10];
end;
begin
theorem :: TOPALG_5:21
for UL being Subset-Family of Tunit_circle(2) st UL is Cover of
Tunit_circle(2) & UL is open for Y being non empty TopSpace, F being continuous
Function of [:Y,I[01]:], Tunit_circle(2), y being Point of Y ex T being non
empty FinSequence of REAL st T.1 = 0 & T.len T = 1 & T is increasing & ex N
being open Subset of Y st y in N & for i being Nat st i in dom T & i
+1 in dom T ex Ui being non empty Subset of Tunit_circle(2) st Ui in UL & F.:[:
N,[.T.i,T.(i+1).]:] c= Ui;
theorem :: TOPALG_5:22
for Y being non empty TopSpace, F being Function of [:Y,I[01]:],
Tunit_circle(2), Ft being Function of [:Y,Sspace(0[01]):], R^1 st F is
continuous & Ft is continuous & F | [:the carrier of Y,{0}:] = CircleMap*Ft ex
G being Function of [:Y,I[01]:], R^1 st G is continuous & F = CircleMap*G & G |
[:the carrier of Y,{0}:] = Ft & for H being Function of [:Y,I[01]:], R^1 st H
is continuous & F = CircleMap*H & H | [:the carrier of Y,{0}:] = Ft holds G = H
;
theorem :: TOPALG_5:23
for x0, y0 being Point of Tunit_circle(2), xt being Point of R^1
, f being Path of x0,y0 st xt in (CircleMap)"{x0} ex ft being Function of I[01]
, R^1 st ft.0 = xt & f = CircleMap*ft & ft is continuous & for f1 being
Function of I[01], R^1 st f1 is continuous & f = CircleMap*f1 & f1.0 = xt holds
ft = f1;
theorem :: TOPALG_5:24
for x0, y0 being Point of Tunit_circle(2), P, Q being Path of x0
,y0, F being Homotopy of P,Q, xt being Point of R^1 st P,Q are_homotopic & xt
in (CircleMap)"{x0} ex yt being Point of R^1, Pt, Qt being Path of xt,yt, Ft
being Homotopy of Pt,Qt st Pt,Qt are_homotopic & F = CircleMap*Ft & yt in (
CircleMap)"{y0} & for F1 being Homotopy of Pt,Qt st F = CircleMap*F1 holds Ft =
F1;
definition
func Ciso -> Function of INT.Group, pi_1(Tunit_circle(2),c[10]) means
:: TOPALG_5:def 5
for n being Integer holds it.n = Class(EqRel(Tunit_circle(2),c[10]),cLoop(n));
end;
theorem :: TOPALG_5:25
for i being Integer, f being Path of R^1(0),R^1(i) holds Ciso.i
= Class(EqRel(Tunit_circle(2),c[10]),CircleMap*f);
registration
cluster Ciso -> multiplicative;
end;
registration
cluster Ciso -> one-to-one onto;
end;
theorem :: TOPALG_5:26
Ciso is bijective;
theorem :: TOPALG_5:27
for S being being_simple_closed_curve SubSpace of TOP-REAL 2, x
being Point of S holds INT.Group, pi_1(S,x) are_isomorphic;
registration
let S be being_simple_closed_curve SubSpace of TOP-REAL 2, x be Point of S;
cluster pi_1(S,x) -> infinite;
end;