:: On the Isomorphism of Fundamental Groups
:: by Artur Korni{\l}owicz
::
:: Received July 30, 2004
:: Copyright (c) 2004-2026 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;
definitions TARSKI, XBOOLE_0, FUNCT_1, FUNCT_2, GROUP_6, TOPS_2, T_0TOPSP,
BORSUK_2, BORSUK_6, CONNSP_1;
equalities STRUCT_0, FUNCOP_1, TOPALG_1;
expansions XBOOLE_0, FUNCT_2, TOPS_2, BORSUK_2, CONNSP_1, STRUCT_0;
theorems GROUP_6, PRE_TOPC, FUNCT_2, BORSUK_1, TOPALG_1, TOPS_2, BORSUK_3,
FUNCT_1, TOPMETR, RELAT_1, FUNCOP_1, TOPREAL6, BORSUK_6, BORSUK_2,
BINOP_1, TARSKI, PCOMPS_1, ZFMISC_1, FUNCT_4, TSEP_1, XBOOLE_1, TOPREAL1,
TOPREAL2, XBOOLE_0, TAXONOM2, TEX_2, CONNSP_1, TDLAT_3, ENUMSET1,
YELLOW12, TOPS_3, YELLOW13, YELLOW_8, SETFAM_1;
schemes FUNCT_2;
begin :: Preliminaries
set I = the carrier of I[01];
Lm1: the carrier of [:I[01],I[01]:] = [:I,I:] by BORSUK_1:def 2;
reconsider j0 = 0, j1 = 1 as Point of I[01] by BORSUK_1:def 14,def 15;
theorem
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
proof
let A, B, a, b be set, f be Function of A,B such that
A1: a in A and
A2: b in B;
A3: {a} c= A by A1,ZFMISC_1:31;
set g = a .--> b;
set f1 = f +* g;
rng g = {b} by FUNCOP_1:8;
then rng g c= B by A2,ZFMISC_1:31;
then
A4: rng f1 c= rng f \/ rng g & rng f \/ rng g c= B \/ B by FUNCT_4:17
,XBOOLE_1:13;
dom f1 = dom f \/ dom g by FUNCT_4:def 1
.= A \/ dom g by A2,FUNCT_2:def 1
.= A \/ {a}
.= A by A3,XBOOLE_1:12;
hence thesis by A4,FUNCT_2:2,XBOOLE_1:1;
end;
theorem
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
proof
let f be Function, X, x be set;
set g = f|X;
assume that
A1: g is one-to-one and
A2: x in rng g;
consider a being object such that
A3: a in dom g and
A4: g.a = x by A2,FUNCT_1:def 3;
dom g = dom f /\ X by RELAT_1:61;
then
A5: a in X by A3,XBOOLE_0:def 4;
dom (g") = rng g by A1,FUNCT_1:32;
hence (f*g").x = f.(g".x) by A2,FUNCT_1:13
.= f.a by A1,A3,A4,FUNCT_1:32
.= x by A4,A5,FUNCT_1:49;
end;
theorem Th3:
for X, a, b being set, f being Function of X,{a,b} holds X = f"{a } \/ f"{b}
proof
let X, a, b be set;
let f be Function of X,{a,b};
thus X = f"{a,b} by FUNCT_2:40
.= f"({a}\/{b}) by ENUMSET1:1
.= f"{a} \/ f"{b} by RELAT_1:140;
end;
theorem
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
for T being non empty TopStruct, t being Point of T, A being Subset of
T st A = {t} holds Sspace(t) = T | A
proof
let T be non empty TopStruct, t be Point of T, A be Subset of T such that
A1: A = {t};
the carrier of Sspace(t) = {t} by TEX_2:def 2
.= [#](T|A) by A1,PRE_TOPC:def 5
.= the carrier of (T|A);
hence thesis by TSEP_1:5;
end;
theorem Th6:
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
by TOPS_3:80;
theorem Th7:
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
proof
set X = {0}, Y = {1};
set J = 1TopSp{0,1};
let T be non empty TopSpace;
A1: the carrier of J = {0,1} by PCOMPS_1:5;
then reconsider X, Y as non empty open Subset of J by TDLAT_3:15,ZFMISC_1:7;
thus T is connected implies not ex f being Function of T,J st f is
continuous onto
proof
assume
A2: T is connected;
given f being Function of T,J such that
A3: f is continuous and
A4: f is onto;
set A = f"X, B = f"Y;
rng f = the carrier of J by A4;
then
A5: A <> {}T & B <> {}T by RELAT_1:139;
A6: the carrier of T = A \/ B & A misses B by A1,Th3,FUNCT_1:71,ZFMISC_1:11;
[#]J <> {};
then A is open & B is open by A3,TOPS_2:43;
hence contradiction by A2,A5,A6,CONNSP_1:11;
end;
reconsider j0 = 0, j1 = 1 as Element of J by A1,TARSKI:def 2;
assume
A7: not ex f being Function of T,J st f is continuous onto;
deffunc G(object) = j1;
deffunc F(object) = j0;
assume not thesis;
then consider A, B being Subset of T such that
A8: [#]T = A \/ B and
A9: A <> {}T and
A10: B <> {}T and
A11: A is open & B is open and
A12: A misses B by CONNSP_1:11;
defpred C[object] means $1 in A;
A13: for x being object st x in the carrier of T holds (C[x] implies F(x) in
the carrier of J) & (not C[x] implies G(x) in the carrier of J);
consider f being Function of the carrier of T, the carrier of J such that
A14: for x being object st x in the carrier of T holds (C[x] implies f.x =
F(x)) & (not C[x] implies f.x = G(x)) from FUNCT_2:sch 5(A13);
reconsider f as Function of T,J;
A15: dom f = the carrier of T by FUNCT_2:def 1;
A16: f"Y = B
proof
hereby
let x be object;
assume
A17: x in f"Y;
then f.x in Y by FUNCT_1:def 7;
then f.x = 1 by TARSKI:def 1;
then not C[x] by A14;
hence x in B by A8,A17,XBOOLE_0:def 3;
end;
let x be object;
assume
A18: x in B;
then not x in A by A12,XBOOLE_0:3;
then f.x = 1 by A14,A18;
then f.x in Y by TARSKI:def 1;
hence thesis by A15,A18,FUNCT_1:def 7;
end;
A19: f"X = A
proof
hereby
let x be object;
assume
A20: x in f"X;
then f.x in X by FUNCT_1:def 7;
then f.x = 0 by TARSKI:def 1;
hence x in A by A14,A20;
end;
let x be object;
assume
A21: x in A;
then f.x = 0 by A14;
then f.x in X by TARSKI:def 1;
hence thesis by A15,A21,FUNCT_1:def 7;
end;
A22: rng f = the carrier of J
proof
thus rng f c= the carrier of J;
let y be object;
assume
A23: y in the carrier of J;
per cases by A1,A23,TARSKI:def 2;
suppose
A24: y = 0;
consider x being object such that
A25: x in f"X by A9,A19,XBOOLE_0:def 1;
f.x in X by A25,FUNCT_1:def 7;
then
A26: f.x = 0 by TARSKI:def 1;
x in dom f by A25,FUNCT_1:def 7;
hence thesis by A24,A26,FUNCT_1:def 3;
end;
suppose
A27: y = 1;
consider x being object such that
A28: x in f"Y by A10,A16,XBOOLE_0:def 1;
f.x in Y by A28,FUNCT_1:def 7;
then
A29: f.x = 1 by TARSKI:def 1;
x in dom f by A28,FUNCT_1:def 7;
hence thesis by A27,A29,FUNCT_1:def 3;
end;
end;
then f"{}J = {}T & f"[#]J = [#]T by A15,RELAT_1:134;
then [#]J <> {} & for P being Subset of J st P is open holds f"P is open by
A1,A11,A19,A16,ZFMISC_1:36;
then
A30: f is continuous by TOPS_2:43;
f is onto by A22;
hence thesis by A7,A30;
end;
registration
cluster empty -> connected for TopStruct;
coherence;
end;
theorem
for T being TopSpace st the TopStruct of T is connected holds T is connected
proof
let T be TopSpace;
set G = the TopStruct of T;
assume
A1: G is connected;
let A, B be Subset of T such that
A2: [#]T = A \/ B & A,B are_separated;
reconsider A1 = A, B1 = B as Subset of G;
[#]G = A1 \/ B1 & A1,B1 are_separated by A2,Th6;
then A1 = {}G or B1 = {}G by A1;
hence thesis;
end;
registration
let T be connected TopSpace;
cluster the TopStruct of T -> connected;
coherence
proof
set G = the TopStruct of T;
let A, B be Subset of G such that
A1: [#]G = A \/ B & A,B are_separated;
reconsider A1 = A, B1 = B as Subset of T;
[#]T = A1 \/ B1 & A1,B1 are_separated by A1,Th6;
then A1 = {}T or B1 = {}T by CONNSP_1:def 2;
hence thesis;
end;
end;
theorem
for S, T be non empty TopSpace st S,T are_homeomorphic &
S is pathwise_connected holds T is pathwise_connected
proof
let S, T be non empty TopSpace;
given h being Function of S,T such that
A1: h is being_homeomorphism;
assume
A2: for a, b being Point of S holds a,b are_connected;
let a, b being Point of T;
h".a,h".b are_connected by A2;
then consider f being Function of I[01], S such that
A3: f is continuous and
A4: f.0 = h".a and
A5: f.1 = h".b;
take g = h*f;
h is continuous by A1;
hence g is continuous by A3;
A6: h is one-to-one & rng h = [#]T by A1;
thus g.0 = h.(h".a) by A4,BORSUK_1:def 14,FUNCT_2:15
.= (h*h").a by FUNCT_2:15
.= (id T).a by A6,TOPS_2:52
.= a;
thus g.1 = h.(h".b) by A5,BORSUK_1:def 15,FUNCT_2:15
.= (h*h").b by FUNCT_2:15
.= (id T).b by A6,TOPS_2:52
.= b;
end;
registration
cluster trivial -> pathwise_connected for non empty TopSpace;
coherence
proof
let T be non empty TopSpace;
assume
A1: T is trivial;
let a, b be Point of T;
take f = I[01] --> a;
thus f is continuous;
a = b by A1;
hence thesis by BORSUK_1:def 14,def 15;
end;
end;
theorem
for T being SubSpace of TOP-REAL 2 st the carrier of T is
Simple_closed_curve holds T is pathwise_connected
proof
let T be SubSpace of TOP-REAL 2;
assume
A1: the carrier of T is Simple_closed_curve;
then reconsider P = the carrier of T as Simple_closed_curve;
let a, b be Point of T;
a in P & b in P;
then reconsider p1 = a, p2 = b as Point of TOP-REAL 2;
per cases;
suppose
p1 <> p2;
then consider P1, P2 being non empty Subset of TOP-REAL 2 such that
A2: P1 is_an_arc_of p1,p2 and
P2 is_an_arc_of p1,p2 and
A3: P = P1 \/ P2 and
P1 /\ P2 = {p1,p2} by TOPREAL2:5;
the carrier of ((TOP-REAL 2)|P1) = P1 by PRE_TOPC:8;
then
A4: the carrier of ((TOP-REAL 2)|P1) c= P by A3,XBOOLE_1:7;
then
A5: (TOP-REAL 2)|P1 is SubSpace of T by TSEP_1:4;
consider f1 being Function of I[01], (TOP-REAL 2)|P1 such that
A6: f1 is being_homeomorphism and
A7: f1.0 = p1 & f1.1 = p2 by A2,TOPREAL1:def 1;
reconsider f = f1 as Function of I[01],T by A4,FUNCT_2:7;
take f;
f1 is continuous by A6;
hence f is continuous by A5,PRE_TOPC:26;
thus thesis by A7;
end;
suppose
A8: p1 = p2;
reconsider T1 = T as non empty SubSpace of TOP-REAL 2 by A1;
reconsider a1 = a as Point of T1;
reconsider f = I[01] --> a1 as Function of I[01],T;
take f;
thus f is continuous;
thus f.0 = f.j0 .= a;
thus f.1 = f.j1 .= b by A8;
end;
end;
theorem
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
proof
let T be TopSpace;
set F = {the carrier of T};
F c= bool the carrier of T
proof
let a be object;
assume a in F;
then a = the carrier of T by TARSKI:def 1;
hence thesis by ZFMISC_1:def 1;
end;
then reconsider F as Subset-Family of T;
take F;
thus F = {the carrier of T};
the carrier of T c= union F by ZFMISC_1:25;
hence F is Cover of T by SETFAM_1:def 11;
let P be Subset of T;
[#]T = the carrier of T;
hence thesis by TARSKI:def 1;
end;
registration
let T be TopSpace;
cluster non empty mutually-disjoint open closed for Subset-Family of T;
existence
proof
set F = {{}T};
F c= bool the carrier of T
proof
let a be object;
assume a in F;
then a = {}T by TARSKI:def 1;
hence thesis;
end;
then reconsider F as Subset-Family of T;
take F;
thus F is non empty mutually-disjoint by TAXONOM2:10;
thus F is open
by TARSKI:def 1;
let P be Subset of T;
thus thesis by TARSKI:def 1;
end;
end;
theorem
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
proof
let T be TopSpace;
let D be mutually-disjoint open Subset-Family of T;
let A be Subset of T;
let X be set such that
A1: T|A is connected and
A2: X in D and
A3: X meets A;
consider x being object such that
A4: x in X & x in A by A3,XBOOLE_0:3;
assume D is Cover of A;
then
A5: A c= union D by SETFAM_1:def 11;
let a be object;
assume
A6: a in A;
then consider Z being set such that
A7: a in Z and
A8: Z in D by A5,TARSKI:def 4;
set D2 = {K /\ A where K is Subset of T: K in D & not a in K};
D2 c= bool A
proof
let d be object;
reconsider dd=d as set by TARSKI:1;
assume d in D2;
then ex K1 being Subset of T st d = K1 /\ A & K1 in D & not a in K1;
then dd c= A by XBOOLE_1:17;
hence thesis;
end;
then reconsider D2 as Subset-Family of T|A by PRE_TOPC:8;
assume not a in X;
then
A9: X /\ A in D2 by A2;
x in X /\ A by A4,XBOOLE_0:def 4;
then
A10: x in union D2 by A9,TARSKI:def 4;
set D1 = {K /\ A where K is Subset of T: K in D & a in K};
D1 c= bool A
proof
let d be object;
reconsider dd=d as set by TARSKI:1;
assume d in D1;
then ex K1 being Subset of T st d = K1 /\ A & K1 in D & a in K1;
then dd c= A by XBOOLE_1:17;
hence thesis;
end;
then reconsider D1 as Subset-Family of T|A by PRE_TOPC:8;
A11: A c= union D1 \/ union D2
proof
let b be object;
assume
A12: b in A;
then consider Z being set such that
A13: b in Z and
A14: Z in D by A5,TARSKI:def 4;
reconsider Z as Subset of T by A14;
A15: b in Z /\ A by A12,A13,XBOOLE_0:def 4;
per cases;
suppose
a in Z;
then Z /\ A in D1 by A14;
then b in union D1 by A15,TARSKI:def 4;
hence thesis by XBOOLE_0:def 3;
end;
suppose
not a in Z;
then Z /\ A in D2 by A14;
then b in union D2 by A15,TARSKI:def 4;
hence thesis by XBOOLE_0:def 3;
end;
end;
A16: Z /\ A in D1 by A7,A8;
A17: [#](T|A) = A by PRE_TOPC:def 5;
D1 is open
proof
let P be Subset of T|A;
assume P in D1;
then consider K1 being Subset of T such that
A18: P = K1 /\ A and
A19: K1 in D and
a in K1;
K1 is open by A19,TOPS_2:def 1;
hence thesis by A17,A18,TOPS_2:24;
end;
then
A20: union D1 is open by TOPS_2:19;
D2 is open
proof
let P be Subset of T|A;
assume P in D2;
then consider K1 being Subset of T such that
A21: P = K1 /\ A and
A22: K1 in D and
not a in K1;
K1 is open by A22,TOPS_2:def 1;
hence thesis by A17,A21,TOPS_2:24;
end;
then
A23: union D2 is open by TOPS_2:19;
the carrier of T|A = A by PRE_TOPC:8;
then
A24: A = union D1 \/ union D2 by A11;
a in Z /\ A by A6,A7,XBOOLE_0:def 4;
then union D1 <> {}(T|A) by A16,TARSKI:def 4;
then union D1 meets union D2 by A1,A17,A20,A23,A24,A10,CONNSP_1:11;
then consider y being object such that
A25: y in union D1 and
A26: y in union D2 by XBOOLE_0:3;
consider Y2 being set such that
A27: y in Y2 and
A28: Y2 in D2 by A26,TARSKI:def 4;
consider K2 being Subset of T such that
A29: Y2 = K2 /\ A and
A30: K2 in D & not a in K2 by A28;
A31: y in K2 by A27,A29,XBOOLE_0:def 4;
consider Y1 being set such that
A32: y in Y1 and
A33: Y1 in D1 by A25,TARSKI:def 4;
consider K1 being Subset of T such that
A34: Y1 = K1 /\ A and
A35: K1 in D & a in K1 by A33;
y in K1 by A32,A34,XBOOLE_0:def 4;
then K1 meets K2 by A31,XBOOLE_0:3;
hence thesis by A35,A30,TAXONOM2:def 5;
end;
begin :: On the product of topologies
theorem Th13:
for S, T being TopSpace holds the TopStruct of [:S,T:] = [:the
TopStruct of S,the TopStruct of T:]
proof
let S, T be TopSpace;
A1: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by
BORSUK_1:def 2
.= the carrier of [:the TopStruct of S,the TopStruct of T:] by
BORSUK_1:def 2;
for C1 being Subset of [:S,T:], C2 being Subset of [:the TopStruct of S,
the TopStruct of T:] st C1 = C2 holds C1 is open iff C2 is open
proof
let C1 be Subset of [:S,T:];
let C2 be Subset of [:the TopStruct of S,the TopStruct of T:];
assume
A2: C1 = C2;
hereby
assume C1 is open;
then consider A being Subset-Family of [:S,T:] such that
A3: C1 = union A and
A4: for e being set st e in A ex X1 being Subset of S, Y1 being
Subset of T st e = [:X1,Y1:] & X1 is open & Y1 is open by BORSUK_1:5;
reconsider AA = A as Subset-Family of [:the TopStruct of S,the TopStruct
of T:] by A1;
for e being set st e in AA ex X1 being Subset of the TopStruct of S,
Y1 being Subset of the TopStruct of T st e = [:X1,Y1:] & X1 is open & Y1 is
open
proof
let e be set;
assume e in AA;
then consider X1 being Subset of S, Y1 being Subset of T such that
A5: e = [:X1,Y1:] & X1 is open & Y1 is open by A4;
reconsider Y2 = Y1 as Subset of the TopStruct of T;
reconsider X2 = X1 as Subset of the TopStruct of S;
take X2, Y2;
thus thesis by A5,TOPS_3:76;
end;
hence C2 is open by A2,A3,BORSUK_1:5;
end;
assume C2 is open;
then consider
A being Subset-Family of [:the TopStruct of S,the TopStruct of T
:] such that
A6: C2 = union A and
A7: for e being set st e in A ex X1 being Subset of the TopStruct of
S, Y1 being Subset of the TopStruct of T st e = [:X1,Y1:] & X1 is open & Y1 is
open by BORSUK_1:5;
reconsider AA = A as Subset-Family of [:S,T:] by A1;
for e being set st e in AA ex X1 being Subset of S, Y1 being Subset
of T st e = [:X1,Y1:] & X1 is open & Y1 is open
proof
let e be set;
assume e in AA;
then consider
X1 being Subset of the TopStruct of S, Y1 being Subset of the
TopStruct of T such that
A8: e = [:X1,Y1:] & X1 is open & Y1 is open by A7;
reconsider Y2 = Y1 as Subset of T;
reconsider X2 = X1 as Subset of S;
take X2, Y2;
thus thesis by A8,TOPS_3:76;
end;
hence thesis by A2,A6,BORSUK_1:5;
end;
hence thesis by A1,TOPS_3:72;
end;
theorem Th14:
for S, T being TopSpace, A being Subset of S, B being Subset of
T holds Cl [:A,B:] = [:Cl A,Cl B:]
proof
let S, T be TopSpace, A be Subset of S, B be Subset of T;
hereby
let x be object;
assume
A1: x in Cl [:A,B:];
then reconsider S1 = S, T1 = T as non empty TopSpace;
reconsider p = x as Point of [:S1,T1:] by A1;
consider K being Basis of p such that
A2: for Q being Subset of [:S1,T1:] st Q in K holds [:A,B:] meets Q by A1,
YELLOW13:17;
consider p1 being Point of S1, p2 being Point of T1 such that
A3: p = [p1,p2] by BORSUK_1:10;
for G being Subset of T1 st G is open & p2 in G holds B meets G
proof
let G be Subset of T1;
assume G is open & p2 in G;
then [p1,p2] in [:[#]S1,G:] & [:[#]S1,G:] is open by BORSUK_1:6
,ZFMISC_1:87;
then consider V being Subset of [:S1,T1:] such that
A4: V in K and
A5: V c= [:[#]S1,G:] by A3,YELLOW_8:def 1;
[:A,B:] meets V by A2,A4;
then consider a being object such that
A6: a in [:A,B:] & a in V by XBOOLE_0:3;
a in [:A,B:] /\ [:[#]S1,G:] by A5,A6,XBOOLE_0:def 4;
then a in [:A/\[#]S1,B/\G:] by ZFMISC_1:100;
then
ex a1, a2 being object st a1 in A/\[#]S1 & a2 in B/\G & a = [a1,a2] by
ZFMISC_1:def 2;
hence thesis;
end;
then
A7: p2 in Cl B by PRE_TOPC:def 7;
for G being Subset of S1 st G is open & p1 in G holds A meets G
proof
let G be Subset of S1;
assume G is open & p1 in G;
then [p1,p2] in [:G,[#]T1:] & [:G,[#]T1:] is open by BORSUK_1:6
,ZFMISC_1:87;
then consider V being Subset of [:S1,T1:] such that
A8: V in K and
A9: V c= [:G,[#]T1:] by A3,YELLOW_8:def 1;
[:A,B:] meets V by A2,A8;
then consider a being object such that
A10: a in [:A,B:] & a in V by XBOOLE_0:3;
a in [:A,B:] /\ [:G,[#]T1:] by A9,A10,XBOOLE_0:def 4;
then a in [:A/\G,B/\[#]T1:] by ZFMISC_1:100;
then
ex a1, a2 being object st a1 in A/\G & a2 in B/\[#]T1 & a = [a1,a2] by
ZFMISC_1:def 2;
hence thesis;
end;
then p1 in Cl A by PRE_TOPC:def 7;
hence x in [:Cl A,Cl B:] by A3,A7,ZFMISC_1:87;
end;
let x be object;
assume x in [:Cl A,Cl B:];
then consider x1, x2 being object such that
A11: x1 in Cl A and
A12: x2 in Cl B and
A13: x = [x1,x2] by ZFMISC_1:def 2;
reconsider S1 = S, T1 = T as non empty TopSpace by A11,A12;
reconsider x1 as Point of S1 by A11;
consider K1 being Basis of x1 such that
A14: for Q being Subset of S1 st Q in K1 holds A meets Q by A11,YELLOW13:17;
reconsider x2 as Point of T1 by A12;
consider K2 being Basis of x2 such that
A15: for Q being Subset of T1 st Q in K2 holds B meets Q by A12,YELLOW13:17;
for G being Subset of [:S1,T1:] st G is open & [x1,x2] in G holds [:A,B
:] meets G
proof
let G be Subset of [:S1,T1:] such that
A16: G is open and
A17: [x1,x2] in G;
consider F being Subset-Family of [:S1,T1:] such that
A18: G = union F and
A19: for e being set st e in F ex X1 being Subset of S1, Y1 being
Subset of T1 st e = [:X1,Y1:] & X1 is open & Y1 is open by A16,BORSUK_1:5;
consider Z being set such that
A20: [x1,x2] in Z and
A21: Z in F by A17,A18,TARSKI:def 4;
consider X1 being Subset of S1, Y1 being Subset of T1 such that
A22: Z = [:X1,Y1:] and
A23: X1 is open and
A24: Y1 is open by A19,A21;
x2 in Y1 by A20,A22,ZFMISC_1:87;
then consider V2 being Subset of T1 such that
A25: V2 in K2 and
A26: V2 c= Y1 by A24,YELLOW_8:def 1;
B meets V2 by A15,A25;
then consider a2 being object such that
A27: a2 in B and
A28: a2 in V2 by XBOOLE_0:3;
x1 in X1 by A20,A22,ZFMISC_1:87;
then consider V1 being Subset of S1 such that
A29: V1 in K1 and
A30: V1 c= X1 by A23,YELLOW_8:def 1;
A meets V1 by A14,A29;
then consider a1 being object such that
A31: a1 in A and
A32: a1 in V1 by XBOOLE_0:3;
[a1,a2] in Z by A22,A30,A32,A26,A28,ZFMISC_1:87;
then
A33: [a1,a2] in union F by A21,TARSKI:def 4;
[a1,a2] in [:A,B:] by A31,A27,ZFMISC_1:87;
hence thesis by A18,A33,XBOOLE_0:3;
end;
hence thesis by A13,PRE_TOPC:def 7;
end;
theorem Th15:
for S, T being TopSpace, A being closed Subset of S, B being
closed Subset of T holds [:A,B:] is closed
proof
let S, T be TopSpace;
let A be closed Subset of S;
let B be closed Subset of T;
Cl A = A & Cl [:A,B:] = [:Cl A,Cl B:] by Th14,PRE_TOPC:22;
hence thesis by PRE_TOPC:22;
end;
registration
let A, B be connected TopSpace;
cluster [:A,B:] -> connected;
coherence
proof
set S = the TopStruct of A, T = the TopStruct of B;
A1: the TopStruct of [:A,B:] = [:S,T:] by Th13;
per cases;
suppose
A2: [:S,T:] is non empty;
now
set J = 1TopSp{0,1};
given f being Function of [:S,T:], J such that
A3: f is continuous and
A4: f is onto;
A5: the carrier of J = {0,1} by PCOMPS_1:5;
then reconsider j0 = 0, j1 = 1 as Element of J by TARSKI:def 2;
A6: rng f = the carrier of J by A4;
then consider xy0 being object such that
A7: xy0 in dom f and
A8: f.xy0 = j0 by FUNCT_1:def 3;
consider xy1 being object such that
A9: xy1 in dom f and
A10: f.xy1 = j1 by A6,FUNCT_1:def 3;
A11: the carrier of [:S,T:] = [:the carrier of S, the carrier of T:] by
BORSUK_1:def 2;
then consider x0, y0 being object such that
A12: x0 in the carrier of S and
A13: y0 in the carrier of T and
A14: xy0 = [x0,y0] by A7,ZFMISC_1:def 2;
A15: dom f = the carrier of [:S,T:] by FUNCT_2:def 1;
consider x1, y1 being object such that
A16: x1 in the carrier of S and
A17: y1 in the carrier of T and
A18: xy1 = [x1,y1] by A11,A9,ZFMISC_1:def 2;
reconsider y0, y1 as Point of T by A13,A17;
reconsider x0, x1 as Point of S by A12,A16;
reconsider S, T as non empty TopSpace by A2;
reconsider Y1 = {y1} as non empty Subset of T by ZFMISC_1:31;
set h = f | [:[#]S,Y1:];
A19: dom h = [:[#]S,Y1:] by A15,RELAT_1:62;
the carrier of [:S,T|Y1:] = [:the carrier of S,the carrier of T|
Y1:] by BORSUK_1:def 2;
then
A20: dom h = the carrier of [:S,T|Y1:] by A19,PRE_TOPC:8;
rng h c= the carrier of J;
then reconsider h as Function of [:S,T|Y1:],J by A20,FUNCT_2:2;
S, [:T|Y1,S:] are_homeomorphic by BORSUK_3:13;
then [:T|Y1,S:] is connected by TOPREAL6:19;
then
A21: [:S,T|Y1:] is connected by TOPREAL6:19,YELLOW12:44;
[:S,T|Y1:] = [:S| [#]S,T|Y1:] by TSEP_1:3
.= [:S,T:] | [:[#]S,Y1:] by BORSUK_3:22;
then
A22: h is continuous by A3,TOPMETR:7;
A23: now
assume
A24: f. [x0,y1] <> 1;
h is onto
proof
thus rng h c= the carrier of J;
let y be object;
A25: y1 in Y1 by TARSKI:def 1;
assume
A26: y in the carrier of J;
per cases by A5,A26,TARSKI:def 2;
suppose
A27: y = 1;
A28: [x1,y1] in dom h by A19,A25,ZFMISC_1:87;
then h. [x1,y1] = y by A10,A18,A19,A27,FUNCT_1:49;
hence thesis by A28,FUNCT_1:def 3;
end;
suppose
A29: y = 0;
[x0,y1] in dom f by A15,A11,A12,A17,ZFMISC_1:87;
then
A30: f. [x0,y1] in rng f by FUNCT_1:def 3;
A31: [x0,y1] in dom h by A19,A25,ZFMISC_1:87;
then h. [x0,y1] = f. [x0,y1] by A19,FUNCT_1:49
.= y by A5,A24,A29,A30,TARSKI:def 2;
hence thesis by A31,FUNCT_1:def 3;
end;
end;
hence contradiction by A21,A22,Th7;
end;
reconsider X0 = {x0} as non empty Subset of S by ZFMISC_1:31;
set g = f | [:X0,[#]T:];
A32: dom g = [:X0,[#]T:] by A15,RELAT_1:62;
the carrier of [:S|X0,T:] = [:the carrier of S|X0,the carrier of
T:] by BORSUK_1:def 2;
then
A33: dom g = the carrier of [:S|X0,T:] by A32,PRE_TOPC:8;
rng g c= the carrier of J;
then reconsider g as Function of [:S|X0,T:],J by A33,FUNCT_2:2;
T, [:S|X0,T:] are_homeomorphic by BORSUK_3:13;
then
A34: [:S|X0,T:] is connected by TOPREAL6:19;
[:S|X0,T:] = [:S|X0,T| [#]T:] by TSEP_1:3
.= [:S,T:] | [:X0,[#]T:] by BORSUK_3:22;
then
A35: g is continuous by A3,TOPMETR:7;
now
assume
A36: f. [x0,y1] <> 0;
g is onto
proof
thus rng g c= the carrier of J;
let y be object;
A37: x0 in X0 by TARSKI:def 1;
assume
A38: y in the carrier of J;
per cases by A5,A38,TARSKI:def 2;
suppose
A39: y = 0;
A40: [x0,y0] in dom g by A32,A37,ZFMISC_1:87;
then g. [x0,y0] = y by A8,A14,A32,A39,FUNCT_1:49;
hence thesis by A40,FUNCT_1:def 3;
end;
suppose
A41: y = 1;
[x0,y1] in dom f by A15,A11,A12,A17,ZFMISC_1:87;
then
A42: f. [x0,y1] in rng f by FUNCT_1:def 3;
A43: [x0,y1] in dom g by A32,A37,ZFMISC_1:87;
then g. [x0,y1] = f. [x0,y1] by A32,FUNCT_1:49
.= y by A5,A36,A41,A42,TARSKI:def 2;
hence thesis by A43,FUNCT_1:def 3;
end;
end;
hence contradiction by A34,A35,Th7;
end;
hence contradiction by A23;
end;
hence thesis by A1,Th7;
end;
suppose
[:S,T:] is empty;
hence thesis by Th13;
end;
end;
end;
theorem
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
proof
let S, T be TopSpace;
let A be Subset of S;
let B be Subset of T;
assume S|A is connected & T|B is connected;
then reconsider SA = S|A, TB = T|B as connected TopSpace;
[:SA,TB:] is connected;
hence [:S,T:] | [:A,B:] is connected by BORSUK_3:22;
end;
theorem
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
proof
let S, T be TopSpace, Y be non empty TopSpace;
let A be Subset of S;
let f be Function of [:S,T:],Y;
let g be Function of [:S|A,T:],Y;
assume
A1: g = f | [:A,the carrier of T:] & f is continuous;
set TT = the TopStruct of T;
A2: [:S|A,TT:] = [:S|A,TT| [#]TT:] by TSEP_1:3
.= [:S,TT:]| [:A,[#]TT:] by BORSUK_3:22;
the TopStruct of [:S,T:] = [:the TopStruct of S,the TopStruct of T:] by Th13;
then
A3: the TopStruct of [:S,TT:] = the TopStruct of [:S,T:] by Th13;
the TopStruct of [:S|A,TT:] = the TopStruct of [:S|A,T:] by Th13;
hence thesis by A1,A3,A2,TOPMETR:7;
end;
theorem
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
proof
let S, T be TopSpace, Y be non empty TopSpace;
let A be Subset of T;
let f be Function of [:S,T:],Y;
let g be Function of [:S,T|A:],Y;
assume
A1: g = f | [:the carrier of S,A:] & f is continuous;
set SS = the TopStruct of S;
A2: [:SS,T|A:] = [:SS| [#]SS,T|A:] by TSEP_1:3
.= [:SS,T:]| [:[#]SS,A:] by BORSUK_3:22;
the TopStruct of [:S,T:] = [:the TopStruct of S,the TopStruct of T:] by Th13;
then
A3: the TopStruct of [:SS,T:] = the TopStruct of [:S,T:] by Th13;
the TopStruct of [:SS,T|A:] = the TopStruct of [:S,T|A:] by Th13;
hence thesis by A1,A3,A2,TOPMETR:7;
end;
theorem
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
proof
let S, T, T1, T2, Y be non empty TopSpace, f be Function of [:Y,T1:],S, g be
Function of [:Y,T2:],S, F1, F2 be closed Subset of T;
assume that
A1: T1 is SubSpace of T and
A2: T2 is SubSpace of T and
A3: F1 = [#]T1 and
A4: F2 = [#]T2 and
A5: ([#]T1) \/ ([#]T2) = [#]T and
A6: f is continuous and
A7: g is continuous and
A8: for p being set st p in ([#][:Y,T1:]) /\ ([#][:Y,T2:]) holds f.p = g .p;
A9: dom f = the carrier of [:Y,T1:] by FUNCT_2:def 1;
set h = f+*g;
A10: the carrier of [:Y,T2:] = [:the carrier of Y,the carrier of T2:] by
BORSUK_1:def 2;
A11: [:Y,T2:] is SubSpace of [:Y,T:] by A2,BORSUK_3:15;
A12: rng h c= rng f \/ rng g by FUNCT_4:17;
A13: dom g = the carrier of [:Y,T2:] by FUNCT_2:def 1;
A14: dom h = dom f \/ dom g by FUNCT_4:def 1;
A15: the carrier of [:Y,T1:] = [:the carrier of Y,the carrier of T1:] by
BORSUK_1:def 2;
then
A16: dom h = [:the carrier of Y,the carrier of T:] by A5,A10,A9,A13,A14,
ZFMISC_1:97;
A17: the carrier of [:Y,T:] = [:the carrier of Y,the carrier of T:] by
BORSUK_1:def 2;
then reconsider h as Function of [:Y,T:],S by A16,A12,FUNCT_2:2,XBOOLE_1:1;
take h;
thus h = f+*g;
A18: [:Y,T1:] is SubSpace of [:Y,T:] by A1,BORSUK_3:15;
for P being Subset of S st P is closed holds h"P is closed
proof
reconsider M = [:[#]Y,F1:] as Subset of [:Y,T:];
let P be Subset of S;
A19: now
let x be object;
thus x in h"P /\ [#][:Y,T2:] implies x in g"P
proof
assume
A20: x in h"P /\ [#][:Y,T2:];
then x in h"P by XBOOLE_0:def 4;
then
A21: h.x in P by FUNCT_1:def 7;
g.x = h.x by A13,A20,FUNCT_4:13;
hence thesis by A13,A20,A21,FUNCT_1:def 7;
end;
assume
A22: x in g"P;
then
A23: x in dom g by FUNCT_1:def 7;
g.x in P by A22,FUNCT_1:def 7;
then
A24: h.x in P by A23,FUNCT_4:13;
x in dom h by A14,A23,XBOOLE_0:def 3;
then x in h"P by A24,FUNCT_1:def 7;
hence x in h"P /\ [#][:Y,T2:] by A22,XBOOLE_0:def 4;
end;
A25: for x being set st x in [#][:Y,T1:] holds h.x = f.x
proof
let x be set such that
A26: x in [#][:Y,T1:];
now
per cases;
suppose
A27: x in [#][:Y,T2:];
then x in [#][:Y,T1:] /\ [#][:Y,T2:] by A26,XBOOLE_0:def 4;
then f.x = g.x by A8;
hence thesis by A13,A27,FUNCT_4:13;
end;
suppose
not x in [#][:Y,T2:];
hence thesis by A13,FUNCT_4:11;
end;
end;
hence thesis;
end;
now
let x be object;
thus x in h"P /\ [#][:Y,T1:] implies x in f"P
proof
assume
A28: x in h"P /\ [#][:Y,T1:];
then x in h"P by XBOOLE_0:def 4;
then
A29: h.x in P by FUNCT_1:def 7;
x in [#][:Y,T1:] by A28;
then
A30: x in dom f by FUNCT_2:def 1;
f.x = h.x by A25,A28;
hence thesis by A29,A30,FUNCT_1:def 7;
end;
assume
A31: x in f"P;
then x in dom f by FUNCT_1:def 7;
then
A32: x in dom h by A14,XBOOLE_0:def 3;
f.x in P by A31,FUNCT_1:def 7;
then h.x in P by A25,A31;
then x in h"P by A32,FUNCT_1:def 7;
hence x in h"P /\ [#][:Y,T1:] by A31,XBOOLE_0:def 4;
end;
then
A33: h"P /\ [#][:Y,T1:] = f"P by TARSKI:2;
the carrier of T2 is Subset of T by A2,TSEP_1:1;
then [#][:Y,T2:] c= [#][:Y,T:] by A17,A10,ZFMISC_1:95;
then reconsider P2 = g"P as Subset of [:Y,T:] by XBOOLE_1:1;
the carrier of T1 is Subset of T by A1,TSEP_1:1;
then [#][:Y,T1:] c= [#][:Y,T:] by A17,A15,ZFMISC_1:95;
then reconsider P1 = f"P as Subset of [:Y,T:] by XBOOLE_1:1;
assume
A34: P is closed;
then f"P is closed by A6,PRE_TOPC:def 6;
then
A35: ex F01 being Subset of [:Y,T:] st F01 is closed & f"P = F01 /\ [#][:Y,
T1:] by A18,PRE_TOPC:13;
h"P = h"P /\ ([#][:Y,T1:] \/ [#][:Y,T2:]) by A17,A9,A13,A14,A16,XBOOLE_1:28
.= (h"P /\ [#][:Y,T1:]) \/ (h"P /\ [#][:Y,T2:]) by XBOOLE_1:23;
then
A36: h"P = f"P \/ g"P by A33,A19,TARSKI:2;
M is closed & [#][:Y,T1:] = [:[#]Y,F1:] by A3,Th15,BORSUK_3:1;
then
A37: P1 is closed by A35;
g"P is closed by A7,A34,PRE_TOPC:def 6;
then
A38: ex F02 being Subset of [:Y,T:] st F02 is closed & g"P = F02 /\ [#][:Y,
T2:] by A11,PRE_TOPC:13;
reconsider M = [:[#]Y,F2:] as Subset of [:Y,T:];
M is closed & [#][:Y,T2:] = [:[#]Y,F2:] by A4,Th15,BORSUK_3:1;
then P2 is closed by A38;
hence thesis by A36,A37;
end;
hence thesis by PRE_TOPC:def 6;
end;
theorem
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
proof
let S, T, T1, T2, Y be non empty TopSpace, f be Function of [:T1,Y:],S, g be
Function of [:T2,Y:],S, F1, F2 be closed Subset of T;
assume that
A1: T1 is SubSpace of T and
A2: T2 is SubSpace of T and
A3: F1 = [#]T1 and
A4: F2 = [#]T2 and
A5: ([#]T1) \/ ([#]T2) = [#]T and
A6: f is continuous and
A7: g is continuous and
A8: for p being set st p in ([#][:T1,Y:]) /\ ([#][:T2,Y:]) holds f.p = g .p;
A9: dom f = the carrier of [:T1,Y:] by FUNCT_2:def 1;
A10: Y is SubSpace of Y by TSEP_1:2;
then
A11: [:T2,Y:] is SubSpace of [:T,Y:] by A2,BORSUK_3:21;
set h = f+*g;
A12: the carrier of [:T2,Y:] = [:the carrier of T2,the carrier of Y:] by
BORSUK_1:def 2;
A13: dom h = dom f \/ dom g by FUNCT_4:def 1;
A14: rng h c= rng f \/ rng g by FUNCT_4:17;
A15: dom g = the carrier of [:T2,Y:] by FUNCT_2:def 1;
A16: the carrier of [:T1,Y:] = [:the carrier of T1,the carrier of Y:] by
BORSUK_1:def 2;
then
A17: dom h = [:the carrier of T,the carrier of Y:] by A5,A12,A9,A15,A13,
ZFMISC_1:97;
A18: the carrier of [:T,Y:] = [:the carrier of T,the carrier of Y:] by
BORSUK_1:def 2;
then reconsider h as Function of [:T,Y:],S by A17,A14,FUNCT_2:2,XBOOLE_1:1;
take h;
thus h = f+*g;
A19: [:T1,Y:] is SubSpace of [:T,Y:] by A1,A10,BORSUK_3:21;
for P being Subset of S st P is closed holds h"P is closed
proof
reconsider M = [:F1,[#]Y:] as Subset of [:T,Y:];
let P be Subset of S;
A20: now
let x be object;
thus x in h"P /\ [#][:T2,Y:] implies x in g"P
proof
assume
A21: x in h"P /\ [#][:T2,Y:];
then x in h"P by XBOOLE_0:def 4;
then
A22: h.x in P by FUNCT_1:def 7;
g.x = h.x by A15,A21,FUNCT_4:13;
hence thesis by A15,A21,A22,FUNCT_1:def 7;
end;
assume
A23: x in g"P;
then
A24: x in dom g by FUNCT_1:def 7;
g.x in P by A23,FUNCT_1:def 7;
then
A25: h.x in P by A24,FUNCT_4:13;
x in dom h by A13,A24,XBOOLE_0:def 3;
then x in h"P by A25,FUNCT_1:def 7;
hence x in h"P /\ [#][:T2,Y:] by A23,XBOOLE_0:def 4;
end;
A26: for x being set st x in [#][:T1,Y:] holds h.x = f.x
proof
let x be set such that
A27: x in [#][:T1,Y:];
now
per cases;
suppose
A28: x in [#][:T2,Y:];
then x in [#][:T1,Y:] /\ [#][:T2,Y:] by A27,XBOOLE_0:def 4;
then f.x = g.x by A8;
hence thesis by A15,A28,FUNCT_4:13;
end;
suppose
not x in [#][:T2,Y:];
hence thesis by A15,FUNCT_4:11;
end;
end;
hence thesis;
end;
now
let x be object;
thus x in h"P /\ [#][:T1,Y:] implies x in f"P
proof
assume
A29: x in h"P /\ [#][:T1,Y:];
then x in h"P by XBOOLE_0:def 4;
then
A30: h.x in P by FUNCT_1:def 7;
x in [#][:T1,Y:] by A29;
then
A31: x in dom f by FUNCT_2:def 1;
f.x = h.x by A26,A29;
hence thesis by A30,A31,FUNCT_1:def 7;
end;
assume
A32: x in f"P;
then x in dom f by FUNCT_1:def 7;
then
A33: x in dom h by A13,XBOOLE_0:def 3;
f.x in P by A32,FUNCT_1:def 7;
then h.x in P by A26,A32;
then x in h"P by A33,FUNCT_1:def 7;
hence x in h"P /\ [#][:T1,Y:] by A32,XBOOLE_0:def 4;
end;
then
A34: h"P /\ [#][:T1,Y:] = f"P by TARSKI:2;
the carrier of T2 is Subset of T by A2,TSEP_1:1;
then [#][:T2,Y:] c= [#][:T,Y:] by A18,A12,ZFMISC_1:95;
then reconsider P2 = g"P as Subset of [:T,Y:] by XBOOLE_1:1;
the carrier of T1 is Subset of T by A1,TSEP_1:1;
then [#][:T1,Y:] c= [#][:T,Y:] by A18,A16,ZFMISC_1:95;
then reconsider P1 = f"P as Subset of [:T,Y:] by XBOOLE_1:1;
assume
A35: P is closed;
then f"P is closed by A6,PRE_TOPC:def 6;
then
A36: ex F01 being Subset of [:T,Y:] st F01 is closed & f"P = F01 /\ [#][:T1
,Y:] by A19,PRE_TOPC:13;
h"P = h"P /\ ([#][:T1,Y:] \/ [#][:T2,Y:]) by A18,A9,A15,A13,A17,XBOOLE_1:28
.= (h"P /\ [#][:T1,Y:]) \/ (h"P /\ [#][:T2,Y:]) by XBOOLE_1:23;
then
A37: h"P = f"P \/ g"P by A34,A20,TARSKI:2;
M is closed & [#][:T1,Y:] = [:F1,[#]Y:] by A3,Th15,BORSUK_3:1;
then
A38: P1 is closed by A36;
g"P is closed by A7,A35,PRE_TOPC:def 6;
then
A39: ex F02 being Subset of [:T,Y:] st F02 is closed & g"P = F02 /\ [#][:T2
,Y:] by A11,PRE_TOPC:13;
reconsider M = [:F2,[#]Y:] as Subset of [:T,Y:];
M is closed & [#][:T2,Y:] = [:F2,[#]Y:] by A4,Th15,BORSUK_3:1;
then P2 is closed by A39;
hence thesis by A37,A38;
end;
hence thesis by PRE_TOPC:def 6;
end;
begin :: On the fundamental groups
registration
let T be non empty TopSpace, t be Point of T;
cluster -> continuous for Loop of t;
coherence
proof
t,t are_connected;
hence thesis by BORSUK_2:def 2;
end;
end;
theorem
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
proof
let T be non empty TopSpace, t be Point of T, x be Point of I[01], P be
constant Loop of t;
P = I[01] --> t by BORSUK_2:5;
hence thesis;
end;
theorem Th22:
for T being non empty TopSpace, t being Point of T, P being Loop
of t holds P.0 = t & P.1 = t
proof
let T be non empty TopSpace, t be Point of T, P be Loop of t;
t,t are_connected;
hence thesis by BORSUK_2:def 2;
end;
theorem Th23:
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
proof
let S, T be non empty TopSpace;
let f be continuous Function of S,T;
let a, b be Point of S;
given g being Function of I[01], S such that
A1: g is continuous and
A2: g.0 = a and
A3: g.1 = b;
take h = f*g;
thus h is continuous by A1;
thus h.0 = f.(g.j0) by FUNCT_2:15
.= f.a by A2;
thus h.1 = f.(g.j1) by FUNCT_2:15
.= f.b by A3;
end;
theorem
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
proof
let S, T be non empty TopSpace;
let f be continuous Function of S,T;
let a, b be Point of S;
let P be Path of a,b;
assume
A1: a,b are_connected;
A2: (f*P).1 = f.(P.j1) by FUNCT_2:15
.= f.b by A1,BORSUK_2:def 2;
A3: (f*P).0 = f.(P.j0) by FUNCT_2:15
.= f.a by A1,BORSUK_2:def 2;
P is continuous & f.a,f.b are_connected by A1,Th23,BORSUK_2:def 2;
hence thesis by A3,A2,BORSUK_2:def 2;
end;
theorem Th25:
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
proof
let S be non empty pathwise_connected TopSpace;
let T be non empty TopSpace;
let f be continuous Function of S,T;
let a, b be Point of S;
let P be Path of a,b;
A1: a,b are_connected by BORSUK_2:def 3;
A2: (f*P).1 = f.(P.j1) by FUNCT_2:15
.= f.b by A1,BORSUK_2:def 2;
A3: (f*P).0 = f.(P.j0) by FUNCT_2:15
.= f.a by A1,BORSUK_2:def 2;
f.a,f.b are_connected by A1,Th23;
hence thesis by A3,A2,BORSUK_2:def 2;
end;
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; :: redefines * (FUNCT_1, synonym) → * (RELAT_1, synonym) → (#) (RELAT_1, definition)
coherence by Th25;
end;
theorem Th26:
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
proof
let S, T be non empty TopSpace;
let f be continuous Function of S,T;
let a be Point of S;
let P be Loop of a;
A1: f.a,f.a are_connected;
A2: (f*P).1 = f.(P.j1) by FUNCT_2:15
.= f.a by Th22;
(f*P).0 = f.(P.j0) by FUNCT_2:15
.= f.a by Th22;
hence thesis by A2,A1,BORSUK_2:def 2;
end;
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; :: redefines * (FUNCT_1, synonym) → * (RELAT_1, synonym) → (#) (RELAT_1, definition)
coherence by Th26;
end;
theorem Th27:
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
proof
let S, T be non empty TopSpace;
let f be continuous Function of S,T;
let a, b be Point of S;
let P, Q be Path of a,b;
let P1, Q1 be Path of f.a,f.b;
assume that
A1: P,Q are_homotopic and
A2: P1 = f*P and
A3: Q1 = f*Q;
set F = the Homotopy of P,Q;
take G = f*F;
F is continuous by A1,BORSUK_6:def 11;
hence G is continuous;
let s be Point of I[01];
thus G.(s,0) = f.(F.(s,j0)) by Lm1,BINOP_1:18
.= f.(P.s) by A1,BORSUK_6:def 11
.= P1.s by A2,FUNCT_2:15;
thus G.(s,1) = f.(F.(s,j1)) by Lm1,BINOP_1:18
.= f.(Q.s) by A1,BORSUK_6:def 11
.= Q1.s by A3,FUNCT_2:15;
thus G.(0,s) = f.(F.(j0,s)) by Lm1,BINOP_1:18
.= f.a by A1,BORSUK_6:def 11;
thus G.(1,s) = f.(F.(j1,s)) by Lm1,BINOP_1:18
.= f.b by A1,BORSUK_6:def 11;
end;
theorem
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
proof
let S, T be non empty TopSpace;
let f be continuous Function of S,T;
let a, b be Point of S;
let P, Q be Path of a,b;
let P1, Q1 be Path of f.a,f.b;
let F be Homotopy of P,Q;
assume that
A1: P,Q are_homotopic and
A2: P1 = f*P and
A3: Q1 = f*Q;
thus P1,Q1 are_homotopic by A1,A2,A3,Th27;
set G = f*F;
F is continuous by A1,BORSUK_6:def 11;
hence G is continuous;
let s be Point of I[01];
thus G.(s,0) = f.(F.(s,j0)) by Lm1,BINOP_1:18
.= f.(P.s) by A1,BORSUK_6:def 11
.= P1.s by A2,FUNCT_2:15;
thus G.(s,1) = f.(F.(s,j1)) by Lm1,BINOP_1:18
.= f.(Q.s) by A1,BORSUK_6:def 11
.= Q1.s by A3,FUNCT_2:15;
thus G.(0,s) = f.(F.(j0,s)) by Lm1,BINOP_1:18
.= f.a by A1,BORSUK_6:def 11;
thus G.(1,s) = f.(F.(j1,s)) by Lm1,BINOP_1:18
.= f.b by A1,BORSUK_6:def 11;
end;
theorem Th29:
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)
proof
let S, T be non empty TopSpace;
let f be continuous Function of S,T;
let a, b, c be Point of S;
let P be Path of a,b;
let Q be Path of b,c;
let P1 be Path of f.a,f.b;
let Q1 be Path of f.b,f.c;
assume that
A1: a,b are_connected & b,c are_connected and
A2: P1 = f*P and
A3: Q1 = f*Q;
for x being Point of I[01] holds (P1+Q1).x = (f*(P+Q)).x
proof
let x be Point of I[01];
A4: f.a,f.b are_connected & f.b,f.c are_connected by A1,Th23;
per cases;
suppose
A5: x <= 1/2;
then
A6: 2*x is Point of I[01] by BORSUK_6:3;
thus (P1+Q1).x = P1.(2*x) by A4,A5,BORSUK_2:def 5
.= f.(P.(2*x)) by A2,A6,FUNCT_2:15
.= f.((P+Q).x) by A1,A5,BORSUK_2:def 5
.= (f*(P+Q)).x by FUNCT_2:15;
end;
suppose
A7: x >= 1/2;
then
A8: 2*x-1 is Point of I[01] by BORSUK_6:4;
thus (P1+Q1).x = Q1.(2*x-1) by A4,A7,BORSUK_2:def 5
.= f.(Q.(2*x-1)) by A3,A8,FUNCT_2:15
.= f.((P+Q).x) by A1,A7,BORSUK_2:def 5
.= (f*(P+Q)).x by FUNCT_2:15;
end;
end;
hence thesis;
end;
definition
let S, T be non empty TopSpace, s be Point of S, f be Function of S,T such
that
A1: f is continuous;
set pT = pi_1(T,f.s);
set pS = pi_1(S,s);
func FundGrIso(f,s) -> Function of pi_1(S,s),pi_1(T,f.s) means
:Def1:
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);
existence
proof
defpred P[set,set] means ex ls being Loop of s st $1 = Class(EqRel(S,s),ls
) & $2 = Class(EqRel(T,f.s),f*ls);
A2: for x being Element of pS ex y being Element of pT st P[x,y]
proof
let x be Element of pS;
consider ls being Loop of s such that
A3: x = Class(EqRel(S,s),ls) by TOPALG_1:47;
reconsider lt = f*ls as Loop of f.s by A1,Th26;
reconsider y = Class(EqRel(T,f.s),lt) as Element of pT by TOPALG_1:47;
take y, ls;
thus thesis by A3;
end;
ex h being Function of pS,pT st for x being Element of pS holds P[x,h.
x] from FUNCT_2:sch 3(A2);
hence thesis;
end;
uniqueness
proof
let g, h be Function of pS,pT such that
A4: for x being Element of pS ex ls being Loop of s st x = Class(EqRel
(S,s),ls) & g.x = Class(EqRel(T,f.s),f*ls) and
A5: for x being Element of pS ex ls being Loop of s st x = Class(EqRel
(S,s),ls) & h.x = Class(EqRel(T,f.s),f*ls);
now
let x be Element of pS;
consider lsg being Loop of s such that
A6: x = Class(EqRel(S,s),lsg) and
A7: g.x = Class(EqRel(T,f.s),f*lsg) by A4;
consider lsh being Loop of s such that
A8: x = Class(EqRel(S,s),lsh) and
A9: h.x = Class(EqRel(T,f.s),f*lsh) by A5;
reconsider ltg = f*lsg, lth = f*lsh as Loop of f.s by A1,Th26;
lsg,lsh are_homotopic by A6,A8,TOPALG_1:46;
then ltg,lth are_homotopic by A1,Th27;
hence g.x = h.x by A7,A9,TOPALG_1:46;
end;
hence thesis;
end;
end;
theorem
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)
proof
let S, T be non empty TopSpace;
let s be Point of S;
let f be continuous Function of S,T;
let ls be Loop of s;
reconsider x = Class(EqRel(S,s),ls) as Element of pi_1(S,s) by TOPALG_1:47;
consider ls1 being Loop of s such that
A1: x = Class(EqRel(S,s),ls1) and
A2: FundGrIso(f,s).x = Class(EqRel(T,f.s),f*ls1) by Def1;
ls,ls1 are_homotopic by A1,TOPALG_1:46;
then f*ls,f*ls1 are_homotopic by Th27;
hence thesis by A2,TOPALG_1:46;
end;
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;
coherence
proof
set h = FundGrIso(f,s);
set pS = pi_1(S,s);
let a, b be Element of pS;
consider lsa being Loop of s such that
A1: a = Class(EqRel(S,s),lsa) and
A2: h.a = Class(EqRel(T,f.s),f*lsa) by Def1;
consider lsb being Loop of s such that
A3: b = Class(EqRel(S,s),lsb) and
A4: h.b = Class(EqRel(T,f.s),f*lsb) by Def1;
A5: f*lsa+f*lsb = f*(lsa+lsb) by Th29;
consider lsab being Loop of s such that
A6: a*b = Class(EqRel(S,s),lsab) and
A7: h.(a*b) = Class(EqRel(T,f.s),f*lsab) by Def1;
a*b = Class(EqRel(S,s),lsa+lsb) by A1,A3,TOPALG_1:61;
then lsab,lsa+lsb are_homotopic by A6,TOPALG_1:46;
then f*lsab,f*lsa+f*lsb are_homotopic by A5,Th27;
hence h.(a * b) = Class(EqRel(T,f.s),f*lsa+f*lsb) by A7,TOPALG_1:46
.= h.a * h.b by A2,A4,TOPALG_1:61;
end;
end;
theorem Th31:
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
proof
let S, T be non empty TopSpace;
let s be Point of S;
set pS = pi_1(S,s);
let f be continuous Function of S,T such that
A1: f is being_homeomorphism;
A2: f is one-to-one by A1;
then
A3: f qua Function".(f.s) = s by FUNCT_2:26;
set h = FundGrIso(f,s);
set pT = pi_1(T,f.s);
A4: f" is continuous by A1;
A5: rng f = [#]T by A1;
then f is onto;
then
A6: f qua Function" = f" by A2,TOPS_2:def 4;
A7: dom h = the carrier of pS by FUNCT_2:def 1;
A8: rng h = the carrier of pT
proof
thus rng h c= the carrier of pT;
let y be object;
assume y in the carrier of pT;
then consider lt being Loop of f.s such that
A9: y = Class(EqRel(T,f.s),lt) by TOPALG_1:47;
reconsider ls = f"*lt as Loop of s by A4,A3,A6,Th26;
set x = Class(EqRel(S,s),ls);
A10: x in the carrier of pS by TOPALG_1:47;
then consider ls1 being Loop of s such that
A11: x = Class(EqRel(S,s),ls1) and
A12: h.x = Class(EqRel(T,f.s),f*ls1) by Def1;
A13: f*ls = (f*f")*lt by RELAT_1:36
.= id rng f * lt by A5,A2,TOPS_2:52
.= lt by A5,FUNCT_2:17;
ls,ls1 are_homotopic by A11,TOPALG_1:46;
then lt,f*ls1 are_homotopic by A13,Th27;
then h.x = y by A9,A12,TOPALG_1:46;
hence thesis by A7,A10,FUNCT_1:def 3;
end;
h is one-to-one
proof
let x1, x2 be object;
assume x1 in dom h;
then consider ls1 being Loop of s such that
A14: x1 = Class(EqRel(S,s),ls1) and
A15: h.x1 = Class(EqRel(T,f.s),f*ls1) by Def1;
assume x2 in dom h;
then consider ls2 being Loop of s such that
A16: x2 = Class(EqRel(S,s),ls2) and
A17: h.x2 = Class(EqRel(T,f.s),f*ls2) by Def1;
reconsider a1 = f"*(f*ls1), a2 = f"*(f*ls2) as Loop of s by A4,A3,A6,Th26;
assume h.x1 = h.x2;
then f*ls1,f*ls2 are_homotopic by A15,A17,TOPALG_1:46;
then
A18: a1,a2 are_homotopic by A4,A3,A6,Th27;
A19: f"*f = id dom f by A5,A2,TOPS_2:52;
A20: f"*(f*ls1) = (f"*f)*ls1 by RELAT_1:36
.= ls1 by A19,FUNCT_2:17;
f"*(f*ls2) = (f"*f)*ls2 by RELAT_1:36
.= ls2 by A19,FUNCT_2:17;
hence thesis by A14,A16,A20,A18,TOPALG_1:46;
end;
hence thesis by A8,GROUP_6:60;
end;
theorem
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
proof
let S, T be non empty TopSpace;
let s be Point of S;
let t be Point of T;
let f be continuous Function of S,T;
let P be Path of t,f.s;
let h be Homomorphism of pi_1(S,s),pi_1(T,t);
assume f is being_homeomorphism;
then
A1: FundGrIso(f,s) is bijective by Th31;
assume that
A2: f.s,t are_connected and
A3: h = pi_1-iso(P) * FundGrIso(f,s);
reconsider G = pi_1-iso(P) as Homomorphism of pi_1(T,f.s),pi_1(T,t) by A2,
TOPALG_1:50;
G is bijective by A2,TOPALG_1:55;
hence thesis by A1,A3,GROUP_6:64;
end;
theorem
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
proof
let S be non empty TopSpace;
let T be non empty pathwise_connected TopSpace;
let s be Point of S;
let t be Point of T;
given f being Function of S,T such that
A1: f is being_homeomorphism;
reconsider f as continuous Function of S,T by A1;
take pi_1-iso(the Path of t,f.s) * FundGrIso(f,s);
FundGrIso(f,s) is bijective by A1,Th31;
hence thesis by GROUP_6:64;
end;