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