:: Commutativeness of Fundamental Groups of Topological Groups :: by Artur Korni{\l}owicz :: :: Received May 19, 2013 :: Copyright (c) 2013-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 NUMBERS, GROUP_1, RELAT_1, FUNCT_1, SUBSET_1, BORSUK_1, PRE_TOPC, CARD_1, XBOOLE_0, ARYTM_3, RCOMP_1, TARSKI, ORDINAL2, ZFMISC_1, BORSUK_2, ALGSTR_1, EQREL_1, WAYBEL20, ALGSTR_0, BINOP_1, BORSUK_6, TOPALG_1, TOPGRP_1, CONNSP_2, XXREAL_0, FUNCOP_1, STRUCT_0, ARYTM_1, VALUED_1, TOPMETR, SETFAM_1, TOPS_1, XXREAL_1, REALSET1, TOPALG_7, REAL_1, MCART_1; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, EQREL_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, REALSET1, FUNCT_3, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, RCOMP_1, FUNCOP_1, STRUCT_0, ALGSTR_0, PRE_TOPC, TOPS_1, CONNSP_2, GROUP_1, GROUP_2, BORSUK_1, BORSUK_2, BORSUK_6, TOPMETR, TOPALG_1, TOPREALB, TOPGRP_1; constructors TOPS_1, REALSET2, GROUP_6, BORSUK_6, MONOID_0, TOPALG_1, TOPGRP_1, COMPTS_1, FUNCOP_1, TOPREALB; registrations XBOOLE_0, RELSET_1, FUNCT_2, XXREAL_0, XREAL_0, MEMBERED, STRUCT_0, TOPS_1, BORSUK_1, BORSUK_2, MONOID_0, PRE_TOPC, TOPALG_1, FUNCOP_1, TOPGRP_1, TOPMETR, TOPALG_3, ORDINAL1; requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL; begin definition let A,B be non empty TopSpace, C be set, f be Function of [:A,B:],C; let a be Element of A; let b be Element of B; redefine func f.(a,b) -> Element of C; end; definition let G be multMagma, g be Element of G; attr g is unital means :: TOPALG_7:def 1 g = 1_G; end; registration let G be multMagma; cluster 1_G -> unital; end; registration let G be unital multMagma; cluster unital for Element of G; end; registration let G be unital multMagma, g be Element of G, h be unital Element of G; reduce g * h to g; reduce h * g to g; end; registration let G be Group; reduce (1_G)" to 1_G; end; scheme :: TOPALG_7:sch 1 TopFuncEx { S,T() -> non empty TopSpace, X() -> non empty set, F(Point of S(),Point of T()) -> Element of X() } : ex f being Function of [:S(),T():],X() st for s being Point of S(), t being Point of T() holds f.(s,t) = F(s,t); scheme :: TOPALG_7:sch 2 TopFuncEq { S,T() -> non empty TopSpace, X() -> non empty set, F(Point of S(),Point of T()) -> Element of X() } : for f,g being Function of [:S(),T():],X() st (for s being Point of S(), t being Point of T() holds f.(s,t) = F(s,t)) & (for s being Point of S(), t being Point of T() holds g.(s,t) = F(s,t)) holds f = g; definition let X be non empty set; let T be non empty multMagma; let f,g be Function of X,T; func f(#)g -> Function of X,T means :: TOPALG_7:def 2 for x being Element of X holds it.x = f.x * g.x; end; theorem :: TOPALG_7:1 for X being non empty set, T being associative non empty multMagma for f,g,h being Function of X,T holds f(#)g(#)h = f(#)(g(#)h); definition let X be non empty set, T be commutative non empty multMagma; let f,g be Function of X,T; redefine func f(#)g; commutativity; end; definition let T be non empty TopGrStr; let t be Point of T; let f,g be Loop of t; func LoopMlt(f,g) -> Function of I[01],T equals :: TOPALG_7:def 3 f(#)g; end; reserve T for BinContinuous unital TopSpace-like non empty TopGrStr, x,y for Point of I[01], s,t for unital Point of T, f,g for Loop of t, c for constant Loop of t; definition let T,t,f,g; redefine func LoopMlt(f,g) -> Loop of t; end; registration let T be UnContinuous TopGroup; cluster inverse_op(T) -> continuous; end; definition let T be TopGroup, t be Point of T, f be Loop of t; func inverse_loop(f) -> Function of I[01],T equals :: TOPALG_7:def 4 inverse_op(T) * f; end; theorem :: TOPALG_7:2 for T being TopGroup, t being Point of T, f being Loop of t holds inverse_loop(f).x = (f.x)"; theorem :: TOPALG_7:3 for T being TopGroup, t being Point of T, f being Loop of t holds inverse_loop(f).x * f.x = 1_T; theorem :: TOPALG_7:4 for T being TopGroup, t being Point of T, f being Loop of t holds f.x * inverse_loop(f).x = 1_T; definition let T be UnContinuous TopGroup,t be unital Point of T,f be Loop of t; redefine func inverse_loop(f) -> Loop of t; end; definition let s,t be Point of I[01]; redefine func s*t -> Point of I[01]; end; definition func R^1-TIMES -> Function of [:R^1,R^1:],R^1 means :: TOPALG_7:def 5 for x,y being Point of R^1 holds it.(x,y) = x*y; end; registration cluster R^1-TIMES -> continuous; end; theorem :: TOPALG_7:5 [:R^1,R^1:] | [:R^1([.0,1.]),R^1([.0,1.]):] = [:I[01],I[01]:]; definition func I[01]-TIMES -> Function of [:I[01],I[01]:],I[01] equals :: TOPALG_7:def 6 R^1-TIMES || R^1([.0,1.]); end; theorem :: TOPALG_7:6 I[01]-TIMES.(x,y) = x*y; registration cluster I[01]-TIMES -> continuous; end; theorem :: TOPALG_7:7 for a,b being Point of I[01] holds for N being a_neighborhood of a*b ex N1 being a_neighborhood of a, N2 being a_neighborhood of b st for x,y being Point of I[01] st x in N1 & y in N2 holds x*y in N; definition let T be non empty multMagma; let F,G be Function of [:I[01],I[01]:],T; func HomotopyMlt(F,G) -> Function of [:I[01],I[01]:],T means :: TOPALG_7:def 7 for a,b being Point of I[01] holds it.(a,b) = F.(a,b) * G.(a,b); end; theorem :: TOPALG_7:8 for F,G being Function of [:I[01],I[01]:],T for M,N being Subset of [:I[01],I[01]:] holds HomotopyMlt(F,G).:(M/\N) c= F.:M * G.:N; registration let T; let F,G be continuous Function of [:I[01],I[01]:],T; cluster HomotopyMlt(F,G) -> continuous; end; theorem :: TOPALG_7:9 for f1,f2,g1,g2 being Loop of t st f1,f2 are_homotopic & g1,g2 are_homotopic holds LoopMlt(f1,g1),LoopMlt(f2,g2) are_homotopic; theorem :: TOPALG_7:10 for f1,f2,g1,g2 being Loop of t, F being Homotopy of f1,f2, G being Homotopy of g1,g2 st f1,f2 are_homotopic & g1,g2 are_homotopic holds HomotopyMlt(F,G) is Homotopy of LoopMlt(f1,g1),LoopMlt(f2,g2); theorem :: TOPALG_7:11 f+g = LoopMlt(f+c,c+g); theorem :: TOPALG_7:12 LoopMlt(f,g),LoopMlt(f+c,c+g) are_homotopic; definition let T be TopGroup,t be Point of T,f,g be Loop of t; func HopfHomotopy(f,g) -> Function of [:I[01],I[01]:],T means :: TOPALG_7:def 8 for a,b being Point of I[01] holds it.(a,b) = inverse_loop(f).(a*b) * f.a * g.a * f.(a*b); end; registration let T be TopologicalGroup, t be Point of T, f,g be Loop of t; cluster HopfHomotopy(f,g) -> continuous; end; reserve T for TopologicalGroup, t for unital Point of T, f,g for Loop of t; theorem :: TOPALG_7:13 LoopMlt(f,g),LoopMlt(g,f) are_homotopic; definition let T,t,f,g; redefine func HopfHomotopy(f,g) -> Homotopy of LoopMlt(f,g),LoopMlt(g,f); end; registration let T,t; cluster pi_1(T,t) -> commutative; end;