:: The Fundamental Group
::  by Artur Korni{\l}owicz , Yasunari Shidama and Adam Grabowski
::
:: Received March 18, 2004
:: Copyright (c) 2004-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, 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;