:: Commutativeness of Fundamental Groups of Topological Groups
:: by Artur Korni{\l}owicz
::
:: Received May 19, 2013
:: Copyright (c) 2013-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 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;
definitions TARSKI, FUNCT_2, GROUP_1, BORSUK_1, BORSUK_2, BORSUK_6;
equalities BINOP_1, REALSET1, STRUCT_0, GROUP_2, BORSUK_1, TOPALG_1, TOPREALB;
expansions TARSKI, BORSUK_2;
theorems TOPALG_1, GROUP_1, BORSUK_1, BORSUK_2, TOPGRP_1, XREAL_1, TARSKI,
CONNSP_2, FUNCT_2, XBOOLE_0, FUNCOP_1, BORSUK_6, ZFMISC_1, PRE_TOPC,
TOPS_1, TOPMETR, TOPREALA, REALSET1, FUNCT_1, TSEP_1, BORSUK_3, BINOP_1,
JGRAPH_2, YELLOW12, FUNCT_3;
schemes FUNCT_2, BINOP_1;
begin
set I = I[01];
set II = [:I,I:];
set R = R^1;
set RR = [:R,R:];
set A = R^1([.0,1.]);
set cR = the carrier of R;
Lm1: the carrier of RR = [:cR,cR:] by BORSUK_1:def 2;
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; :: redefines . (BINOP_1, definition)
coherence
proof
f. [a,b] is Element of C;
hence thesis;
end;
end;
definition
let G be multMagma, g be Element of G;
attr g is unital means :Def1:
g = 1_G;
end;
registration
let G be multMagma;
cluster 1_G -> unital;
coherence;
end;
registration
let G be unital multMagma;
cluster unital for Element of G;
existence
proof
take 1_G;
thus 1_G = 1_G;
end;
end;
registration
let G be unital multMagma, g be Element of G, h be unital Element of G;
reduce g * h to g;
reducibility
proof
h = 1_G by Def1;
hence thesis by GROUP_1:def 4;
end;
reduce h * g to g;
reducibility
proof
h = 1_G by Def1;
hence thesis by GROUP_1:def 4;
end;
end;
registration
let G be Group;
reduce (1_G)" to 1_G;
reducibility by GROUP_1:8;
end;
scheme 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);
consider f being Function of [:the carrier of S(),the carrier of T():],X()
such that
A1: for x being Point of S(), y being Point of T() holds f.(x,y) = F(x,y)
from BINOP_1:sch 4;
[:the carrier of S(),the carrier of T():] = the carrier of [:S(),T():]
by BORSUK_1:def 2;
then reconsider f as Function of [:S(),T():],X();
take f;
thus thesis by A1;
end;
scheme 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;
let f,g be Function of [:S(),T():],X() such that
A1: for a being Point of S(), b being Point of T() holds f.(a,b) = F(a,b) and
A2: for a being Point of S(), b being Point of T() holds g.(a,b) = F(a,b);
let x be Point of [:S(),T():];
consider a being Point of S(), b being Point of T() such that
A3: x = [a,b] by BORSUK_1:10;
thus f.x = f.(a,b) by A3
.= F(a,b) by A1
.= g.(a,b) by A2
.= g.x by A3;
end;
definition
let X be non empty set;
let T be non empty multMagma;
let f,g be Function of X,T;
deffunc F(Element of X) = f.$1 * g.$1;
func f(#)g -> Function of X,T means :Def2:
for x being Element of X holds it.x = f.x * g.x;
existence
proof
thus ex f being Function of X,T st
for x being Element of X holds f.x = F(x) from FUNCT_2:sch 4;
end;
uniqueness
proof
let F,G be Function of X,T such that
A1: for x being Element of X holds F.x = F(x) and
A2: for x being Element of X holds G.x = F(x);
let x be Element of X;
thus F.x = F(x) by A1
.= G.x by A2;
end;
end;
theorem
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)
proof
let X be non empty set;
let T be associative non empty multMagma;
let f,g,h be Function of X,T;
let x be Element of X;
thus (f(#)g(#)h).x = (f(#)g).x*h.x by Def2
.= f.x*g.x*h.x by Def2
.= f.x*(g.x*h.x) by GROUP_1:def 3
.= f.x*(g(#)h).x by Def2
.= (f(#)(g(#)h)).x by Def2;
end;
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; :: redefines (#) (TOPALG_7, definition)
commutativity
proof let f,g be Function of X,T;
let x be Element of X;
thus (f(#)g).x = f.x*g.x by Def2
.= (g(#)f).x by Def2;
end;
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
f(#)g;
coherence;
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; :: redefines LoopMlt (TOPALG_7, definition)
coherence
proof
set F = LoopMlt(f,g);
thus
A1: t,t are_connected;
thus F is continuous
proof
let a be Point of I, G be a_neighborhood of F.a;
F.a = f.a * g.a by Def2;
then consider A being open a_neighborhood of f.a,
B being open a_neighborhood of g.a such that
A2: A * B c= G by TOPGRP_1:37;
consider Ha being a_neighborhood of a such that
A3: f.:Ha c= A by BORSUK_1:def 1;
consider Hb being a_neighborhood of a such that
A4: g.:Hb c= B by BORSUK_1:def 1;
reconsider H = Ha /\ Hb as a_neighborhood of a by CONNSP_2:2;
take H;
F.:H c= A * B
proof
let y be object;
assume y in F.:H;
then consider c being Element of I such that
A5: c in H and
A6: F.c = y by FUNCT_2:65;
A7: F.c = f.c * g.c by Def2;
c in Ha & c in Hb by A5,XBOOLE_0:def 4;
then f.c in f.:Ha & g.c in g.:Hb by FUNCT_2:35;
hence thesis by A3,A4,A6,A7;
end;
hence F.:H c= G by A2;
end;
A8: t = 1_T by Def1;
A9: 1_T * 1_T = 1_T;
f.0[01] = t & g.0[01] = t & f.1[01] = t & g.1[01] = t by A1,BORSUK_2:def 2;
hence thesis by A8,A9,Def2;
end;
end;
registration
let T be UnContinuous TopGroup;
cluster inverse_op(T) -> continuous;
coherence;
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
inverse_op(T) * f;
coherence;
end;
theorem Th2:
for T being TopGroup, t being Point of T, f being Loop of t holds
inverse_loop(f).x = (f.x)"
proof
let T be TopGroup;
let t be Point of T;
let f be Loop of t;
thus inverse_loop(f).x = inverse_op(T).(f.x) by FUNCT_2:15
.= (f.x)" by GROUP_1:def 6;
end;
theorem Th3:
for T being TopGroup, t being Point of T, f being Loop of t holds
inverse_loop(f).x * f.x = 1_T
proof
let T be TopGroup, t be Point of T, f be Loop of t;
inverse_loop(f).x = (f.x)" by Th2;
hence thesis by GROUP_1:def 5;
end;
theorem
for T being TopGroup, t being Point of T, f being Loop of t holds
f.x * inverse_loop(f).x = 1_T
proof
let T be TopGroup, t be Point of T, f be Loop of t;
inverse_loop(f).x = (f.x)" by Th2;
hence thesis by GROUP_1:def 5;
end;
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; :: redefines inverse_loop (TOPALG_7, definition)
coherence
proof
thus
A1: t,t are_connected;
thus inverse_loop(f) is continuous;
A2: t = 1_T by Def1;
A3: (1_T)" = 1_T;
f.0[01] = t & f.1[01] = t by A1,BORSUK_2:def 2;
hence thesis by A2,A3,Th2;
end;
end;
definition
let s,t be Point of I[01];
redefine func s*t -> Point of I[01]; :: redefines * (XCMPLX_0, definition)
coherence
proof
0 <= s & 0 <= t & s <= 1 & t <= 1 by BORSUK_1:43;
hence thesis by BORSUK_1:43,XREAL_1:160;
end;
end;
definition
func R^1-TIMES -> Function of [:R^1,R^1:],R^1 means :Def5:
for x,y being Point of R^1 holds it.(x,y) = x*y;
existence
proof
deffunc F(Point of R,Point of R) = R^1($1*$2);
consider f being Function of RR,R such that
A1: for s,t being Point of R holds f.(s,t) = F(s,t) from TopFuncEx;
take f;
let x,y be Point of R;
f.(x,y) = F(x,y) by A1;
hence thesis;
end;
uniqueness
proof
let f,g be Function of RR,R such that
A2: for x,y being Point of R holds f.(x,y) = x*y and
A3: for x,y being Point of R holds g.(x,y) = x*y;
now
let x,y be Point of R;
thus f.(x,y) = x*y by A2
.= g.(x,y) by A3;
end;
hence thesis by Lm1,BINOP_1:2;
end;
end;
registration
cluster R^1-TIMES -> continuous;
coherence
proof
reconsider f1 = pr1(cR,cR) as continuous Function of RR,R by YELLOW12:39;
reconsider f2 = pr2(cR,cR) as continuous Function of RR,R by YELLOW12:40;
consider g being Function of RR,R such that
A1: for p being Point of RR, r1,r2 being Real st f1.p = r1 & f2.p = r2 holds
g.p = r1*r2 and
A2: g is continuous by JGRAPH_2:25;
now
let a,b be Point of R;
A3: f1.(a,b) = a & f2.(a,b) = b by FUNCT_3:def 4,def 5;
thus R^1-TIMES.(a,b) = a*b by Def5
.= g. [a,b] by A1,A3
.= g.(a,b);
end;
hence thesis by A2,Lm1,BINOP_1:2;
end;
end;
theorem Th5:
[:R^1,R^1:] | [:R^1([.0,1.]),R^1([.0,1.]):] = [:I[01],I[01]:]
proof
A1: II is SubSpace of RR by BORSUK_3:21;
the carrier of II = [:A,A:] by BORSUK_1:def 2,40;
hence thesis by A1,TSEP_1:5,PRE_TOPC:8;
end;
definition
func I[01]-TIMES -> Function of [:I[01],I[01]:],I[01] equals
R^1-TIMES || R^1([.0,1.]);
coherence
proof
reconsider f = R^1-TIMES as BinOp of cR by Lm1;
for x being set holds x in [:A,A:] implies f.x in A
proof
let x be set;
assume x in [:A,A:];
then consider a,b being object such that
A1: a in A & b in A and
A2: x = [a,b] by ZFMISC_1:def 2;
reconsider a,b as Point of I by A1,BORSUK_1:40;
reconsider a1 = a, b1 = b as Point of R by A1;
f.(a1,b1) = a*b by Def5;
hence f.x in A by A2,BORSUK_1:40;
end;
then reconsider A as Preserv of f by REALSET1:def 1;
A3: the carrier of II = [:the carrier of I,the carrier of I:]
by BORSUK_1:def 2;
f || A is BinOp of A;
hence thesis by A3,BORSUK_1:40;
end;
end;
theorem Th6:
I[01]-TIMES.(x,y) = x*y
proof
x is Point of R & y is Point of R by PRE_TOPC:25;
hence x*y = R^1-TIMES.(x,y) by Def5
.= I[01]-TIMES.(x,y) by FUNCT_1:49,ZFMISC_1:87,BORSUK_1:40;
end;
registration
cluster I[01]-TIMES -> continuous;
coherence
proof
reconsider f = I[01]-TIMES as Function of II,R by TOPREALA:7;
f is continuous by Th5,TOPMETR:7;
hence thesis by PRE_TOPC:27;
end;
end;
theorem Th7:
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
proof
let a,b be Point of I;
let N be a_neighborhood of a*b;
set g = I[01]-TIMES;
g.(a,b) = a*b by Th6;
then consider H being a_neighborhood of [a,b] such that
A1: g.:H c= N by BORSUK_1:def 1;
consider F being Subset-Family of [:I,I:] such that
A2: Int H = union F and
A3: for e being set st e in F ex X1, Y1 being Subset of I st e = [:X1,Y1:] &
X1 is open & Y1 is open by BORSUK_1:5;
[a,b] in Int H by CONNSP_2:def 1;
then consider M being set such that
A4: [a,b] in M and
A5: M in F by A2,TARSKI:def 4;
consider A, B being Subset of I such that
A6: M = [:A,B:] and
A7: A is open and
A8: B is open by A3,A5;
a in A by A4,A6,ZFMISC_1:87;
then
A9: a in Int A by A7,TOPS_1:23;
b in B by A4,A6,ZFMISC_1:87;
then b in Int B by A8,TOPS_1:23;
then reconsider B as open a_neighborhood of b by A8,CONNSP_2:def 1;
reconsider A as open a_neighborhood of a by A7,A9,CONNSP_2:def 1;
take A,B;
let x,y be Point of I such that
A10: x in A & y in B;
A11: Int H c= H by TOPS_1:16;
A12: g.(x,y) = x*y by Th6;
[x,y] in M by A6,A10,ZFMISC_1:87;
then [x,y] in Int H by A2,A5,TARSKI:def 4;
then g.(x,y) in g.:H by A11,FUNCT_2:35;
hence thesis by A1,A12;
end;
definition
let T be non empty multMagma;
let F,G be Function of [:I[01],I[01]:],T;
deffunc F(Point of I,Point of I) = F.($1,$2) * G.($1,$2);
func HomotopyMlt(F,G) -> Function of [:I[01],I[01]:],T means :Def7:
for a,b being Point of I[01] holds it.(a,b) = F.(a,b) * G.(a,b);
existence
proof
thus ex f being Function of II,T st
for a,b being Point of I holds f.(a,b) = F(a,b) from TopFuncEx;
end;
uniqueness
proof
thus for f,g being Function of II,T st
(for a,b being Point of I holds f.(a,b) = F(a,b)) &
(for a,b being Point of I holds g.(a,b) = F(a,b)) holds f = g
from TopFuncEq;
end;
end;
Lm2: now
let T,t,x;
let f1,f2,g1,g2 be Loop of t,
F be Homotopy of f1,f2, G be Homotopy of g1,g2;
assume
A1: f1,f2 are_homotopic & g1,g2 are_homotopic;
then
A2: F.(x,0[01]) = f1.x & G.(x,0[01]) = g1.x by BORSUK_6:def 11;
thus HomotopyMlt(F,G).(x,0) = F.(x,0[01]) * G.(x,0[01]) by Def7
.= LoopMlt(f1,g1).x by A2,Def2;
A3: F.(x,1[01]) = f2.x & G.(x,1[01]) = g2.x by A1,BORSUK_6:def 11;
thus HomotopyMlt(F,G).(x,1) = F.(x,1[01]) * G.(x,1[01]) by Def7
.= LoopMlt(f2,g2).x by A3,Def2;
F.(0[01],x) = t & G.(0[01],x) = t by A1,BORSUK_6:def 11;
hence HomotopyMlt(F,G).(0,x) = t * t by Def7
.= t;
F.(1[01],x) = t & G.(1[01],x) = t by A1,BORSUK_6:def 11;
hence HomotopyMlt(F,G).(1,x) = t * t by Def7
.= t;
end;
theorem Th8:
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
proof
let F,G be Function of II,T;
let M,N be Subset of II;
let y be object;
assume y in HomotopyMlt(F,G).:(M/\N);
then consider x being Point of II such that
A1: x in M /\ N and
A2: HomotopyMlt(F,G).x = y by FUNCT_2:65;
consider a,b being Point of I such that
A3: x = [a,b] by BORSUK_1:10;
A4: HomotopyMlt(F,G).(a,b) = F.(a,b) * G.(a,b) by Def7;
[a,b] in M & [a,b] in N by A1,A3,XBOOLE_0:def 4;
then F.(a,b) in F.:M & G.(a,b) in G.:N by FUNCT_2:35;
hence thesis by A2,A3,A4;
end;
registration
let T;
let F,G be continuous Function of [:I[01],I[01]:],T;
cluster HomotopyMlt(F,G) -> continuous;
coherence
proof
let W be Point of II,
N be a_neighborhood of HomotopyMlt(F,G).W;
consider a,b being Point of I such that
A1: W = [a,b] by BORSUK_1:10;
HomotopyMlt(F,G).(a,b) = F.(a,b) * G.(a,b) by Def7;
then consider A being open a_neighborhood of F.(a,b),
B being open a_neighborhood of G.(a,b) such that
A2: A * B c= N by A1,TOPGRP_1:37;
consider NF being a_neighborhood of [a,b] such that
A3: F.:NF c= A by BORSUK_1:def 1;
consider NG being a_neighborhood of [a,b] such that
A4: G.:NG c= B by BORSUK_1:def 1;
reconsider H = NF /\ NG as a_neighborhood of W by A1,CONNSP_2:2;
take H;
A5: HomotopyMlt(F,G).:(NF/\NG) c= F.:NF * G.:NG by Th8;
F.:NF * G.:NG c= A * B by A3,A4,TOPGRP_1:4;
hence thesis by A5,A2;
end;
end;
theorem Th9:
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
proof
let f1,f2,g1,g2 be Loop of t;
assume
A1: f1,f2 are_homotopic;
then consider F being Function of II,T such that
A2: F is continuous &
for x being Point of I holds F.(x,0) = f1.x & F.(x,1) = f2.x &
F.(0,x) = t & F.(1,x) = t;
assume
A3: g1,g2 are_homotopic;
then consider G being Function of II,T such that
A4: G is continuous &
for x being Point of I holds G.(x,0) = g1.x & G.(x,1) = g2.x &
G.(0,x) = t & G.(1,x) = t;
take HomotopyMlt(F,G);
F is Homotopy of f1,f2 & G is Homotopy of g1,g2
by A2,A4,A1,A3,BORSUK_6:def 11;
hence thesis by A1,A2,A3,A4,Lm2;
end;
theorem
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)
proof
let f1,f2,g1,g2 be Loop of t,
F be Homotopy of f1,f2, G be Homotopy of g1,g2 such that
A1: f1,f2 are_homotopic & g1,g2 are_homotopic;
thus LoopMlt(f1,g1),LoopMlt(f2,g2) are_homotopic by A1,Th9;
F is continuous & G is continuous by A1,BORSUK_6:def 11;
hence HomotopyMlt(F,G) is continuous;
thus thesis by A1,Lm2;
end;
theorem Th11:
f+g = LoopMlt(f+c,c+g)
proof
let x;
A1: c = I --> t by BORSUK_2:5;
now per cases;
suppose
A2: x <= 1/2;
then reconsider z = 2*x as Point of I by BORSUK_6:3;
A3: (f+c).x = f.z by A2,BORSUK_2:def 5;
(c+g).x = c.z by A2,BORSUK_2:def 5
.= t by A1;
hence (f+g).x = (f+c).x * (c+g).x by A2,A3,BORSUK_2:def 5;
end;
suppose
A4: x >= 1/2;
then reconsider z = 2*x-1 as Point of I by BORSUK_6:4;
A5: (f+c).x = c.z by A4,BORSUK_2:def 5
.= t by A1;
(c+g).x = g.z by A4,BORSUK_2:def 5;
hence (f+g).x = (f+c).x * (c+g).x by A5,A4,BORSUK_2:def 5;
end;
end;
hence thesis by Def2;
end;
theorem Th12:
LoopMlt(f,g),LoopMlt(f+c,c+g) are_homotopic
proof
f,f+c are_homotopic & c+g,g are_homotopic by BORSUK_6:80,82;
hence thesis by Th9;
end;
definition
let T be TopGroup,t be Point of T,f,g be Loop of t;
deffunc F(Point of I,Point of I) =
inverse_loop(f).($1*$2) * f.$1 * g.$1 * f.($1*$2);
func HopfHomotopy(f,g) -> Function of [:I[01],I[01]:],T means :Def8:
for a,b being Point of I[01] holds
it.(a,b) = inverse_loop(f).(a*b) * f.a * g.a * f.(a*b);
existence
proof
thus ex F being Function of II,T st
for x,y being Point of I holds F.(x,y) = F(x,y) from TopFuncEx;
end;
uniqueness
proof
thus for f,g being Function of II,T st
(for a,b being Point of I holds f.(a,b) = F(a,b)) &
(for a,b being Point of I holds g.(a,b) = F(a,b)) holds f = g
from TopFuncEq;
end;
end;
registration
let T be TopologicalGroup, t be Point of T, f,g be Loop of t;
cluster HopfHomotopy(f,g) -> continuous;
coherence
proof
set F = HopfHomotopy(f,g);
set i = inverse_loop(f);
let W be Point of II,
G be a_neighborhood of F.W;
consider a,b being Point of I such that
A1: W = [a,b] by BORSUK_1:10;
F.(a,b) = i.(a*b) * f.a * g.a * f.(a*b) by Def8;
then consider A1 being open a_neighborhood of i.(a*b) * f.a * g.a,
B1 being open a_neighborhood of f.(a*b) such that
A2: A1*B1 c= G by A1,TOPGRP_1:37;
consider A2 being open a_neighborhood of i.(a*b) * f.a,
B2 being open a_neighborhood of g.a such that
A3: A2*B2 c= A1 by TOPGRP_1:37;
consider A3 being open a_neighborhood of i.(a*b),
B3 being open a_neighborhood of f.a such that
A4: A3*B3 c= A2 by TOPGRP_1:37;
i.(a*b) = inverse_op(T).(f.(a*b)) by FUNCT_2:15
.= (f.(a*b))" by GROUP_1:def 6;
then consider A4 being open a_neighborhood of f.(a*b) such that
A5: A4" c= A3 by TOPGRP_1:39;
consider A5 being a_neighborhood of a*b such that
A6: f.:A5 c= A4 by BORSUK_1:def 1;
consider NB1 being a_neighborhood of a*b such that
A7: f.:NB1 c= B1 by BORSUK_1:def 1;
consider NB2 being a_neighborhood of a such that
A8: g.:NB2 c= B2 by BORSUK_1:def 1;
consider NB3 being a_neighborhood of a such that
A9: f.:NB3 c= B3 by BORSUK_1:def 1;
A5/\NB1 is a_neighborhood of a*b by CONNSP_2:2;
then consider N1 being a_neighborhood of a,
N2 being a_neighborhood of b such that
A10: for x,y being Point of I st x in N1 & y in N2 holds x*y in A5/\NB1 by Th7;
N1/\NB2 is a_neighborhood of a by CONNSP_2:2;
then reconsider Na = N1/\NB2/\NB3 as a_neighborhood of a by CONNSP_2:2;
reconsider H = [:Na,N2:] as a_neighborhood of W by A1;
take H;
let y be object;
assume y in F.:H;
then consider x being Element of II such that
A11: x in H and
A12: F.x = y by FUNCT_2:65;
consider c,d being Point of I such that
A13: x = [c,d] by BORSUK_1:10;
A14: i.(c*d) = inverse_op(T).(f.(c*d)) by FUNCT_2:15
.= (f.(c*d))" by GROUP_1:def 6;
A15: F.(c,d) = i.(c*d) * f.c * g.c * f.(c*d) by Def8;
A16: c in N1/\NB2/\NB3 by A11,A13,ZFMISC_1:87;
A17: c in N1/\NB2 by A16,XBOOLE_0:def 4;
then
A18: c in N1 by XBOOLE_0:def 4;
d in N2 by A11,A13,ZFMISC_1:87;
then
A19: c*d in A5/\NB1 by A18,A10;
then c*d in A5 by XBOOLE_0:def 4;
then f.(c*d) in f.:A5 by FUNCT_2:35;
then
A20: (f.(c*d))" in A4" by A6;
c in NB3 by A16,XBOOLE_0:def 4;
then f.c in f.:NB3 by FUNCT_2:35;
then
A21: i.(c*d)*f.c in A3*B3 by A5,A9,A14,A20;
c in NB2 by A17,XBOOLE_0:def 4;
then g.c in g.:NB2 by FUNCT_2:35;
then
A22: i.(c*d)*f.c*g.c in A2*B2 by A4,A8,A21;
c*d in NB1 by A19,XBOOLE_0:def 4;
then f.(c*d) in f.:NB1 by FUNCT_2:35;
then i.(c*d)*f.c*g.c*f.(c*d) in A1*B1 by A3,A7,A22;
hence thesis by A2,A12,A13,A15;
end;
end;
reserve
T for TopologicalGroup,
t for unital Point of T,
f,g for Loop of t;
Lm3: now
let T,t,f,g,x;
set F = HopfHomotopy(f,g);
set i = inverse_loop(f);
A1: t = 1_T by Def1;
A2: t,t are_connected;
A3: f.0[01] = t by A2,BORSUK_2:def 2;
A4: f.1[01] = t by A2,BORSUK_2:def 2;
A5: g.0[01] = t by A2,BORSUK_2:def 2;
A6: i.0[01] = t by A2,BORSUK_2:def 2;
thus F.(x,0) = i.(x*0[01]) * f.x * g.x * f.(x*0[01]) by Def8
.= LoopMlt(f,g).x by A3,A6,Def2;
thus F.(x,1) = i.(x*1[01]) * f.x * g.x * f.(x*1[01]) by Def8
.= t * g.x * f.x by A1,Th3
.= LoopMlt(g,f).x by Def2;
thus F.(0,x) = i.(0[01]*x) * f.0[01] * g.0[01] * f.(0[01]*x) by Def8
.= t by A3,A5,A2,BORSUK_2:def 2;
thus F.(1,x) = i.(1[01]*x) * f.1[01] * g.1[01] * f.(1[01]*x) by Def8
.= i.x * t * t * f.x by A4,A2,BORSUK_2:def 2
.= t by A1,Th3;
end;
theorem Th13:
LoopMlt(f,g),LoopMlt(g,f) are_homotopic
proof
take HopfHomotopy(f,g);
thus thesis by Lm3;
end;
definition
let T,t,f,g;
redefine func HopfHomotopy(f,g) -> Homotopy of LoopMlt(f,g),LoopMlt(g,f); :: redefines HopfHomotopy (TOPALG_7, definition)
coherence
proof
thus LoopMlt(f,g),LoopMlt(g,f) are_homotopic by Th13;
thus thesis by Lm3;
end;
end;
registration
let T,t;
cluster pi_1(T,t) -> commutative;
coherence
proof
set c = the constant Loop of t;
set E = EqRel(T,t);
let x,y be Element of pi_1(T,t);
consider f being Loop of t such that
A1: x = Class(E,f) by TOPALG_1:47;
consider g being Loop of t such that
A2: y = Class(E,g) by TOPALG_1:47;
A3: x * y = Class(E,f+g) & y * x = Class(E,g+f) by A1,A2,TOPALG_1:61;
A4: f+g = LoopMlt(f+c,c+g) & g+f = LoopMlt(g+c,c+f) by Th11;
A5: LoopMlt(f,g),LoopMlt(f+c,c+g) are_homotopic by Th12;
A6: LoopMlt(g,f),LoopMlt(g+c,c+f) are_homotopic by Th12;
LoopMlt(f,g),LoopMlt(g,f) are_homotopic by Th13;
then LoopMlt(f,g), LoopMlt(g+c,c+f) are_homotopic by A6,BORSUK_6:79;
then LoopMlt(f+c,c+g),LoopMlt(g+c,c+f) are_homotopic by A5,BORSUK_6:79;
hence thesis by A3,A4,TOPALG_1:46;
end;
end;