:: Commutativeness of Fundamental Groups of Topological Groups
:: by Artur Korni{\l}owicz
::
:: Received May 19, 2013
:: Copyright (c) 2013-2016 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,
TOPGRP_1, TOPMETR, TOPALG_3, ORDINAL1;
requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL;
begin
registration
let A be non empty set, x be object, a be Element of A;
reduce (A --> x).a to x;
end;
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;