:: On the Fundamental Groups of Products of Topological Spaces :: by Artur Korni{\l}owicz :: :: Received August 20, 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 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; begin theorem :: TOPALG_4:1 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*>; 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 :: TOPALG_4:def 1 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*>; end; theorem :: TOPALG_4:2 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*>; 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; end; theorem :: TOPALG_4:3 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; theorem :: TOPALG_4:4 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; theorem :: TOPALG_4:5 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; theorem :: TOPALG_4:6 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; begin 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 :: TOPALG_4:7 for f, g being Function st dom f = dom g holds pr1 <:f,g:> = f; theorem :: TOPALG_4:8 for f, g being Function st dom f = dom g holds pr2 <:f,g:> = g; 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:]; end; definition let S, T, Y; let f be Function of Y, [:S,T:]; redefine func pr1 f -> Function of Y,S; redefine func pr2 f -> Function of Y,T; end; theorem :: TOPALG_4:9 for f being continuous Function of Y,[:S,T:] holds pr1 f is continuous; theorem :: TOPALG_4:10 for f being continuous Function of Y,[:S,T:] holds pr2 f is continuous; theorem :: TOPALG_4:11 [s1,t1],[s2,t2] are_connected implies s1,s2 are_connected; theorem :: TOPALG_4:12 [s1,t1],[s2,t2] are_connected implies t1,t2 are_connected; theorem :: TOPALG_4:13 [s1,t1],[s2,t2] are_connected implies for L being Path of [s1,t1 ],[s2,t2] holds pr1 L is Path of s1,s2; theorem :: TOPALG_4:14 [s1,t1],[s2,t2] are_connected implies for L being Path of [s1,t1 ],[s2,t2] holds pr2 L is Path of t1,t2; theorem :: TOPALG_4:15 s1,s2 are_connected & t1,t2 are_connected implies [s1,t1],[s2,t2 ] are_connected; theorem :: TOPALG_4:16 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 ]; 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]; 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]; end; registration let S, T be non empty pathwise_connected TopSpace; cluster [:S,T:] -> pathwise_connected; 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; redefine func pr2 L -> Path of t1,t2; 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; redefine func pr2 L -> Loop of t; end; theorem :: TOPALG_4:17 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; theorem :: TOPALG_4:18 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; theorem :: TOPALG_4:19 for p, q being Path of s1,s2 st p = pr1 l1 & q = pr1 l2 & l1,l2 are_homotopic holds p,q are_homotopic; theorem :: TOPALG_4:20 for p, q being Path of t1,t2 st p = pr2 l1 & q = pr2 l2 & l1,l2 are_homotopic holds p,q are_homotopic; theorem :: TOPALG_4:21 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; theorem :: TOPALG_4:22 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; theorem :: TOPALG_4:23 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; theorem :: TOPALG_4:24 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); theorem :: TOPALG_4:25 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; theorem :: TOPALG_4:26 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); definition let S, T be non empty TopSpace, s be Point of S, t be Point of T; func FGPrIso(s,t) -> Function of pi_1([:S,T:],[s,t]), product <*pi_1(S,s), pi_1(T,t)*> means :: TOPALG_4:def 2 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)*>; end; theorem :: TOPALG_4:27 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)*>; theorem :: TOPALG_4:28 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)*>; 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; end; registration let S, T be non empty TopSpace, s be Point of S, t be Point of T; cluster FGPrIso(s,t) -> multiplicative; end; theorem :: TOPALG_4:29 FGPrIso(s,t) is bijective; theorem :: TOPALG_4:30 pi_1([:S,T:],[s,t]), product <*pi_1(S,s),pi_1(T,t)*> are_isomorphic; theorem :: TOPALG_4:31 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; theorem :: TOPALG_4:32 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;