:: 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;