:: On the Isomorphism of Fundamental Groups :: by Artur Korni{\l}owicz :: :: Received July 30, 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 STRUCT_0, BORSUK_1, ZFMISC_1, CARD_1, PRE_TOPC, FUNCT_1, FUNCT_4, FUNCOP_1, TARSKI, RELAT_1, XBOOLE_0, SUBSET_1, TEX_2, CONNSP_1, RELAT_2, COMPTS_1, ORDINAL2, FUNCT_2, RCOMP_1, T_0TOPSP, BORSUK_2, TOPS_2, EUCLID, TOPREAL2, TOPREAL1, SETFAM_1, TAXONOM2, RLVECT_3, ALGSTR_1, GRAPH_1, BORSUK_6, ARYTM_3, XXREAL_0, ARYTM_1, TOPALG_1, EQREL_1, WAYBEL20, GROUP_6, WELLORD1, TOPALG_3, MSSUBFAM; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, EQREL_1, ORDINAL1, NUMBERS, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, XCMPLX_0, FUNCOP_1, FUNCT_4, STRUCT_0, ALGSTR_0, PRE_TOPC, GROUP_6, BORSUK_1, TOPS_2, COMPTS_1, CONNSP_1, TOPREAL1, TEX_2, TOPREAL2, EUCLID, BORSUK_2, BORSUK_3, TAXONOM2, YELLOW_8, BORSUK_6, TOPALG_1, XXREAL_0; constructors REAL_1, CONNSP_1, TOPS_2, COMPTS_1, GRCAT_1, TDLAT_3, TEX_2, TOPREAL1, TOPREAL2, YELLOW_8, TAXONOM2, BORSUK_3, BORSUK_6, TOPALG_1, FUNCOP_1, GROUP_6, FUNCT_4; registrations XBOOLE_0, SUBSET_1, FUNCT_1, FUNCT_2, FUNCOP_1, XREAL_0, STRUCT_0, PRE_TOPC, TOPS_1, COMPTS_1, BORSUK_1, TEX_1, EUCLID, TOPREAL2, BORSUK_2, TOPALG_1, RELSET_1, TOPMETR, MEMBERED, RELAT_1, GROUP_6, GROUP_1; requirements NUMERALS, BOOLE, SUBSET; begin theorem :: TOPALG_3:1 for A, B, a, b being set, f being Function of A,B st a in A & b in B holds f +* (a .--> b) is Function of A,B; theorem :: TOPALG_3:2 for f being Function, X, x being set st f|X is one-to-one & x in rng ( f|X) holds (f*(f|X)").x = x; theorem :: TOPALG_3:3 for X, a, b being set, f being Function of X,{a,b} holds X = f"{a } \/ f"{b}; theorem :: TOPALG_3:4 for S, T being non empty 1-sorted, s being Point of S, t being Point of T holds (S --> t).s = t; :: Topological preliminaries theorem :: TOPALG_3:5 for T being non empty TopStruct, t being Point of T, A being Subset of T st A = {t} holds Sspace(t) = T | A; theorem :: TOPALG_3:6 for T being TopSpace, A, B being Subset of T, C, D being Subset of the TopStruct of T st A = C & B = D holds A,B are_separated iff C,D are_separated; theorem :: TOPALG_3:7 for T being non empty TopSpace holds T is connected iff not ex f being Function of T, 1TopSp{0,1} st f is continuous onto; registration cluster empty -> connected for TopStruct; end; theorem :: TOPALG_3:8 for T being TopSpace st the TopStruct of T is connected holds T is connected; registration let T be connected TopSpace; cluster the TopStruct of T -> connected; end; theorem :: TOPALG_3:9 for S, T be non empty TopSpace st S,T are_homeomorphic & S is pathwise_connected holds T is pathwise_connected; registration cluster trivial -> pathwise_connected for non empty TopSpace; end; theorem :: TOPALG_3:10 for T being SubSpace of TOP-REAL 2 st the carrier of T is Simple_closed_curve holds T is pathwise_connected; theorem :: TOPALG_3:11 for T being TopSpace ex F being Subset-Family of T st F = {the carrier of T} & F is Cover of T & F is open; registration let T be TopSpace; cluster non empty mutually-disjoint open closed for Subset-Family of T; end; theorem :: TOPALG_3:12 for T being TopSpace, D being mutually-disjoint open Subset-Family of T, A being Subset of T, X being set st A is connected & X in D & X meets A & D is Cover of A holds A c= X; begin :: On the product of topologies theorem :: TOPALG_3:13 for S, T being TopSpace holds the TopStruct of [:S,T:] = [:the TopStruct of S,the TopStruct of T:]; theorem :: TOPALG_3:14 for S, T being TopSpace, A being Subset of S, B being Subset of T holds Cl [:A,B:] = [:Cl A,Cl B:]; theorem :: TOPALG_3:15 for S, T being TopSpace, A being closed Subset of S, B being closed Subset of T holds [:A,B:] is closed; registration let A, B be connected TopSpace; cluster [:A,B:] -> connected; end; theorem :: TOPALG_3:16 for S, T being TopSpace, A being Subset of S, B being Subset of T st A is connected & B is connected holds [:A,B:] is connected; theorem :: TOPALG_3:17 for S, T be TopSpace, Y being non empty TopSpace, A being Subset of S, f being Function of [:S,T:],Y, g being Function of [:S|A,T:],Y st g = f | [:A, the carrier of T:] & f is continuous holds g is continuous; theorem :: TOPALG_3:18 for S, T be TopSpace, Y being non empty TopSpace, A being Subset of T, f being Function of [:S,T:],Y, g being Function of [:S,T|A:],Y st g = f | [:the carrier of S,A:] & f is continuous holds g is continuous; theorem :: TOPALG_3:19 for S, T, T1, T2, Y being non empty TopSpace, f being Function of [:Y, T1:],S, g being Function of [:Y,T2:],S, F1, F2 being closed Subset of T st T1 is SubSpace of T & T2 is SubSpace of T & F1 = [#]T1 & F2 = [#]T2 & ([#]T1) \/ ( [#]T2) = [#]T & f is continuous & g is continuous & (for p being set st p in ( [#][:Y,T1:]) /\ ([#][:Y,T2:]) holds f.p = g.p) ex h being Function of [:Y,T:],S st h = f+*g & h is continuous; theorem :: TOPALG_3:20 for S, T, T1, T2, Y being non empty TopSpace, f being Function of [:T1 ,Y:],S, g being Function of [:T2,Y:],S, F1, F2 being closed Subset of T st T1 is SubSpace of T & T2 is SubSpace of T & F1 = [#]T1 & F2 = [#]T2 & ([#]T1) \/ ( [#]T2) = [#]T & f is continuous & g is continuous & (for p being set st p in ( [#][:T1,Y:]) /\ ([#][:T2,Y:]) holds f.p = g.p) ex h being Function of [:T,Y:],S st h = f+*g & h is continuous; begin :: On the fundamental groups registration let T be non empty TopSpace, t be Point of T; cluster -> continuous for Loop of t; end; theorem :: TOPALG_3:21 for T being non empty TopSpace, t being Point of T, x being Point of I[01], P being constant Loop of t holds P.x = t; theorem :: TOPALG_3:22 for T being non empty TopSpace, t being Point of T, P being Loop of t holds P.0 = t & P.1 = t; theorem :: TOPALG_3:23 for S, T being non empty TopSpace, f being continuous Function of S,T, a, b being Point of S st a,b are_connected holds f.a,f.b are_connected; theorem :: TOPALG_3:24 for S, T being non empty TopSpace, f being continuous Function of S,T, a, b being Point of S, P being Path of a,b st a,b are_connected holds f*P is Path of f.a,f.b; theorem :: TOPALG_3:25 for S being non empty pathwise_connected TopSpace, T being non empty TopSpace, f being continuous Function of S,T, a, b being Point of S, P being Path of a,b holds f*P is Path of f.a,f.b; definition let S be non empty pathwise_connected TopSpace, T be non empty TopSpace, a, b be Point of S, P be Path of a,b, f be continuous Function of S,T; redefine func f*P -> Path of f.a,f.b; end; theorem :: TOPALG_3:26 for S, T being non empty TopSpace, f being continuous Function of S,T, a being Point of S, P being Loop of a holds f*P is Loop of f.a; definition let S, T be non empty TopSpace, a be Point of S, P be Loop of a, f be continuous Function of S,T; redefine func f*P -> Loop of f.a; end; theorem :: TOPALG_3:27 for S, T being non empty TopSpace, f being continuous Function of S,T, a, b being Point of S, P, Q being Path of a,b, P1, Q1 being Path of f.a ,f.b st P,Q are_homotopic & P1 = f*P & Q1 = f*Q holds P1,Q1 are_homotopic; theorem :: TOPALG_3:28 for S, T being non empty TopSpace, f being continuous Function of S,T, a, b being Point of S, P, Q being Path of a,b, P1, Q1 being Path of f.a,f.b, F being Homotopy of P,Q st P,Q are_homotopic & P1 = f*P & Q1 = f*Q holds f*F is Homotopy of P1,Q1; theorem :: TOPALG_3:29 for S, T being non empty TopSpace, f being continuous Function of S,T, a, b, c being Point of S, P being Path of a,b, Q being Path of b,c, P1 being Path of f.a,f.b, Q1 being Path of f.b,f.c st a,b are_connected & b,c are_connected & P1 = f*P & Q1 = f*Q holds P1+Q1 = f*(P+Q); definition let S, T be non empty TopSpace, s be Point of S, f be Function of S,T such that f is continuous; func FundGrIso(f,s) -> Function of pi_1(S,s),pi_1(T,f.s) means :: TOPALG_3:def 1 for x being Element of pi_1(S,s) ex ls being Loop of s st x = Class(EqRel(S,s),ls) & it.x = Class(EqRel(T,f.s),f*ls); end; theorem :: TOPALG_3:30 for S, T being non empty TopSpace, s being Point of S, f being continuous Function of S,T, ls being Loop of s holds FundGrIso(f,s).Class(EqRel (S,s),ls) = Class(EqRel(T,f.s),f*ls); registration let S, T be non empty TopSpace, s be Point of S, f be continuous Function of S,T; cluster FundGrIso(f,s) -> multiplicative; end; theorem :: TOPALG_3:31 for S, T being non empty TopSpace, s being Point of S, f being continuous Function of S,T st f is being_homeomorphism holds FundGrIso(f,s) is bijective; theorem :: TOPALG_3:32 for S, T being non empty TopSpace, s being Point of S, t being Point of T, f being continuous Function of S,T, P being Path of t,f.s, h being Homomorphism of pi_1(S,s),pi_1(T,t) st f is being_homeomorphism & f.s,t are_connected & h = pi_1-iso(P) * FundGrIso(f,s) holds h is bijective; theorem :: TOPALG_3:33 for S being non empty TopSpace, T being non empty pathwise_connected TopSpace, s being Point of S, t being Point of T st S,T are_homeomorphic holds pi_1(S,s),pi_1(T,t) are_isomorphic;