:: On the Fundamental Groups of Products of Topological Spaces
:: by Artur Korni{\l}owicz
::
:: Received August 20, 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 XBOOLE_0, ALGSTR_0, SUBSET_1, CARD_3, FINSEQ_1, STRUCT_0,
RLVECT_2, FUNCT_1, RELAT_1, GROUP_1, GROUP_6, FUNCT_2, TARSKI, WELLORD1,
BORSUK_1, CARD_1, PRE_TOPC, GRAPH_1, BORSUK_6, MCART_1, PARTFUN1,
ZFMISC_1, ORDINAL2, RCOMP_1, BORSUK_2, ALGSTR_1, ARYTM_3, XXREAL_0,
ARYTM_1, TOPALG_1, EQREL_1, WAYBEL20, TOPALG_4, MSSUBFAM;
notations TARSKI, XBOOLE_0, ZFMISC_1, EQREL_1, XTUPLE_0, MCART_1, ORDINAL1,
NUMBERS, XCMPLX_0, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2,
FUNCT_3, BINOP_1, FINSEQ_1, CARD_3, STRUCT_0, ALGSTR_0, PRALG_1, GROUP_1,
GROUP_6, GROUP_7, PRE_TOPC, BORSUK_1, BORSUK_2, BORSUK_6, TOPALG_1,
XXREAL_0;
constructors REAL_1, MONOID_0, PRALG_1, GROUP_7, BORSUK_3, BORSUK_6, TOPALG_1,
GROUP_6, XTUPLE_0, BINOP_1;
registrations RELSET_1, XREAL_0, FINSEQ_1, STRUCT_0, TOPS_1, BORSUK_1,
MONOID_0, BORSUK_2, GROUP_7, TOPALG_1, PRE_TOPC, RELAT_1, MEMBERED,
TOPMETR, XTUPLE_0;
requirements NUMERALS, BOOLE, SUBSET;
definitions TARSKI, XBOOLE_0, FUNCT_1, FUNCT_2, BORSUK_2, BORSUK_6, GROUP_6;
equalities XBOOLE_0, BINOP_1, STRUCT_0, TOPALG_1;
expansions FUNCT_1, FUNCT_2, BORSUK_2;
theorems BORSUK_1, BORSUK_2, FUNCT_2, TOPALG_3, MCART_1, FUNCT_1, ZFMISC_1,
JGRAPH_2, TOPALG_1, GROUP_7, CARD_3, FINSEQ_1, PRALG_1, TARSKI, BORSUK_6,
FUNCT_3, YELLOW12, GROUP_6, PARTFUN1;
schemes FUNCT_2;
begin :: On the product of groups
Lm1: 1 in {1,2} by TARSKI:def 2;
Lm2: 2 in {1,2} by TARSKI:def 2;
theorem Th1:
for G, H being non empty multMagma, x being Element of product <*
G,H*> ex g being Element of G, h being Element of H st x = <*g,h*>
proof
let G, H be non empty multMagma, x be Element of product <*G,H*>;
the carrier of product <*G,H*> = product Carrier <*G,H*> by GROUP_7:def 2;
then consider g being Function such that
A1: x = g and
A2: dom g = dom Carrier <*G,H*> and
A3: for y being object st y in dom Carrier <*G,H*> holds g.y in Carrier <*G
,H*>.y by CARD_3:def 5;
A4: ex R being 1-sorted st R = <*G,H*>.2 & Carrier <*G,H*>.2 = the carrier
of R by Lm2,PRALG_1:def 15;
A5: dom Carrier <*G,H*> = {1,2} by PARTFUN1:def 2;
then reconsider g as FinSequence by A2,FINSEQ_1:2,def 2;
g.2 in Carrier <*G,H*>.2 by A3,A5,Lm2;
then reconsider h1 = g.2 as Element of H by A4;
A6: ex R being 1-sorted st R = <*G,H*>.1 & Carrier <*G,H*>.1 = the carrier
of R by Lm1,PRALG_1:def 15;
g.1 in Carrier <*G,H*>.1 by A3,A5,Lm1;
then reconsider g1 = g.1 as Element of G by A6;
take g1, h1;
len g = 2 by A2,A5,FINSEQ_1:2,def 3;
hence thesis by A1,FINSEQ_1:44;
end;
definition
let G1, G2, H1, H2 be non empty multMagma, f be Function of G1,H1, g be
Function of G2,H2;
func Gr2Iso(f,g) -> Function of product <*G1,G2*>, product <*H1,H2*> means
:
Def1: for x being Element of product <*G1,G2*> ex x1 being Element of G1, x2
being Element of G2 st x = <*x1,x2*> & it.x = <*f.x1,g.x2*>;
existence
proof
defpred P[set,set] means ex x1 being Element of G1, x2 being Element of G2
st $1 = <*x1,x2*> & $2 = <*f.x1,g.x2*>;
A1: for x being Element of product <*G1,G2*> ex y being Element of product
<*H1,H2*> st P[x,y]
proof
let x be Element of product <*G1,G2*>;
consider a being Element of G1, h being Element of G2 such that
A2: x = <*a,h*> by Th1;
take <*f.a,g.h*>, a, h;
thus thesis by A2;
end;
ex h being Function of product <*G1,G2*>, product <*H1,H2*> st for x
being Element of product <*G1,G2*> holds P[x,h.x] from FUNCT_2:sch 3(A1);
hence thesis;
end;
uniqueness
proof
let F, G be Function of product <*G1,G2*>, product <*H1,H2*> such that
A3: for x being Element of product <*G1,G2*> ex x1 being Element of G1
, x2 being Element of G2 st x = <*x1,x2*> & F.x = <*f.x1,g.x2*> and
A4: for x being Element of product <*G1,G2*> ex x1 being Element of G1
, x2 being Element of G2 st x = <*x1,x2*> & G.x = <*f.x1,g.x2*>;
now
let x be Element of product <*G1,G2*>;
consider x1 being Element of G1, x2 being Element of G2 such that
A5: x = <*x1,x2*> and
A6: F.x = <*f.x1,g.x2*> by A3;
consider y1 being Element of G1, y2 being Element of G2 such that
A7: x = <*y1,y2*> and
A8: G.x = <*f.y1,g.y2*> by A4;
x1 = y1 by A5,A7,FINSEQ_1:77;
hence F.x = G.x by A5,A6,A7,A8,FINSEQ_1:77;
end;
hence thesis;
end;
end;
theorem
for G1, G2, H1, H2 being non empty multMagma, f being Function of G1,
H1, g being Function of G2,H2, x1 being Element of G1, x2 being Element of G2
holds Gr2Iso(f,g).<*x1,x2*> = <*f.x1,g.x2*>
proof
let G1, G2, H1, H2 be non empty multMagma, f be Function of G1,H1, g be
Function of G2,H2, x1 be Element of G1, x2 be Element of G2;
consider y1 being Element of G1, y2 being Element of G2 such that
A1: <*y1,y2*> = <*x1,x2*> and
A2: Gr2Iso(f,g).<*x1,x2*> = <*f.y1,g.y2*> by Def1;
x1 = y1 by A1,FINSEQ_1:77;
hence thesis by A1,A2,FINSEQ_1:77;
end;
registration
let G1, G2, H1, H2 be Group, f be Homomorphism of G1,H1,
g be Homomorphism of G2,H2;
cluster Gr2Iso(f,g) -> multiplicative;
coherence
proof
set h = Gr2Iso(f,g);
let a, b be Element of product <*G1,G2*>;
consider a1 being Element of G1, a2 being Element of G2 such that
A1: a = <*a1,a2*> and
A2: h.a = <*f.a1,g.a2*> by Def1;
consider b1 being Element of G1, b2 being Element of G2 such that
A3: b = <*b1,b2*> and
A4: h.b = <*f.b1,g.b2*> by Def1;
A5: b.2 = b2 by A3;
consider r1 being Element of G1, r2 being Element of G2 such that
A6: a*b = <*r1,r2*> and
A7: h.(a*b) = <*f.r1,g.r2*> by Def1;
G2 = <*G1,G2*>.2 & a.2 = a2 by A1;
then a2*b2 = <*r1,r2*>.2 by A6,A5,Lm2,GROUP_7:1;
then
A8: g.r2 = g.(a2*b2)
.= g.a2 * g.b2 by GROUP_6:def 6;
A9: b.1 = b1 by A3;
G1 = <*G1,G2*>.1 & a.1 = a1 by A1;
then a1*b1 = <*r1,r2*>.1 by A6,A9,Lm1,GROUP_7:1;
then f.r1 = f.(a1*b1)
.= f.a1 * f.b1 by GROUP_6:def 6;
hence h.(a*b) = h.a * h.b by A2,A4,A7,A8,GROUP_7:29;
end;
end;
theorem Th3:
for G1, G2, H1, H2 being non empty multMagma, f being Function of
G1,H1, g being Function of G2,H2 st f is one-to-one & g is one-to-one holds
Gr2Iso(f,g) is one-to-one
proof
let G1, G2, H1, H2 be non empty multMagma;
let f be Function of G1,H1, g be Function of G2,H2 such that
A1: f is one-to-one and
A2: g is one-to-one;
let a, b be object;
set h = Gr2Iso(f,g);
assume a in dom h;
then consider a1 being Element of G1, a2 being Element of G2 such that
A3: a = <*a1,a2*> and
A4: h.a = <*f.a1,g.a2*> by Def1;
assume b in dom h;
then consider b1 being Element of G1, b2 being Element of G2 such that
A5: b = <*b1,b2*> and
A6: h.b = <*f.b1,g.b2*> by Def1;
assume
A7: h.a = h.b;
then dom f = the carrier of G1 & f.a1 = f.b1 by A4,A6,FINSEQ_1:77
,FUNCT_2:def 1;
then
A8: a1 = b1 by A1;
dom g = the carrier of G2 & g.a2 = g.b2 by A4,A6,A7,FINSEQ_1:77,FUNCT_2:def 1
;
hence thesis by A2,A3,A5,A8;
end;
theorem Th4:
for G1, G2, H1, H2 being non empty multMagma, f being Function of
G1,H1, g being Function of G2,H2 st f is onto & g is onto holds Gr2Iso(f,g) is
onto
proof
let G1, G2, H1, H2 be non empty multMagma;
let f be Function of G1,H1, g be Function of G2,H2 such that
A1: rng f = the carrier of H1 and
A2: rng g = the carrier of H2;
set h = Gr2Iso(f,g);
thus rng h c= the carrier of product <*H1,H2*>;
let a be object;
assume a in the carrier of product <*H1,H2*>;
then consider x being Element of H1, y being Element of H2 such that
A3: a = <*x,y*> by Th1;
consider a2 being object such that
A4: a2 in dom g and
A5: g.a2 = y by A2,FUNCT_1:def 3;
consider a1 being object such that
A6: a1 in dom f and
A7: f.a1 = x by A1,FUNCT_1:def 3;
dom h = the carrier of product <*G1,G2*> & for g being Element of G1, h
being Element of G2 holds <*g,h*> in the carrier of product <*G1,G2*> by
FUNCT_2:def 1;
then
A8: <*a1,a2*> in dom h by A6,A4;
then consider k1 being Element of G1, k2 being Element of G2 such that
A9: <*a1,a2*> = <*k1,k2*> and
A10: h.<*a1,a2*> = <*f.k1,g.k2*> by Def1;
a1 = k1 & a2 = k2 by A9,FINSEQ_1:77;
hence thesis by A3,A7,A5,A8,A10,FUNCT_1:def 3;
end;
theorem Th5:
for G1, G2, H1, H2 being Group, f being Homomorphism of G1,H1,
g being Homomorphism of G2,H2 st f is bijective & g is bijective holds
Gr2Iso(f,g) is bijective
by Th4,Th3;
theorem Th6:
for G1, G2, H1, H2 being Group st G1,H1 are_isomorphic & G2,H2
are_isomorphic holds product <*G1,G2*>, product <*H1,H2*> are_isomorphic
proof
let G1, G2, H1, H2 be Group;
given h1 being Homomorphism of G1,H1 such that
A1: h1 is bijective;
given h2 being Homomorphism of G2,H2 such that
A2: h2 is bijective;
take Gr2Iso(h1,h2);
thus thesis by A1,A2,Th5;
end;
begin :: On the fundamental groups of products of topological spaces
set I = the carrier of I[01];
reconsider j0 = 0, j1 = 1 as Point of I[01] by BORSUK_1:def 14,def 15;
reserve S, T, Y for non empty TopSpace,
s, s1, s2, s3 for Point of S,
t, t1, t2, t3 for Point of T,
l1, l2 for Path of [s1,t1],[s2,t2],
H for Homotopy of l1 ,l2;
theorem Th7:
for f, g being Function st dom f = dom g holds pr1 <:f,g:> = f
proof
let f, g be Function such that
A1: dom f = dom g;
A2: dom pr1 <:f,g:> = dom <:f,g:> by MCART_1:def 12;
A3: for x being object st x in dom pr1 <:f,g:> holds pr1 <:f,g:>.x = f.x
proof
let x be object such that
A4: x in dom pr1 <:f,g:>;
thus pr1 <:f,g:>.x = (<:f,g:>.x)`1 by A2,A4,MCART_1:def 12
.= [f.x,g.x]`1 by A2,A4,FUNCT_3:def 7
.= f.x;
end;
dom <:f,g:> = dom f /\ dom g by FUNCT_3:def 7
.= dom f by A1;
hence thesis by A2,A3;
end;
theorem Th8:
for f, g being Function st dom f = dom g holds pr2 <:f,g:> = g
proof
let f, g be Function such that
A1: dom f = dom g;
A2: dom pr2 <:f,g:> = dom <:f,g:> by MCART_1:def 13;
A3: for x being object st x in dom pr2 <:f,g:> holds pr2 <:f,g:>.x = g.x
proof
let x be object such that
A4: x in dom pr2 <:f,g:>;
thus pr2 <:f,g:>.x = (<:f,g:>.x)`2 by A2,A4,MCART_1:def 13
.= [f.x,g.x]`2 by A2,A4,FUNCT_3:def 7
.= g.x;
end;
dom <:f,g:> = dom f /\ dom g by FUNCT_3:def 7
.= dom g by A1;
hence thesis by A2,A3;
end;
definition
let S, T, Y;
let f be Function of Y, S;
let g be Function of Y, T;
redefine func <:f,g:> -> Function of Y,[:S,T:]; :: redefines <: (FUNCT_3, definition)
coherence
proof
dom f = the carrier of Y & dom g = the carrier of Y by FUNCT_2:def 1;
then
A1: dom <:f,g:> = the carrier of Y by FUNCT_3:50;
the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by
BORSUK_1:def 2;
hence thesis by A1;
end;
end;
definition
let S, T, Y;
let f be Function of Y, [:S,T:];
redefine func pr1 f -> Function of Y,S; :: redefines pr1 (MCART_1, definition)
coherence
proof
A1: dom pr1 f = dom f by MCART_1:def 12;
A2: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by
BORSUK_1:def 2;
A3: rng pr1 f c= the carrier of S
proof
let y be object;
assume y in rng pr1 f;
then consider x being object such that
A4: x in dom pr1 f and
A5: (pr1 f).x = y by FUNCT_1:def 3;
(pr1 f).x = (f.x)`1 & f.x in rng f by A1,A4,FUNCT_1:def 3,MCART_1:def 12;
hence thesis by A2,A5,MCART_1:10;
end;
dom f = the carrier of Y by FUNCT_2:def 1;
hence thesis by A1,A3,FUNCT_2:2;
end;
redefine func pr2 f -> Function of Y,T; :: redefines pr2 (MCART_1, definition)
coherence
proof
A6: dom pr2 f = dom f by MCART_1:def 13;
A7: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by
BORSUK_1:def 2;
A8: rng pr2 f c= the carrier of T
proof
let y be object;
assume y in rng pr2 f;
then consider x being object such that
A9: x in dom pr2 f and
A10: (pr2 f).x = y by FUNCT_1:def 3;
(pr2 f).x = (f.x)`2 & f.x in rng f by A6,A9,FUNCT_1:def 3,MCART_1:def 13;
hence thesis by A7,A10,MCART_1:10;
end;
dom f = the carrier of Y by FUNCT_2:def 1;
hence thesis by A6,A8,FUNCT_2:2;
end;
end;
theorem Th9:
for f being continuous Function of Y,[:S,T:] holds pr1 f is continuous
proof
let f be continuous Function of Y,[:S,T:];
set g = pr1 f;
for p being Point of Y, V being Subset of S st g.p in V & V is open
holds ex W being Subset of Y st p in W & W is open & g.:W c= V
proof
let p be Point of Y, V be Subset of S such that
A1: g.p in V and
A2: V is open;
A3: [:V,[#]T:] is open by A2,BORSUK_1:6;
the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by
BORSUK_1:def 2;
then consider s, t being object such that
s in the carrier of S and
A4: t in the carrier of T and
A5: f.p = [s,t] by ZFMISC_1:def 2;
A6: dom f = the carrier of Y by FUNCT_2:def 1;
then g.p = [s,t]`1 by A5,MCART_1:def 12
.= s;
then f.p in [:V,[#]T:] by A1,A4,A5,ZFMISC_1:87;
then consider W being Subset of Y such that
A7: p in W & W is open and
A8: f.:W c= [:V,[#]T:] by A3,JGRAPH_2:10;
take W;
thus p in W & W is open by A7;
let y be object;
assume y in g.:W;
then consider x being Point of Y such that
A9: x in W and
A10: y = g.x by FUNCT_2:65;
A11: g.x = (f.x)`1 by A6,MCART_1:def 12;
f.x in f.:W by A6,A9,FUNCT_1:def 6;
hence thesis by A8,A10,A11,MCART_1:10;
end;
hence thesis by JGRAPH_2:10;
end;
theorem Th10:
for f being continuous Function of Y,[:S,T:] holds pr2 f is continuous
proof
let f be continuous Function of Y,[:S,T:];
set g = pr2 f;
for p being Point of Y, V being Subset of T st g.p in V & V is open
holds ex W being Subset of Y st p in W & W is open & g.:W c= V
proof
let p be Point of Y, V be Subset of T such that
A1: g.p in V and
A2: V is open;
A3: [:[#]S,V:] is open by A2,BORSUK_1:6;
the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by
BORSUK_1:def 2;
then consider s, t being object such that
A4: s in the carrier of S and
t in the carrier of T and
A5: f.p = [s,t] by ZFMISC_1:def 2;
A6: dom f = the carrier of Y by FUNCT_2:def 1;
then g.p = [s,t]`2 by A5,MCART_1:def 13
.= t;
then f.p in [:[#]S,V:] by A1,A4,A5,ZFMISC_1:87;
then consider W being Subset of Y such that
A7: p in W & W is open and
A8: f.:W c= [:[#]S,V:] by A3,JGRAPH_2:10;
take W;
thus p in W & W is open by A7;
let y be object;
assume y in g.:W;
then consider x being Point of Y such that
A9: x in W and
A10: y = g.x by FUNCT_2:65;
A11: g.x = (f.x)`2 by A6,MCART_1:def 13;
f.x in f.:W by A6,A9,FUNCT_1:def 6;
hence thesis by A8,A10,A11,MCART_1:10;
end;
hence thesis by JGRAPH_2:10;
end;
theorem Th11:
[s1,t1],[s2,t2] are_connected implies s1,s2 are_connected
proof
given L being Function of I[01], [:S,T:] such that
A1: L is continuous and
A2: L.0 = [s1,t1] and
A3: L.1 = [s2,t2];
take f = pr1 L;
thus f is continuous by A1,Th9;
A4: dom f = I & dom f = dom L by FUNCT_2:def 1,MCART_1:def 12;
then j0 in dom L;
hence f.0 = [s1,t1]`1 by A2,MCART_1:def 12
.= s1;
j1 in dom L by A4;
hence f.1 = [s2,t2]`1 by A3,MCART_1:def 12
.= s2;
end;
theorem Th12:
[s1,t1],[s2,t2] are_connected implies t1,t2 are_connected
proof
given L being Function of I[01], [:S,T:] such that
A1: L is continuous and
A2: L.0 = [s1,t1] and
A3: L.1 = [s2,t2];
take f = pr2 L;
thus f is continuous by A1,Th10;
A4: dom f = I & dom f = dom L by FUNCT_2:def 1,MCART_1:def 13;
then j0 in dom L;
hence f.0 = [s1,t1]`2 by A2,MCART_1:def 13
.= t1;
j1 in dom L by A4;
hence f.1 = [s2,t2]`2 by A3,MCART_1:def 13
.= t2;
end;
theorem Th13:
[s1,t1],[s2,t2] are_connected implies for L being Path of [s1,t1
],[s2,t2] holds pr1 L is Path of s1,s2
proof
assume
A1: [s1,t1], [s2,t2] are_connected;
let L be Path of [s1,t1],[s2,t2];
set f = pr1 L;
A2: dom f = I & dom f = dom L by FUNCT_2:def 1,MCART_1:def 12;
then j0 in dom L;
then
A3: f.0 = (L.0)`1 by MCART_1:def 12
.= [s1,t1]`1 by A1,BORSUK_2:def 2
.= s1;
j1 in dom L by A2;
then
A4: f.1 = (L.1)`1 by MCART_1:def 12
.= [s2,t2]`1 by A1,BORSUK_2:def 2
.= s2;
L is continuous by A1,BORSUK_2:def 2;
then
A5: f is continuous by Th9;
then s1,s2 are_connected by A3,A4;
hence thesis by A5,A3,A4,BORSUK_2:def 2;
end;
theorem Th14:
[s1,t1],[s2,t2] are_connected implies for L being Path of [s1,t1
],[s2,t2] holds pr2 L is Path of t1,t2
proof
assume
A1: [s1,t1], [s2,t2] are_connected;
let L be Path of [s1,t1],[s2,t2];
set f = pr2 L;
A2: dom f = I & dom f = dom L by FUNCT_2:def 1,MCART_1:def 13;
then j0 in dom L;
then
A3: f.0 = (L.0)`2 by MCART_1:def 13
.= [s1,t1]`2 by A1,BORSUK_2:def 2
.= t1;
j1 in dom L by A2;
then
A4: f.1 = (L.1)`2 by MCART_1:def 13
.= [s2,t2]`2 by A1,BORSUK_2:def 2
.= t2;
L is continuous by A1,BORSUK_2:def 2;
then
A5: f is continuous by Th10;
then t1,t2 are_connected by A3,A4;
hence thesis by A5,A3,A4,BORSUK_2:def 2;
end;
theorem Th15:
s1,s2 are_connected & t1,t2 are_connected implies [s1,t1],[s2,t2
] are_connected
proof
given f being Function of I[01], S such that
A1: f is continuous and
A2: f.0 = s1 and
A3: f.1 = s2;
given g being Function of I[01], T such that
A4: g is continuous and
A5: g.0 = t1 and
A6: g.1 = t2;
take <:f,g:>;
thus <:f,g:> is continuous by A1,A4,YELLOW12:41;
A7: dom f = I & dom g = I by FUNCT_2:def 1;
hence <:f,g:>.0 = [f.j0,g.j0] by FUNCT_3:49
.= [s1,t1] by A2,A5;
thus <:f,g:>.1 = [f.j1,g.j1] by A7,FUNCT_3:49
.= [s2,t2] by A3,A6;
end;
theorem Th16:
s1,s2 are_connected & t1,t2 are_connected implies for L1 being
Path of s1,s2, L2 being Path of t1,t2 holds <:L1,L2:> is Path of [s1,t1],[s2,t2
]
proof
assume that
A1: s1,s2 are_connected and
A2: t1,t2 are_connected;
let L1 be Path of s1,s2, L2 be Path of t1,t2;
L1 is continuous & L2 is continuous by A1,A2,BORSUK_2:def 2;
then
A3: <:L1,L2:> is continuous by YELLOW12:41;
A4: dom L1 = I & dom L2 = I by FUNCT_2:def 1;
then
A5: <:L1,L2:>.j1 = [L1.j1,L2.j1] by FUNCT_3:49
.= [s2,L2.j1] by A1,BORSUK_2:def 2
.= [s2,t2] by A2,BORSUK_2:def 2;
A6: <:L1,L2:>.j0 = [L1.j0,L2.j0] by A4,FUNCT_3:49
.= [s1,L2.j0] by A1,BORSUK_2:def 2
.= [s1,t1] by A2,BORSUK_2:def 2;
then [s1,t1], [s2,t2] are_connected by A3,A5;
hence thesis by A3,A6,A5,BORSUK_2:def 2;
end;
definition
let S, T be non empty pathwise_connected TopSpace, s1, s2 be Point of S, t1,
t2 be Point of T, L1 be Path of s1,s2, L2 be Path of t1,t2;
redefine func <:L1,L2:> -> Path of [s1,t1],[s2,t2]; :: redefines <: (FUNCT_3, definition)
coherence
proof
s1,s2 are_connected & t1,t2 are_connected by BORSUK_2:def 3;
hence thesis by Th16;
end;
end;
definition
let S, T be non empty TopSpace, s be Point of S, t be Point of T, L1 be Loop
of s, L2 be Loop of t;
redefine func <:L1,L2:> -> Loop of [s,t]; :: redefines <: (FUNCT_3, definition)
coherence by Th16;
end;
registration
let S, T be non empty pathwise_connected TopSpace;
cluster [:S,T:] -> pathwise_connected;
coherence
proof
let a, b be Point of [:S,T:];
consider a1 being Point of S, a2 being Point of T such that
A1: a = [a1,a2] by BORSUK_1:10;
consider b1 being Point of S, b2 being Point of T such that
A2: b = [b1,b2] by BORSUK_1:10;
a1,b1 are_connected & a2,b2 are_connected by BORSUK_2:def 3;
hence thesis by A1,A2,Th15;
end;
end;
definition
let S, T be non empty pathwise_connected TopSpace, s1, s2 be Point of S, t1,
t2 be Point of T, L be Path of [s1,t1],[s2,t2];
redefine func pr1 L -> Path of s1,s2; :: redefines pr1 (MCART_1, definition)
coherence
by BORSUK_2:def 3,Th13;
redefine func pr2 L -> Path of t1,t2; :: redefines pr2 (MCART_1, definition)
coherence
by BORSUK_2:def 3,Th14;
end;
definition
let S, T be non empty TopSpace, s be Point of S, t be Point of T, L be Loop
of [s,t];
redefine func pr1 L -> Loop of s; :: redefines pr1 (MCART_1, definition)
coherence by Th13;
redefine func pr2 L -> Loop of t; :: redefines pr2 (MCART_1, definition)
coherence by Th14;
end;
Lm3: l1,l2 are_homotopic implies pr1 H is continuous & for a being Point of
I[01] holds pr1 H.(a,0) = pr1 l1.a & pr1 H.(a,1) = pr1 l2.a & for b being Point
of I[01] holds pr1 H.(0,b) = s1 & pr1 H.(1,b) = s2
proof
A1: dom l1 = I by FUNCT_2:def 1;
A2: dom l2 = I by FUNCT_2:def 1;
assume
A3: l1,l2 are_homotopic;
then H is continuous by BORSUK_6:def 11;
hence pr1 H is continuous by Th9;
let a be Point of I[01];
A4: dom H = the carrier of [:I[01],I[01]:] by FUNCT_2:def 1;
hence pr1 H.(a,0) = (H. [a,j0])`1 by MCART_1:def 12
.= (H.(a,j0))`1
.= (l1.a)`1 by A3,BORSUK_6:def 11
.= pr1 l1.a by A1,MCART_1:def 12;
thus pr1 H.(a,1) = (H. [a,j1])`1 by A4,MCART_1:def 12
.= (H.(a,j1))`1
.= (l2.a)`1 by A3,BORSUK_6:def 11
.= pr1 l2.a by A2,MCART_1:def 12;
let b be Point of I[01];
thus pr1 H.(0,b) = (H. [j0,b])`1 by A4,MCART_1:def 12
.= (H.(j0,b))`1
.= [s1,t1]`1 by A3,BORSUK_6:def 11
.= s1;
thus pr1 H.(1,b) = (H. [j1,b])`1 by A4,MCART_1:def 12
.= (H.(j1,b))`1
.= [s2,t2]`1 by A3,BORSUK_6:def 11
.= s2;
end;
Lm4: l1,l2 are_homotopic implies pr2 H is continuous & for a being Point of
I[01] holds pr2 H.(a,0) = pr2 l1.a & pr2 H.(a,1) = pr2 l2.a & for b being Point
of I[01] holds pr2 H.(0,b) = t1 & pr2 H.(1,b) = t2
proof
A1: dom l1 = I by FUNCT_2:def 1;
A2: dom l2 = I by FUNCT_2:def 1;
assume
A3: l1,l2 are_homotopic;
then H is continuous by BORSUK_6:def 11;
hence pr2 H is continuous by Th10;
let a be Point of I[01];
A4: dom H = the carrier of [:I[01],I[01]:] by FUNCT_2:def 1;
hence pr2 H.(a,0) = (H. [a,j0])`2 by MCART_1:def 13
.= (H.(a,j0))`2
.= (l1.a)`2 by A3,BORSUK_6:def 11
.= pr2 l1.a by A1,MCART_1:def 13;
thus pr2 H.(a,1) = (H. [a,j1])`2 by A4,MCART_1:def 13
.= (H.(a,j1))`2
.= (l2.a)`2 by A3,BORSUK_6:def 11
.= pr2 l2.a by A2,MCART_1:def 13;
let b be Point of I[01];
thus pr2 H.(0,b) = (H. [j0,b])`2 by A4,MCART_1:def 13
.= (H.(j0,b))`2
.= [s1,t1]`2 by A3,BORSUK_6:def 11
.= t1;
thus pr2 H.(1,b) = (H. [j1,b])`2 by A4,MCART_1:def 13
.= (H.(j1,b))`2
.= [s2,t2]`2 by A3,BORSUK_6:def 11
.= t2;
end;
theorem
for p, q being Path of s1,s2 st p = pr1 l1 & q = pr1 l2 & l1,l2
are_homotopic holds pr1 H is Homotopy of p,q
proof
let p, q be Path of s1,s2 such that
A1: p = pr1 l1 & q = pr1 l2 & l1,l2 are_homotopic;
thus p,q are_homotopic
proof
take pr1 H;
thus thesis by A1,Lm3;
end;
thus thesis by A1,Lm3;
end;
theorem
for p, q being Path of t1,t2 st p = pr2 l1 & q = pr2 l2 & l1,l2
are_homotopic holds pr2 H is Homotopy of p,q
proof
let p, q be Path of t1,t2 such that
A1: p = pr2 l1 & q = pr2 l2 & l1,l2 are_homotopic;
thus p,q are_homotopic
proof
take pr2 H;
thus thesis by A1,Lm4;
end;
thus thesis by A1,Lm4;
end;
theorem Th19:
for p, q being Path of s1,s2 st p = pr1 l1 & q = pr1 l2 & l1,l2
are_homotopic holds p,q are_homotopic
proof
let p, q be Path of s1,s2 such that
A1: p = pr1 l1 & q = pr1 l2 and
A2: l1,l2 are_homotopic;
consider f being Function of [:I[01],I[01]:], [:S,T:] such that
A3: f is continuous & for a being Point of I[01] holds f.(a,0) = l1.a &
f.(a,1) = l2.a & for b being Point of I[01] holds f.(0,b) = [s1,t1] & f.(1,b) =
[s2,t2] by A2;
take pr1 f;
f is Homotopy of l1,l2 by A2,A3,BORSUK_6:def 11;
hence thesis by A1,A2,Lm3;
end;
theorem Th20:
for p, q being Path of t1,t2 st p = pr2 l1 & q = pr2 l2 & l1,l2
are_homotopic holds p,q are_homotopic
proof
let p, q be Path of t1,t2 such that
A1: p = pr2 l1 & q = pr2 l2 and
A2: l1,l2 are_homotopic;
consider f being Function of [:I[01],I[01]:], [:S,T:] such that
A3: f is continuous & for a being Point of I[01] holds f.(a,0) = l1.a &
f.(a,1) = l2.a & for b being Point of I[01] holds f.(0,b) = [s1,t1] & f.(1,b) =
[s2,t2] by A2;
take pr2 f;
f is Homotopy of l1,l2 by A2,A3,BORSUK_6:def 11;
hence thesis by A1,A2,Lm4;
end;
Lm5: for p, q being Path of s1,s2, x, y being Path of t1,t2, f being Homotopy
of p,q, g being Homotopy of x,y st p = pr1 l1 & q = pr1 l2 & x = pr2 l1 & y =
pr2 l2 & p,q are_homotopic & x,y are_homotopic holds <:f,g:> is continuous &
for a being Point of I[01] holds <:f,g:>.(a,0) = l1.a & <:f,g:>.(a,1) = l2.a &
for b being Point of I[01] holds <:f,g:>.(0,b) = [s1,t1] & <:f,g:>.(1,b) = [s2,
t2]
proof
let p, q be Path of s1,s2, x, y be Path of t1,t2, f be Homotopy of p,q, g be
Homotopy of x,y such that
A1: p = pr1 l1 and
A2: q = pr1 l2 and
A3: x = pr2 l1 and
A4: y = pr2 l2 and
A5: p,q are_homotopic and
A6: x,y are_homotopic;
set h = <:f,g:>;
f is continuous & g is continuous by A5,A6,BORSUK_6:def 11;
hence h is continuous by YELLOW12:41;
let a be Point of I[01];
A7: dom l1 = I by FUNCT_2:def 1;
A8: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by
BORSUK_1:def 2;
A9: dom f = the carrier of [:I[01],I[01]:] & dom g = the carrier of [:I[01],
I[01]:] by FUNCT_2:def 1;
hence h.(a,0) = [f. [a,j0], g. [a,j0]] by FUNCT_3:49
.= [f.(a,j0), g.(a,j0)]
.= [pr1 l1.a, g.(a,j0)] by A1,A5,BORSUK_6:def 11
.= [pr1 l1.a, pr2 l1.a] by A3,A6,BORSUK_6:def 11
.= [(l1.a)`1, pr2 l1.a] by A7,MCART_1:def 12
.= [(l1.a)`1, (l1.a)`2] by A7,MCART_1:def 13
.= l1.a by A8,MCART_1:21;
A10: dom l2 = I by FUNCT_2:def 1;
thus h.(a,1) = [f. [a,j1], g. [a,j1]] by A9,FUNCT_3:49
.= [f.(a,j1), g.(a,j1)]
.= [pr1 l2.a, g.(a,j1)] by A2,A5,BORSUK_6:def 11
.= [pr1 l2.a, pr2 l2.a] by A4,A6,BORSUK_6:def 11
.= [(l2.a)`1, pr2 l2.a] by A10,MCART_1:def 12
.= [(l2.a)`1, (l2.a)`2] by A10,MCART_1:def 13
.= l2.a by A8,MCART_1:21;
let b be Point of I[01];
thus h.(0,b) = [f. [j0,b], g. [j0,b]] by A9,FUNCT_3:49
.= [f.(j0,b), g.(j0,b)]
.= [s1, g.(j0,b)] by A5,BORSUK_6:def 11
.= [s1,t1] by A6,BORSUK_6:def 11;
thus h.(1,b) = [f. [j1,b], g. [j1,b]] by A9,FUNCT_3:49
.= [f.(j1,b), g.(j1,b)]
.= [s2, g.(j1,b)] by A5,BORSUK_6:def 11
.= [s2,t2] by A6,BORSUK_6:def 11;
end;
theorem
for p, q being Path of s1,s2, x, y being Path of t1,t2, f being
Homotopy of p,q, g being Homotopy of x,y st p = pr1 l1 & q = pr1 l2 & x = pr2
l1 & y = pr2 l2 & p,q are_homotopic & x,y are_homotopic holds <:f,g:> is
Homotopy of l1,l2
proof
let p, q be Path of s1,s2, x, y be Path of t1,t2, f be Homotopy of p,q, g be
Homotopy of x,y such that
A1: p = pr1 l1 & q = pr1 l2 & x = pr2 l1 & y = pr2 l2 & p,q
are_homotopic & x,y are_homotopic;
thus l1,l2 are_homotopic
proof
take <:f,g:>;
thus thesis by A1,Lm5;
end;
thus thesis by A1,Lm5;
end;
theorem Th22:
for p, q being Path of s1,s2, x, y being Path of t1, t2 st p =
pr1 l1 & q = pr1 l2 & x = pr2 l1 & y = pr2 l2 & p,q are_homotopic & x,y
are_homotopic holds l1, l2 are_homotopic
proof
let p, q be Path of s1,s2, x, y be Path of t1, t2 such that
A1: p = pr1 l1 & q = pr1 l2 and
A2: x = pr2 l1 & y = pr2 l2 and
A3: p,q are_homotopic and
A4: x,y are_homotopic;
consider g being Function of [:I[01],I[01]:], T such that
A5: g is continuous & for a being Point of I[01] holds g.(a,0) = pr2 l1.
a & g.(a,1) = pr2 l2.a & for b being Point of I[01] holds g.(0,b) = t1 & g.(1,
b) = t2 by A2,A4;
A6: g is Homotopy of x,y by A2,A4,A5,BORSUK_6:def 11;
consider f being Function of [:I[01],I[01]:], S such that
A7: f is continuous & for a being Point of I[01] holds f.(a,0) = pr1 l1.
a & f.(a,1) = pr1 l2.a & for b being Point of I[01] holds f.(0,b) = s1 & f.(1,
b) = s2 by A1,A3;
take <:f,g:>;
f is Homotopy of p,q by A1,A3,A7,BORSUK_6:def 11;
hence thesis by A1,A2,A3,A4,A6,Lm5;
end;
theorem Th23:
for l1 being Path of [s1,t1],[s2,t2], l2 being Path of [s2,t2],[
s3,t3], p1 being Path of s1,s2, p2 being Path of s2,s3 st [s1,t1],[s2,t2]
are_connected & [s2,t2],[s3,t3] are_connected & p1 = pr1 l1 & p2 = pr1 l2 holds
pr1 (l1+l2) = p1 + p2
proof
let l1 be Path of [s1,t1],[s2,t2], l2 be Path of [s2,t2],[s3,t3], p1 be Path
of s1,s2, p2 be Path of s2,s3 such that
A1: [s1,t1],[s2,t2] are_connected & [s2,t2],[s3,t3] are_connected and
A2: p1 = pr1 l1 and
A3: p2 = pr1 l2;
A4: s1,s2 are_connected & s2,s3 are_connected by A1,Th11;
now
A5: dom l2 = I by FUNCT_2:def 1;
A6: dom l1 = I by FUNCT_2:def 1;
let x be Element of I[01];
A7: dom (l1+l2) = I by FUNCT_2:def 1;
per cases;
suppose
A8: x <= 1/2;
then
A9: 2*x is Point of I[01] by BORSUK_6:3;
thus (pr1 (l1+l2)).x = ((l1+l2).x)`1 by A7,MCART_1:def 12
.= (l1.(2*x))`1 by A1,A8,BORSUK_2:def 5
.= p1.(2*x) by A2,A6,A9,MCART_1:def 12
.= (p1 + p2).x by A4,A8,BORSUK_2:def 5;
end;
suppose
A10: x >= 1/2;
then
A11: 2*x-1 is Point of I[01] by BORSUK_6:4;
thus (pr1 (l1+l2)).x = ((l1+l2).x)`1 by A7,MCART_1:def 12
.= (l2.(2*x-1))`1 by A1,A10,BORSUK_2:def 5
.= p2.(2*x-1) by A3,A5,A11,MCART_1:def 12
.= (p1 + p2).x by A4,A10,BORSUK_2:def 5;
end;
end;
hence thesis;
end;
theorem
for S, T being non empty pathwise_connected TopSpace, s1, s2, s3 being
Point of S, t1, t2, t3 being Point of T, l1 being Path of [s1,t1],[s2,t2], l2
being Path of [s2,t2],[s3,t3] holds pr1 (l1+l2) = (pr1 l1) + (pr1 l2)
proof
let S, T be non empty pathwise_connected TopSpace, s1, s2, s3 be Point of S,
t1, t2, t3 be Point of T, l1 be Path of [s1,t1],[s2,t2], l2 be Path of [s2,t2],
[s3,t3];
[s1,t1],[s2,t2] are_connected & [s2,t2],[s3,t3] are_connected by
BORSUK_2:def 3;
hence thesis by Th23;
end;
theorem Th25:
for l1 being Path of [s1,t1],[s2,t2], l2 being Path of [s2,t2],[
s3,t3], p1 being Path of t1,t2, p2 being Path of t2,t3 st [s1,t1],[s2,t2]
are_connected & [s2,t2],[s3,t3] are_connected & p1 = pr2 l1 & p2 = pr2 l2 holds
pr2 (l1+l2) = p1 + p2
proof
let l1 be Path of [s1,t1],[s2,t2], l2 be Path of [s2,t2],[s3,t3], p1 be Path
of t1,t2, p2 be Path of t2,t3 such that
A1: [s1,t1],[s2,t2] are_connected & [s2,t2],[s3,t3] are_connected and
A2: p1 = pr2 l1 and
A3: p2 = pr2 l2;
A4: t1,t2 are_connected & t2,t3 are_connected by A1,Th12;
now
A5: dom l2 = I by FUNCT_2:def 1;
A6: dom l1 = I by FUNCT_2:def 1;
let x be Element of I[01];
A7: dom (l1+l2) = I by FUNCT_2:def 1;
per cases;
suppose
A8: x <= 1/2;
then
A9: 2*x is Point of I[01] by BORSUK_6:3;
thus (pr2 (l1+l2)).x = ((l1+l2).x)`2 by A7,MCART_1:def 13
.= (l1.(2*x))`2 by A1,A8,BORSUK_2:def 5
.= p1.(2*x) by A2,A6,A9,MCART_1:def 13
.= (p1 + p2).x by A4,A8,BORSUK_2:def 5;
end;
suppose
A10: x >= 1/2;
then
A11: 2*x-1 is Point of I[01] by BORSUK_6:4;
thus (pr2 (l1+l2)).x = ((l1+l2).x)`2 by A7,MCART_1:def 13
.= (l2.(2*x-1))`2 by A1,A10,BORSUK_2:def 5
.= p2.(2*x-1) by A3,A5,A11,MCART_1:def 13
.= (p1 + p2).x by A4,A10,BORSUK_2:def 5;
end;
end;
hence thesis;
end;
theorem
for S, T being non empty pathwise_connected TopSpace, s1, s2, s3 being
Point of S, t1, t2, t3 being Point of T, l1 being Path of [s1,t1],[s2,t2], l2
being Path of [s2,t2],[s3,t3] holds pr2 (l1+l2) = (pr2 l1) + (pr2 l2)
proof
let S, T be non empty pathwise_connected TopSpace, s1, s2, s3 be Point of S,
t1, t2, t3 be Point of T, l1 be Path of [s1,t1],[s2,t2], l2 be Path of [s2,t2],
[s3,t3];
[s1,t1],[s2,t2] are_connected & [s2,t2],[s3,t3] are_connected by
BORSUK_2:def 3;
hence thesis by Th25;
end;
definition
let S, T be non empty TopSpace, s be Point of S, t be Point of T;
set pS = pi_1([:S,T:],[s,t]);
set G = <*pi_1(S,s),pi_1(T,t)*>;
set pT = product G;
func FGPrIso(s,t) -> Function of pi_1([:S,T:],[s,t]), product <*pi_1(S,s),
pi_1(T,t)*> means
:Def2:
for x being Point of pi_1([:S,T:],[s,t]) ex l being
Loop of [s,t] st x = Class(EqRel([:S,T:],[s,t]),l) & it.x = <*Class(EqRel(S,s),
pr1 l),Class(EqRel(T,t),pr2 l)*>;
existence
proof
defpred P[set,set] means ex l being Loop of [s,t] st $1 = Class(EqRel([:S,
T:],[s,t]),l) & $2 = <*Class(EqRel(S,s),pr1 l),Class(EqRel(T,t),pr2 l)*>;
A1: for x being Element of pS ex y being Element of pT st P[x,y]
proof
let x be Element of pS;
consider l being Loop of [s,t] such that
A2: x = Class(EqRel([:S,T:],[s,t]),l) by TOPALG_1:47;
set B = Class(EqRel(T,t),pr2 l);
set A = Class(EqRel(S,s),pr1 l);
A3: dom Carrier G = {1,2} by PARTFUN1:def 2;
A4: now
let x be object such that
A5: x in dom Carrier G;
A6: x = 1 or x = 2 by A5,TARSKI:def 2;
ex R being 1-sorted st R = G.x & Carrier G.x = the carrier of R by A5,
PRALG_1:def 15;
hence <*A,B*>.x in Carrier G.x by A6,TOPALG_1:47;
end;
the carrier of pT = product Carrier G & dom <*A,B*> = {1,2} by FINSEQ_1:2
,89,GROUP_7:def 2;
then reconsider y = <*A,B*> as Element of pT by A3,A4,CARD_3:9;
take y, l;
thus thesis by A2;
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(A1);
hence thesis;
end;
uniqueness
proof
let f, g be Function of pS,pT such that
A9: for x being Point of pi_1([:S,T:],[s,t]) ex l being Loop of [s,t]
st x = Class(EqRel([:S,T:],[s,t]),l) & f.x = <*Class(EqRel(S,s),pr1 l),Class(
EqRel(T,t),pr2 l)*> and
A10: for x being Point of pi_1([:S,T:],[s,t]) ex l being Loop of [s,t]
st x = Class(EqRel([:S,T:],[s,t]),l) & g.x = <*Class(EqRel(S,s),pr1 l),Class(
EqRel(T,t),pr2 l)*>;
now
let x be Point of pS;
consider l1 being Loop of [s,t] such that
A11: x = Class(EqRel([:S,T:],[s,t]),l1) and
A12: f.x = <*Class(EqRel(S,s),pr1 l1),Class(EqRel(T,t),pr2 l1)*> by A9;
consider l2 being Loop of [s,t] such that
A13: x = Class(EqRel([:S,T:],[s,t]),l2) and
A14: g.x = <*Class(EqRel(S,s),pr1 l2),Class(EqRel(T,t),pr2 l2)*> by A10;
A15: l1,l2 are_homotopic by A11,A13,TOPALG_1:46;
then pr2 l1,pr2 l2 are_homotopic by Th20;
then
A16: Class(EqRel(T,t),pr2 l1) = Class(EqRel(T,t),pr2 l2) by TOPALG_1:46;
pr1 l1,pr1 l2 are_homotopic by A15,Th19;
hence f.x = g.x by A12,A14,A16,TOPALG_1:46;
end;
hence thesis;
end;
end;
theorem Th27:
for x being Point of pi_1([:S,T:],[s,t]), l being Loop of [s,t]
st x = Class(EqRel([:S,T:],[s,t]),l) holds FGPrIso(s,t).x = <*Class(EqRel(S,s),
pr1 l),Class(EqRel(T,t),pr2 l)*>
proof
let x be Point of pi_1([:S,T:],[s,t]), l be Loop of [s,t];
consider l1 being Loop of [s,t] such that
A1: x = Class(EqRel([:S,T:],[s,t]),l1) and
A2: FGPrIso(s,t).x = <*Class(EqRel(S,s),pr1 l1),Class(EqRel(T,t),pr2 l1)
*> by Def2;
assume x = Class(EqRel([:S,T:],[s,t]),l);
then
A3: l,l1 are_homotopic by A1,TOPALG_1:46;
then pr2 l,pr2 l1 are_homotopic by Th20;
then
A4: Class(EqRel(T,t),pr2 l) = Class(EqRel(T,t),pr2 l1) by TOPALG_1:46;
pr1 l,pr1 l1 are_homotopic by A3,Th19;
hence thesis by A2,A4,TOPALG_1:46;
end;
theorem Th28:
for l being Loop of [s,t] holds FGPrIso(s,t).Class(EqRel([:S,T:]
,[s,t]),l) = <*Class(EqRel(S,s),pr1 l),Class(EqRel(T,t),pr2 l)*>
proof
let l be Loop of [s,t];
Class(EqRel([:S,T:],[s,t]),l) is Point of pi_1([:S,T:],[s,t]) by TOPALG_1:47;
hence thesis by Th27;
end;
registration
let S, T be non empty TopSpace, s be Point of S, t be Point of T;
cluster FGPrIso(s,t) -> one-to-one onto;
coherence
proof
set F = FGPrIso(s,t);
set G = <*pi_1(S,s),pi_1(T,t)*>;
set pS = pi_1([:S,T:],[s,t]);
set pT = product G;
A1: the carrier of pT = product Carrier G by GROUP_7:def 2;
thus F is one-to-one
proof
let a, b be object;
assume a in dom F;
then consider la being Loop of [s,t] such that
A2: a = Class(EqRel([:S,T:],[s,t]),la) and
A3: F.a = <*Class(EqRel(S,s),pr1 la),Class(EqRel(T,t),pr2 la)*> by Def2;
assume b in dom F;
then consider lb being Loop of [s,t] such that
A4: b = Class(EqRel([:S,T:],[s,t]),lb) and
A5: F.b = <*Class(EqRel(S,s),pr1 lb),Class(EqRel(T,t),pr2 lb)*> by Def2;
assume
A6: F.a = F.b;
then Class(EqRel(T,t),pr2 la) = Class(EqRel(T,t),pr2 lb) by A3,A5,
FINSEQ_1:77;
then
A7: pr2 la, pr2 lb are_homotopic by TOPALG_1:46;
Class(EqRel(S,s),pr1 la) = Class(EqRel(S,s),pr1 lb) by A3,A5,A6,
FINSEQ_1:77;
then pr1 la, pr1 lb are_homotopic by TOPALG_1:46;
then la,lb are_homotopic by A7,Th22;
hence thesis by A2,A4,TOPALG_1:46;
end;
thus rng F c= the carrier of pT;
let y be object;
assume y in the carrier of pT;
then consider g being Function such that
A8: y = g and
A9: dom g = dom Carrier G and
A10: for z being object st z in dom Carrier G holds g.z in Carrier G.z by A1,
CARD_3:def 5;
A11: dom Carrier G = {1,2} by PARTFUN1:def 2;
then reconsider g as FinSequence by A9,FINSEQ_1:2,def 2;
A12: len g = 2 by A9,A11,FINSEQ_1:2,def 3;
A13: ( ex R2 being 1-sorted st R2 = G.2 & Carrier G.2 = the carrier of R2)
& G.2 = pi_1(T,t) by Lm2,PRALG_1:def 15;
g.2 in Carrier G.2 by A10,A11,Lm2;
then consider l2 being Loop of t such that
A14: g.2 = Class(EqRel(T,t),l2) by A13,TOPALG_1:47;
A15: ( ex R1 being 1-sorted st R1 = G.1 & Carrier G.1 = the carrier of R1)
& G.1 = pi_1(S,s) by Lm1,PRALG_1:def 15;
g.1 in Carrier G.1 by A10,A11,Lm1;
then consider l1 being Loop of s such that
A16: g.1 = Class(EqRel(S,s),l1) by A15,TOPALG_1:47;
set x = Class(EqRel([:S,T:],[s,t]),<:l1,l2:>);
A17: dom l1 = I by FUNCT_2:def 1
.= dom l2 by FUNCT_2:def 1;
dom F = the carrier of pS by FUNCT_2:def 1;
then
A18: x in dom F by TOPALG_1:47;
F.x = <*Class(EqRel(S,s),pr1 <:l1,l2:>),Class(EqRel(T,t),pr2 <:l1,l2
:>)*> by Th28
.= <*Class(EqRel(S,s),l1),Class(EqRel(T,t),pr2 <:l1,l2:>)*> by A17,Th7
.= <*Class(EqRel(S,s),l1),Class(EqRel(T,t),l2)*> by A17,Th8
.= y by A8,A12,A16,A14,FINSEQ_1:44;
hence thesis by A18,FUNCT_1:def 3;
end;
end;
registration
let S, T be non empty TopSpace, s be Point of S, t be Point of T;
cluster FGPrIso(s,t) -> multiplicative;
coherence
proof
set F = FGPrIso(s,t);
let a, b be Element of pi_1([:S,T:],[s,t]);
consider la being Loop of [s,t] such that
A1: a = Class(EqRel([:S,T:],[s,t]),la) and
A2: F.a = <*Class(EqRel(S,s),pr1 la),Class(EqRel(T,t),pr2 la)*> by Def2;
consider lb being Loop of [s,t] such that
A3: b = Class(EqRel([:S,T:],[s,t]),lb) and
A4: F.b = <*Class(EqRel(S,s),pr1 lb),Class(EqRel(T,t),pr2 lb)*> by Def2;
reconsider B1 = Class(EqRel(T,t),pr2 la), B2 = Class(EqRel(T,t),pr2 lb)
as Element of pi_1(T,t) by TOPALG_1:47;
reconsider A1 = Class(EqRel(S,s),pr1 la), A2 = Class(EqRel(S,s),pr1 lb)
as Element of pi_1(S,s) by TOPALG_1:47;
consider lab being Loop of [s,t] such that
A5: a*b = Class(EqRel([:S,T:],[s,t]),lab) and
A6: F .(a*b) = <*Class(EqRel(S,s),pr1 lab),Class(EqRel(T,t),pr2 lab) *>
by Def2;
a*b = Class(EqRel([:S,T:],[s,t]),la+lb) by A1,A3,TOPALG_1:61;
then
A7: lab,la+lb are_homotopic by A5,TOPALG_1:46;
then
A8: pr1 lab, pr1(la+lb) are_homotopic by Th19;
A9: pr2 lab, pr2(la+lb) are_homotopic by A7,Th20;
A10: B1*B2 = Class(EqRel(T,t),pr2 la + pr2 lb) by TOPALG_1:61
.= Class(EqRel(T,t),pr2 (la+lb)) by Th25
.= Class(EqRel(T,t),pr2 lab) by A9,TOPALG_1:46;
A1*A2 = Class(EqRel(S,s),pr1 la + pr1 lb) by TOPALG_1:61
.= Class(EqRel(S,s),pr1 (la+lb)) by Th23
.= Class(EqRel(S,s),pr1 lab) by A8,TOPALG_1:46;
hence F.(a*b) = F.a * F.b by A2,A4,A6,A10,GROUP_7:29;
end;
end;
theorem
FGPrIso(s,t) is bijective;
theorem Th30:
pi_1([:S,T:],[s,t]), product <*pi_1(S,s),pi_1(T,t)*> are_isomorphic
proof
take FGPrIso(s,t);
thus thesis;
end;
theorem
for f being Homomorphism of pi_1(S,s1),pi_1(S,s2), g being
Homomorphism of pi_1(T,t1),pi_1(T,t2) st f is bijective & g is bijective holds
Gr2Iso(f,g) * FGPrIso(s1,t1) is bijective
proof
let f be Homomorphism of pi_1(S,s1),pi_1(S,s2), g be Homomorphism of pi_1(T,
t1),pi_1(T,t2);
assume f is bijective & g is bijective;
then
A1: Gr2Iso(f,g) is bijective by Th5;
FGPrIso(s1,t1) is bijective;
hence thesis by A1,GROUP_6:64;
end;
theorem
for S, T being non empty pathwise_connected TopSpace, s1, s2 being
Point of S, t1, t2 being Point of T holds pi_1([:S,T:],[s1,t1]), product <*pi_1
(S,s2),pi_1(T,t2)*> are_isomorphic
proof
let S, T be non empty pathwise_connected TopSpace, s1, s2 be Point of S, t1,
t2 be Point of T;
pi_1(S,s1),pi_1(S,s2) are_isomorphic & pi_1(T,t1),pi_1(T,t2)
are_isomorphic by TOPALG_3:33;
then
A1: product <*pi_1(S,s1),pi_1(T,t1)*>, product <*pi_1(S,s2),pi_1(T,t2)*>
are_isomorphic by Th6;
pi_1([:S,T:],[s1,t1]), product <*pi_1(S,s1),pi_1(T,t1)*> are_isomorphic
by Th30;
hence thesis by A1,GROUP_6:67;
end;